Theorem: Tutorial.GroupHom.range_eq_top (Tutorial/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
  sorry
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:
sorry
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:
sorry
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:
sorry
State after:
no goals