Implicit arguments in definition of subset

Stream: mathlib4

[Dan Velleman]

Consider these examples:

import Mathlib

example (A B : Set Nat) (h : A ⊆ B ∧ True) : A ⊆ B := h.left
example (A B : Set Nat) (h : A ⊆ B ∧ True) : A ⊆ B := And.left h
example (A B : Set Nat) (h : A ⊆ B ∧ True) : A ⊆ B := by
  have h1 : A ⊆ B := h.left
  exact h1

The first works and the other two don't. The error message in the second is

application type mismatch
  h.left
argument
  h
has type
  A ⊆ B ∧ True : Prop
but is expected to have type
  (a✝ ∈ A → a✝ ∈ B) ∧ ?m.88 : Prop

The error message in the third is

type mismatch
  h1
has type
  ?m.353 ∈ A → ?m.353 ∈ B : Prop
but is expected to have type
  A ⊆ B : Prop

I assume the problem is caused by the implicit argument in the definition of subset. I have two questions:

1. Why are the first and second examples different? I thought h.left would be synonymous with And.left h.
2. How do I avoid these problems with implicit arguments?

[Dan Velleman]

By the way, in the third example, after the line have h1 : A ⊆ B := h.left, the tactic state includes h1 : A ⊆ B and the goal is A ⊆ B. How could exact h1 not work?

[Floris van Doorn]

2: It should be fixed by redefining:

protected def Subset (s₁ s₂ : Set α) :=
∀ {a}, a ∈ s₁ → a ∈ s₂

as

protected def Subset (s₁ s₂ : Set α) :=
∀ \{{a\}}, a ∈ s₁ → a ∈ s₂

[Dan Velleman]

@Floris van Doorn , should I file an issue for this or will you?

[Eric Wieser]

Was this manually ported incorrectly? Or is this a mathport bug?

[Mario Carneiro]

it was manually ported before semi-implicits existed

[Dan Velleman]

I filed an issue: #738.

[Jireh Loreaux]

In mathlib4#735 I encountered an issue where Lean 3 and Lean 4 elaborated a declaration differently, and I wanted to mention it in case it matters: The declaration in question was:

@[simp] lemma units.mul_inv' (u : G₀ˣ) : (u : G₀) * u⁻¹ = 1 := mul_inv_cancel u.ne_zero

Note that Lean 3 elaborates this to `(↑u)⁻¹. However, the analogous declaration in Lean 4:

theorem Units.mul_inv' (u : G₀ˣ) : (u : G₀) * u⁻¹ = 1 :=
  mul_inv_cancel u.ne_zero

elaborates to ↑(u⁻¹), which caused us a bit of confusion in that PR. It was easily fixed to match the Lean 3 declaration with:

theorem Units.mul_inv' (u : G₀ˣ) : u * (u : G₀)⁻¹ = 1 :=
  mul_inv_cancel u.ne_zero

Is this difference in elaboration expected and we just need to be aware it might be an issue, or is it aberrant behavior?