Theorem: Tutorial.Subgroups.SubgroupInf_is_Inf (GlimpseOfLean/Solutions/Topics/GaloisAdjunctions.lean)

State before:
G : Type
inst✝ : Group G
⊢ isInfFun SubgroupInf
Tactic:
intro s H
State after:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ H ∈ lowerBounds s ↔ H ≤ SubgroupInf s

State before:
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ H ∈ lowerBounds s ↔ H ≤ SubgroupInf s
Tactic:
apply isInf.lift (fun H H' ↦ (Subgroup.ext_iff H H').2)
State after:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (SubgroupInf s).carrier

State before:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (SubgroupInf s).carrier
Tactic:
rw [SubgroupInf_carrier]
State after:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (⋂₀ (Subgroup.carrier '' s))

State before:
case hy
G : Type
inst✝ : Group G
s : Set (Subgroup G)
H : Subgroup G
⊢ isInf ((fun H => H.carrier) '' s) (⋂₀ (Subgroup.carrier '' s))
Tactic:
apply isInfInter
State after:
no goals