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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card M.A = ∑ i in range (M.t + 1), card (MultiPart.P M i)
Tactic:
rw [biUnion_parts M]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card (Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i) = ∑ i in range (M.t + 1), card (MultiPart.P M i)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ card (Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i) = ∑ i in range (M.t + 1), card (MultiPart.P M i)
Tactic:
rw [card_biUnion]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ), x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (MultiPart.P M x) (MultiPart.P M y)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ), x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (MultiPart.P M x) (MultiPart.P M y)
Tactic:
intro x hx y hy ne
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (MultiPart.P M x) (MultiPart.P M y)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (MultiPart.P M x) (MultiPart.P M y)
Tactic:
exact M.disj x hx y hy ne
State after:
no goals