Theorem: Turanpartition.uniq_part (Turan4/Turanpartition.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
⊢ i ∈ range (M.t + 1) → j ∈ range (M.t + 1) → v ∈ MultiPart.P M i → v ∈ MultiPart.P M j → i = j
Tactic:
intro hi hj hiv hjv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
⊢ i = j

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
⊢ i = j
Tactic:
by_contra h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
h : ¬i = j
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hiv : v ∈ MultiPart.P M i
hjv : v ∈ MultiPart.P M j
h : ¬i = j
⊢ False
Tactic:
apply not_disjoint_iff.2 ⟨v, hiv, hjv⟩ (M.disj i hi j hj h)
State after:
no goals