[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
rcases exists_pair_ne α with ⟨y, y', h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
⊢ ∃ y, y ≠ x
[PROOFSTEP]
by_cases hx : x = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
rw [← hx] at h 
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : x ≠ y'
hx : x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact ⟨y', h.symm⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x y y' : α
h : y ≠ y'
hx : ¬x = y
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact ⟨y, Ne.symm hx⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
x : α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
letI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
x : α
this : DecidableEq α := Classical.decEq α
⊢ ∃ y, y ≠ x
[PROOFSTEP]
exact Decidable.exists_ne x
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
⊢ ∃ x y, x < y
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ x y, x < y
[PROOFSTEP]
cases lt_or_gt_of_ne hxy
[GOAL]
case intro.intro.inl
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x < y
⊢ ∃ x y, x < y
[PROOFSTEP]
exact ⟨_, _, ‹_›⟩
[GOAL]
case intro.intro.inr
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x > y
⊢ ∃ x y, x < y
[PROOFSTEP]
exact ⟨_, _, ‹_›⟩
[GOAL]
α : Type u_1
β : Type u_2
p : α → Prop
x : Subtype p
⊢ Nontrivial (Subtype p) ↔ ∃ y x_1, y ≠ ↑x
[PROOFSTEP]
simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne.def, Subtype.ext_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
⊢ x = default
[PROOFSTEP]
by_contra H
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Inhabited α
h : ¬Nontrivial α
x : α
H : ¬x = default
⊢ False
[PROOFSTEP]
exact h ⟨_, _, H⟩
[GOAL]
α : Type u_1
β : Type u_2
⊢ Subsingleton α → ∀ (x y : α), x = y
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
h : Subsingleton α
⊢ ∀ (x y : α), x = y
[PROOFSTEP]
exact Subsingleton.elim
[GOAL]
α : Type u_1
β : Type u_2
⊢ ¬Nontrivial α ↔ Subsingleton α
[PROOFSTEP]
simp only [nontrivial_iff, subsingleton_iff, not_exists, Ne.def, not_not]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α
[PROOFSTEP]
rw [← not_nontrivial_iff_subsingleton, or_comm]
[GOAL]
α✝ : Type u_1
β : Type u_2
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α
[PROOFSTEP]
exact Classical.em _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
⊢ Nontrivial (Option α)
[PROOFSTEP]
inhabit α
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
inhabited_h : Inhabited α
⊢ Nontrivial (Option α)
[PROOFSTEP]
exact ⟨none, some default, fun.⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
⊢ Nontrivial α
[PROOFSTEP]
rcases exists_pair_ne β with ⟨x, y, h⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
⊢ Nontrivial α
[PROOFSTEP]
rcases hf x with ⟨x', hx'⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α
[PROOFSTEP]
rcases hf y with ⟨y', hy'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
[PROOFSTEP]
have : x' ≠ y' := by
  refine fun H ↦ h ?_
  rw [← hx', ← hy', H]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ x' ≠ y'
[PROOFSTEP]
refine fun H ↦ h ?_
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [← hx', ← hy', H]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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 α
[PROOFSTEP]
exact ⟨⟨x', y', this⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
by_cases h : f x₂ = y
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : f x₂ = y
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : Nontrivial α
f : α → β
hf : Injective f
y : β
x₁ x₂ : α
hx : x₁ ≠ x₂
h : ¬f x₂ = y
⊢ ∃ x, f x ≠ y
[PROOFSTEP]
exact ⟨x₂, h⟩
[GOAL]
α : Type u_1
β : Type u_2
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
⊢ Nontrivial ((i : I) → f i)
[PROOFSTEP]
letI := Classical.decEq (∀ i : I, f i)
[GOAL]
α : Type u_1
β : Type u_2
I : Type u_3
f : I → Type u_4
i' : I
inst : ∀ (i : I), Nonempty (f i)
inst✝ : Nontrivial (f i')
this : DecidableEq ((i : I) → f i) := Classical.decEq ((i : I) → f i)
⊢ Nontrivial ((i : I) → f i)
[PROOFSTEP]
exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial
