case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
⊢ leftInv (leftInv S) ≤ S
rintro x ⟨⟨y, z, h₁⟩, h₂ : x * y = 1⟩
case h.e'_4
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z
case intro.mk.intro
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x ∈ S
convert z.prop
no goals
case h.e'_4
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : { x // x ∈ S }
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]