Theorem: Weight.pair_swap_le (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
cases' eq_or_ne i j with h h
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i = j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i = j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
simp only [Weight.comp, h, Equiv.swap_self, Equiv.coe_refl, Function.comp_id, le_refl]
State after:
no goals

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
have haij {k} (hk : k ∈ (univ.erase j).erase i) : (a.comp (Equiv.swap i j)) k = a k
State after:
case haij
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
k : Fin (Nat.succ n)
hk : k ∈ erase (erase univ j) i
⊢ Weight.comp a (Equiv.swap i j) k = a k

case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
simp only [pair]
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ ∑ j_1 : Fin (Nat.succ n), Weight.comp a (Equiv.swap i j) j_1 * w j_1 ≤ ∑ j : Fin (Nat.succ n), a j * w j

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ ∑ j_1 : Fin (Nat.succ n), Weight.comp a (Equiv.swap i j) j_1 * w j_1 ≤ ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
rw [← add_sum_erase _ _ (mem_univ i), ← add_sum_erase _ _ (mem_univ j),
    ← add_sum_erase _ _ (mem_erase.mpr ⟨h.symm, mem_univ _⟩),
    ← add_sum_erase _ _ (mem_erase.mpr ⟨h, mem_univ _⟩),
    erase_right_comm, sum_congr rfl @ht, ← add_assoc, ← add_assoc]
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ Weight.comp a (Equiv.swap i j) i * w i + Weight.comp a (Equiv.swap i j) j * w j +
      ∑ x in erase (erase univ j) i, a x * w x ≤
    a j * w j + a i * w i + ∑ x in erase (erase univ j) i, a x * w x

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ Weight.comp a (Equiv.swap i j) i * w i + Weight.comp a (Equiv.swap i j) j * w j +
      ∑ x in erase (erase univ j) i, a x * w x ≤
    a j * w j + a i * w i + ∑ x in erase (erase univ j) i, a x * w x
Tactic:
simp only [comp_apply, Equiv.swap_apply_left, Equiv.swap_apply_right, add_le_add_iff_right]
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a j * w i + a i * w j ≤ a j * w j + a i * w i

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a j * w i + a i * w j ≤ a j * w j + a i * w i
Tactic:
rw [add_comm (a j * w i), add_comm (a j * w j)]
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a i * w j + a j * w i ≤ a i * w i + a j * w j

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a i * w j + a j * w i ≤ a i * w i + a j * w j
Tactic:
exact mul_add_mul_le_mul_add_mul ha hw
State after:
no goals

State before:
case haij
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
k : Fin (Nat.succ n)
hk : k ∈ erase (erase univ j) i
⊢ Weight.comp a (Equiv.swap i j) k = a k
Tactic:
rw [comp_apply,
    Equiv.swap_apply_of_ne_of_ne (ne_of_mem_erase hk)
                                 (ne_of_mem_erase (mem_of_mem_erase hk))]
State after:
no goals