Theorem: SimpleGraph.moved (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∃ N, N.A = M.A ∧ N.t = M.t ∧ TuranPartition N ∧ mpDsum M ≤ mpDsum N
Tactic:
apply WellFounded.recursion (InvImage.wf sumSqC Nat.lt_wfRel.wf) M
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : MultiPart α),
    (∀ (y : MultiPart α),
        InvImage WellFoundedRelation.rel sumSqC y x →
          ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N) →
      ∃ N, N.A = x.A ∧ N.t = x.t ∧ TuranPartition N ∧ mpDsum x ≤ mpDsum N

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : MultiPart α),
    (∀ (y : MultiPart α),
        InvImage WellFoundedRelation.rel sumSqC y x →
          ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N) →
      ∃ N, N.A = x.A ∧ N.t = x.t ∧ TuranPartition N ∧ mpDsum x ≤ mpDsum N
Tactic:
intro X h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
by_cases h' : TuranPartition X
State after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
exact ⟨X, rfl, rfl, h', le_rfl⟩
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
obtain ⟨i, hi, j, hj, v, hv, ne, hc⟩ := not_turanPartition_imp h'
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
set Y := move X ⟨hi, hv⟩ ⟨hj, ne⟩ with hY
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h :
  ∀ (y : MultiPart α),
    InvImage WellFoundedRelation.rel sumSqC y X → ∃ N, N.A = y.A ∧ N.t = y.t ∧ TuranPartition N ∧ mpDsum y ≤ mpDsum N
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
specialize h Y (sumSqC_dec X ⟨hi, hv⟩ ⟨hj, ne⟩ hc)
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = Y.A ∧ N.t = Y.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = Y.A ∧ N.t = Y.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
rw [move_t, move_a] at h
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
have := mp_deg_sum_move ⟨hi, hv⟩ ⟨hj, ne⟩ hc
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this :
  ∑ w in X.A, degree (mp X) w <
    ∑ w in (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)).A,
      degree (mp (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i))) w
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this :
  ∑ w in X.A, degree (mp X) w <
    ∑ w in (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)).A,
      degree (mp (move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i))) w
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
rw [← mpDsum, ← mpDsum, ← hY] at this
State after:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this : mpDsum X < mpDsum Y
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
h : ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum Y ≤ mpDsum N
this : mpDsum X < mpDsum Y
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
obtain ⟨N, h1, h2, h3, h4⟩ := h
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ ∃ N, N.A = X.A ∧ N.t = X.t ∧ TuranPartition N ∧ mpDsum X ≤ mpDsum N
Tactic:
refine ⟨N, h1, h2, h3, ?_⟩
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ mpDsum X ≤ mpDsum N

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M X : MultiPart α
h' : ¬TuranPartition X
i : ℕ
hi : i ∈ range (X.t + 1)
j : ℕ
hj : j ∈ range (X.t + 1)
v : α
hv : v ∈ MultiPart.P X i
ne : j ≠ i
hc : card (MultiPart.P X j) + 1 < card (MultiPart.P X i)
Y : MultiPart α := move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
hY : Y = move X (_ : i ∈ range (X.t + 1) ∧ v ∈ MultiPart.P X i) (_ : j ∈ range (X.t + 1) ∧ j ≠ i)
this : mpDsum X < mpDsum Y
N : MultiPart α
h1 : N.A = X.A
h2 : N.t = X.t
h3 : TuranPartition N
h4 : mpDsum Y ≤ mpDsum N
⊢ mpDsum X ≤ mpDsum N
Tactic:
exact this.le.trans h4
State after:
no goals