α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) ↔ ∃ x x_1 y x_2, x ≠ y
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Nontrivial ↑s ↔ Set.Nontrivial s
rw [← nontrivial_univ_iff, Set.Nontrivial, Set.Nontrivial]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y

case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) ↔ ∃ x x_1 y x_2, x ≠ y
apply Iff.intro
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : ↑s
w✝¹ : x ∈ univ
y : ↑s
w✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y
rintro ⟨x, _, y, _, hxy⟩
no goals
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : ↑s
w✝¹ : x ∈ univ
y : ↑s
w✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
exact ⟨x, Subtype.prop x, y, Subtype.prop y, fun h => hxy (Subtype.coe_injective h)⟩
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y
rintro ⟨x, hx, y, hy, hxy⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
exact ⟨⟨x, hx⟩, mem_univ _, ⟨y, hy⟩, mem_univ _, Subtype.mk_eq_mk.not.mpr hxy⟩