Theorem: Tutorial.GroupHom.range_eq_top (Solution/Advanced/Algebra/Lecture2.lean)

State before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ ↔ Function.Surjective ⇑f
Tactic:
constructor
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ → Function.Surjective ⇑f

case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Surjective ⇑f → range f = ⊤

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ → Function.Surjective ⇑f
Tactic:
intro hrange y
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ ∃ a, f a = y

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ ∃ a, f a = y
Tactic:
have hy : y ∈ (⊤ : Subgroup G₂) := by
  simp
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y
Tactic:
rw [← hrange] at hy
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
⊢ ∃ a, f a = y

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
⊢ ∃ a, f a = y
Tactic:
have ⟨x, hx⟩ := hy
State after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
x : G₁
hx : f x = y
⊢ ∃ a, f a = y

State before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ range f
x : G₁
hx : f x = y
⊢ ∃ a, f a = y
Tactic:
exists x
State after:
no goals

State before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ y ∈ ⊤
Tactic:
simp
State after:
no goals

State before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Surjective ⇑f → range f = ⊤
Tactic:
intro hsurj
State after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
⊢ range f = ⊤

State before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
⊢ range f = ⊤
Tactic:
ext y
State after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ y ∈ range f ↔ y ∈ ⊤

State before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ y ∈ range f ↔ y ∈ ⊤
Tactic:
simp only [mem_range, mem_top, iff_true]
State after:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ ∃ a, f a = y

State before:
case mpr.a
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
y : G₂
⊢ ∃ a, f a = y
Tactic:
apply hsurj y
State after:
no goals