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) → i ≠ j → v ∈ MultiPart.P M i → ¬v ∈ MultiPart.P M j
Tactic:
intro hi hj hiv ne
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 : i ≠ j
ne : v ∈ MultiPart.P M i
⊢ ¬v ∈ MultiPart.P M 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 : i ≠ j
ne : v ∈ MultiPart.P M i
⊢ ¬v ∈ MultiPart.P M j
Tactic:
contrapose hiv
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)
ne : v ∈ MultiPart.P M i
hiv : ¬¬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)
ne : v ∈ MultiPart.P M i
hiv : ¬¬v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Tactic:
push_neg at hiv
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)
ne : v ∈ MultiPart.P M i
hiv : 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)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ ¬i ≠ j
Tactic:
rw [not_ne_iff]
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)
ne : v ∈ MultiPart.P M i
hiv : 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)
ne : v ∈ MultiPart.P M i
hiv : v ∈ MultiPart.P M j
⊢ i = j
Tactic:
exact uniq_part hi hj ne hiv
State after:
no goals