case mp
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

case mpr
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a
constructor
case mp.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
case mp
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
f g : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a
rintro ⟨u, rfl⟩
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
case mp.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a
refine' ⟨a, ha, ⟨a, b, h, pure_injective _⟩, rfl⟩
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1
rw [← pure_mul_pure, ← ha, ← hb]
no goals
case mp.intro.intro.intro.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1
exact u.inv_mul
case mpr.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)
case mpr
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
rintro ⟨a, rfl, ha⟩
no goals
case mpr.intro.intro
F : Type ?u.300168
α : Type u_1
β : Type ?u.300174
γ : Type ?u.300177
δ : Type ?u.300180
ε : Type ?u.300183
inst✝ : DivisionMonoid α
g : Filter α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)
exact ha.filter