case refine'_1
α : Type u_1
β : Type ?u.164615
s t : Set α
a b x y : α
f : α → β
h : ncard s = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

case refine'_2
α : Type u_1
β : Type ?u.164615
s t : Set α
a b x y : α
f : α → β
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → ncard s = 3
α : Type u_1
β : Type ?u.164615
s t : Set α
a b x y : α
f : α → β
⊢ ncard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
refine' ⟨fun h ↦ _, _⟩
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ncard {x, y, z} = 3
case refine'_2
α : Type u_1
β : Type ?u.164615
s t : Set α
a b x y : α
f : α → β
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → ncard s = 3
rintro ⟨x, y, z, xy, xz, yz, rfl⟩
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬y ∈ {z}

case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬x ∈ {y, z}
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ncard {x, y, z} = 3
rw [ncard_insert_of_not_mem, ncard_insert_of_not_mem, ncard_singleton]
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬(x = y ∨ x = z)
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬x ∈ {y, z}
rw [mem_insert_iff, mem_singleton_iff]
no goals
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬(x = y ∨ x = z)
tauto
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t✝ : Set α
a b x✝ y : α
f : α → β
x : α
t : Set α
hxt : ¬x ∈ t
ht : ncard t = 2
h : ncard (insert x t) = 3
⊢ ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ insert x t = {x_1, y, z}
case refine'_1
α : Type u_1
β : Type ?u.164615
s t : Set α
a b x y : α
f : α → β
h : ncard s = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
obtain ⟨x, t, hxt, rfl, ht⟩ := eq_insert_of_ncard_eq_succ h
case refine'_1.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
hyz : y ≠ z
hxt : ¬x ∈ {y, z}
ht : ncard {y, z} = 2
h : ncard {x, y, z} = 3
⊢ ∃ x_1 y_1 z_1, x_1 ≠ y_1 ∧ x_1 ≠ z_1 ∧ y_1 ≠ z_1 ∧ {x, y, z} = {x_1, y_1, z_1}
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t✝ : Set α
a b x✝ y : α
f : α → β
x : α
t : Set α
hxt : ¬x ∈ t
ht : ncard t = 2
h : ncard (insert x t) = 3
⊢ ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ insert x t = {x_1, y, z}
obtain ⟨y, z, hyz, rfl⟩ := ncard_eq_two.mp ht
case refine'_1.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
hyz : y ≠ z
hxt : ¬x = y ∧ ¬x = z
ht : ncard {y, z} = 2
h : ncard {x, y, z} = 3
⊢ ∃ x_1 y_1 z_1, x_1 ≠ y_1 ∧ x_1 ≠ z_1 ∧ y_1 ≠ z_1 ∧ {x, y, z} = {x_1, y_1, z_1}
case refine'_1.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
hyz : y ≠ z
hxt : ¬x ∈ {y, z}
ht : ncard {y, z} = 2
h : ncard {x, y, z} = 3
⊢ ∃ x_1 y_1 z_1, x_1 ≠ y_1 ∧ x_1 ≠ z_1 ∧ y_1 ≠ z_1 ∧ {x, y, z} = {x_1, y_1, z_1}
rw [mem_insert_iff, mem_singleton_iff, not_or] at hxt
no goals
case refine'_1.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
hyz : y ≠ z
hxt : ¬x = y ∧ ¬x = z
ht : ncard {y, z} = 2
h : ncard {x, y, z} = 3
⊢ ∃ x_1 y_1 z_1, x_1 ≠ y_1 ∧ x_1 ≠ z_1 ∧ y_1 ≠ z_1 ∧ {x, y, z} = {x_1, y_1, z_1}
exact ⟨x, y, z, hxt.1, hxt.2, hyz, rfl⟩
no goals
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.164615
t : Set α
a b x✝ y✝ : α
f : α → β
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ ¬y ∈ {z}
rwa [mem_singleton_iff]