case intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α
rcases exists_pair_ne β with ⟨x, y, h⟩
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
case intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
rcases hf x with ⟨x', hx'⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
case intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
rcases hf y with ⟨y', hy'⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
have : x' ≠ y' := by
  refine fun H ↦ h ?_
  rw [← hx', ← hy', H]
no goals
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
this : x' ≠ y'
⊢ Nontrivial α
exact ⟨⟨x', y', this⟩⟩
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'
refine fun H ↦ h ?_
no goals
α : Type u_2
β : Type u_1
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y
rw [← hx', ← hy', H]