α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
hs : Set.Nontrivial s
z : α
H : ∀ (x : α), x ∈ s → x = z
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
hs : Set.Nontrivial s
z : α
⊢ ∃ x, x ∈ s ∧ x ≠ z
by_contra' H
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
hs : Set.Nontrivial s
z : α
H : ∀ (x : α), x ∈ s → x = z
⊢ False
rcases hs with ⟨x, hx, y, hy, hxy⟩
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False
rw [H x hx, H y hy] at hxy
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False
exact hxy rfl