internlm/Lean-Github huggingface dataset:
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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₂
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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 _)
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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 ?_
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm
Proof 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)
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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']
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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'
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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 _)
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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✝
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm
Proof 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']
Proof state after:
no goals
Theorem: Weight.dom_of_dom_perm'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ sorted w ≤ w'
Tactic:
convert dom_of_dom_perm (sorted_is_Monotone w) ((dom_perm w w' (Tuple.sort w)).mpr hd)
Proof state after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = sorted (Weight.comp w' (Tuple.sort w))
Theorem: Weight.dom_of_dom_perm'
Proof state before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = sorted (Weight.comp w' (Tuple.sort w))
Tactic:
rw [sorted, comp_comp]
Proof state after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Theorem: Weight.dom_of_dom_perm'
Proof state before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Tactic:
have help : w' = w'.comp (Tuple.sort w') ↔ Monotone w'
Proof state after:
case help
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
⊢ w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'

case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Theorem: Weight.dom_of_dom_perm'
Proof state before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ w' = Weight.comp w' (Tuple.sort w * Tuple.sort (Weight.comp w' (Tuple.sort w)))
Tactic:
rw [help.mpr hw', comp_comp, eq_comm]
Proof state after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Weight.comp w'
      (Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))) =
    Weight.comp w' (Tuple.sort w')
Theorem: Weight.dom_of_dom_perm'
Proof state before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Weight.comp w'
      (Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))) =
    Weight.comp w' (Tuple.sort w')
Tactic:
apply Tuple.comp_sort_eq_comp_iff_monotone.mpr
Proof state after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Theorem: Weight.dom_of_dom_perm'
Proof state before:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))
Tactic:
let w'' := (w'.comp (Tuple.sort w)).comp (Tuple.sort (w'.comp (Tuple.sort w)))
Proof state after:
case h.e'_4
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw' : Monotone w'
hd : w ≤ w'
help : w' = Weight.comp w' (Tuple.sort w') ↔ Monotone w'
w'' : Weight n d := Weight.comp (Weight.comp w' (Tuple.sort w)) (Tuple.sort (Weight.comp w' (Tuple.sort w)))
⊢ Monotone
    (w' ∘ ⇑(Tuple.sort w' * (Tuple.sort w * Tuple.sort (Weight.comp (Weight.comp w' (Tuple.sort w')) (Tuple.sort w)))))