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

State before:
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ push f ∘ generate = generate ∘ Set.image ⇑f
Tactic:
apply left_comm_of_right_comm
State after:
case hXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (Set.image ⇑f) ?uXY

case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = ?uXY ∘ ?uYW

case uXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Set G' → Set G

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G

State before:
case hXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (Set.image ⇑f) ?uXY

case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = ?uXY ∘ ?uYW

case uXY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Set G' → Set G

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply image_preimage_adjunction
State after:
case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = Set.preimage ⇑f ∘ ?uYW

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G

State before:
case hZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction (push f) ?uZW

case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ ?uZW = Set.preimage ⇑f ∘ ?uYW

case uZW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Subgroup G

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply push_pull_adjunction
State after:
case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ ?uYW

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G

State before:
case hWY
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uYW

case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ ?uYW

case uYW
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G' → Set G'

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply generate_forget_adjunction
State after:
case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ forget

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G

State before:
case hXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ adjunction generate ?uXZ

case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ ?uXZ ∘ pull f = Set.preimage ⇑f ∘ forget

case uXZ
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ Subgroup G → Set G
Tactic:
apply generate_forget_adjunction
State after:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ⇑f ∘ forget

State before:
case h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
⊢ forget ∘ pull f = Set.preimage ⇑f ∘ forget
Tactic:
ext H
State after:
case h.h.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
H : Subgroup G'
x✝ : G
⊢ x✝ ∈ (forget ∘ pull f) H ↔ x✝ ∈ (Set.preimage ⇑f ∘ forget) H

State before:
case h.h.h
G : Type
inst✝¹ : Group G
G' : Type
inst✝ : Group G'
f : G →* G'
H : Subgroup G'
x✝ : G
⊢ x✝ ∈ (forget ∘ pull f) H ↔ x✝ ∈ (Set.preimage ⇑f ∘ forget) H
Tactic:
exact Iff.rfl
State after:
no goals