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

State before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) (pull f)
Tactic:
apply adjunction_of_Inf
State after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ∀ (s : Set (Subgroup G')), pull f (Inf s) = Inf (pull f '' s)

State before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ∀ (s : Set (Subgroup G')), pull f (Inf s) = Inf (pull f '' s)
Tactic:
intro S
State after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
⊢ pull f (Inf S) = Inf (pull f '' S)

State before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
⊢ pull f (Inf S) = Inf (pull f '' S)
Tactic:
ext x
State after:
case h.carrier.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
x : G
⊢ x ∈ (pull f (Inf S)).carrier ↔ x ∈ (Inf (pull f '' S)).carrier

State before:
case h.carrier.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
S : Set (Subgroup G')
x : G
⊢ x ∈ (pull f (Inf S)).carrier ↔ x ∈ (Inf (pull f '' S)).carrier
Tactic:
simp [Inf_carrier, Set.image_image, pull, Set.preimage_iInter]
State after:
no goals