Theorem: Weight.dom_of_dom_perm (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
⊢ w ≤ sorted w'
Tactic:
refine Tuple.bubble_sort_induction hd (fun (g : Weight n d) i j hij₁ hij₂ hwg ↦ ?_)
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)
Tactic:
let g' := g.comp (Equiv.swap i j)
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
g' : Weight n d := Weight.comp g (Equiv.swap i j)
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
g' : Weight n d := Weight.comp g (Equiv.swap i j)
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)
Tactic:
change w ≤d g'
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
g' : Weight n d := Weight.comp g (Equiv.swap i j)
⊢ w ≤ g'

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
g' : Weight n d := Weight.comp g (Equiv.swap i j)
⊢ w ≤ g'
Tactic:
simp only [dom_iff, f_le_iff, f_apply, SetCoe.forall, Subtype.coe_mk] at hwg ⊢
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x
Tactic:
have hgg' : g'.comp (Equiv.swap i j) = g
State after:
case hgg'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
⊢ Weight.comp g' (Equiv.swap i j) = g

n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x
Tactic:
have hgs : g' i ≤ g' j
State after:
case hgs
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ g' i ≤ g' j

n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
⊢ ∀ x ∈ testvecs n d, E w - pair w x ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) x
Tactic:
intro a ha
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w - pair w a ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w - pair w a ≤ E (Weight.comp g (Equiv.swap i j)) - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
rw [E_perm g (Equiv.swap i j)]
State after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
cases' le_or_lt (a i) (a j) with ham ham
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case hgg'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
⊢ Weight.comp g' (Equiv.swap i j) = g
Tactic:
ext
State after:
case hgg'.h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
i✝ : Fin (Nat.succ n)
⊢ Weight.comp g' (Equiv.swap i j) i✝ = g i✝

State before:
case hgg'.h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
i✝ : Fin (Nat.succ n)
⊢ Weight.comp g' (Equiv.swap i j) i✝ = g i✝
Tactic:
simp only [Weight.comp, Function.comp_apply, Equiv.swap_apply_self]
State after:
no goals

State before:
case hgs
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ g' i ≤ g' j
Tactic:
simp only [Weight.comp, Function.comp_apply, Equiv.swap_apply_left, Equiv.swap_apply_right]
State after:
case hgs
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ g j ≤ g i

State before:
case hgs
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
⊢ g j ≤ g i
Tactic:
exact le_of_lt hij₂
State after:
no goals

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
rw [tsub_le_iff_right]
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a
Tactic:
specialize hwg (a.comp (Equiv.swap i j)) (testvecs_perm ha _)
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w - pair w (Weight.comp a (Equiv.swap i j)) ≤ E g - pair g (Weight.comp a (Equiv.swap i j))
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w - pair w (Weight.comp a (Equiv.swap i j)) ≤ E g - pair g (Weight.comp a (Equiv.swap i j))
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a
Tactic:
rw [pair_swap_eq g, tsub_le_iff_right] at hwg
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a
Tactic:
refine hwg.trans ?_
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j)) ≤
    E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j)) ≤
    E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w a
Tactic:
rw [add_le_add_iff_left]
State after:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

State before:
case inl
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a i ≤ a j
hwg : E w ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a + pair w (Weight.comp a (Equiv.swap i j))
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
exact pair_swap_le (hw (le_of_lt hij₁)) ham
State after:
no goals

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
let a' := a.comp (Equiv.swap i j)
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
have haa' : a'.comp (Equiv.swap i j) = a
State after:
case haa'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
⊢ Weight.comp a' (Equiv.swap i j) = a

case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
have ham' : a' i ≤ a' j
State after:
case ham'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ a' i ≤ a' j

case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
have hag : g'.pair a' = pair g a := by simp only [pair_swap_eq g' a, hgg']
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
have := pair_swap_le (n := n) (d := d) hgs ham'
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
this : pair g' (Weight.comp a' (Equiv.swap i j)) ≤ pair g' a'
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
this : pair g' (Weight.comp a' (Equiv.swap i j)) ≤ pair g' a'
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
simp only [haa', hag] at this
State after:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
this : pair (Weight.comp g (Equiv.swap i j)) a ≤ pair g a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a

State before:
case inr
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
hag : pair g' a' = pair g a
this : pair (Weight.comp g (Equiv.swap i j)) a ≤ pair g a
⊢ E w - pair w a ≤ E g - pair (Weight.comp g (Equiv.swap i j)) a
Tactic:
exact (hwg a ha).trans (Nat.sub_le_sub_left this _)
State after:
no goals

State before:
case haa'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
⊢ Weight.comp a' (Equiv.swap i j) = a
Tactic:
ext
State after:
case haa'.h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
i✝ : Fin (Nat.succ n)
⊢ Weight.comp a' (Equiv.swap i j) i✝ = a i✝

State before:
case haa'.h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
i✝ : Fin (Nat.succ n)
⊢ Weight.comp a' (Equiv.swap i j) i✝ = a i✝
Tactic:
simp only [Weight.comp, Function.comp_apply, Equiv.swap_apply_self]
State after:
no goals

State before:
case ham'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ a' i ≤ a' j
Tactic:
simp only [Weight.comp, Function.comp_apply, Equiv.swap_apply_left, Equiv.swap_apply_right]
State after:
case ham'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ a j ≤ a i

State before:
case ham'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
⊢ a j ≤ a i
Tactic:
exact le_of_lt ham
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
g' : Weight n d := Weight.comp g (Equiv.swap i j)
hwg : ∀ x ∈ testvecs n d, E w - pair w x ≤ E g - pair g x
hgg' : Weight.comp g' (Equiv.swap i j) = g
hgs : g' i ≤ g' j
a : Weight n d
ha : a ∈ testvecs n d
ham : a j < a i
a' : Weight n d := Weight.comp a (Equiv.swap i j)
haa' : Weight.comp a' (Equiv.swap i j) = a
ham' : a' i ≤ a' j
⊢ pair g' a' = pair g a
Tactic:
simp only [pair_swap_eq g' a, hgg']
State after:
no goals