internlm/Lean-Github huggingface dataset:
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j ∧ 1 ≤ E w
Tactic:
refine ⟨?_, one_le_E w⟩
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ 1 ≤ w j
Tactic:
rw [(Function.update_same k 1 w).symm, this]
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ Function.update w k 1 k ≤ Function.update w k 1 j
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
this : w j = Function.update w k 1 j
⊢ Function.update w k 1 k ≤ Function.update w k 1 j
Tactic:
exact hk₂ (le_of_eq_of_le hi.symm hij)
Proof state after:
no goals
Theorem: Weight.balanced_of_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i = k
hj : j ≠ k
⊢ w j = Function.update w k 1 j
Tactic:
simp only [Function.update_apply, hj, if_false]
Proof state after:
no goals
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j = k
⊢ w i ≤ 1 ∨ E w ≤ 1
Tactic:
exact Or.inl ((le_of_le_of_eq (hw.2 (le_of_le_of_eq hij hj)) hk₁).trans zero_le_one)
Proof state after:
no goals
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
cases' le_or_lt w.E (w j) with h h
Proof state after:
case intro.intro.intro.intro.intro.inr.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : E w ≤ w j
⊢ w i ≤ w j ∨ E w ≤ w j

case intro.intro.intro.intro.intro.inr.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : w j < E w
⊢ w i ≤ w j ∨ E w ≤ w j
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inr.inr.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : E w ≤ w j
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Weight.balanced_of_min'
Proof state before:
case intro.intro.intro.intro.intro.inr.inr.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
k : Fin (Nat.succ n)
hk₁ : w k = 0
hk₂ : Monotone (Function.update w k 1)
hE' : E (Function.update (trunc w) k 1) = E (trunc w)
hb' : balanced (Function.update (trunc w) k 1)
hc : trunc w ≤ Function.update (trunc w) k 1
hne : trunc w ≠ Function.update (trunc w) k 1
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : i ≠ k
hj : j ≠ k
h : w j < E w
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inl (hw.2 hij)
Proof state after:
no goals
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
⊢ w = w'
Tactic:
have h₁ := hmin _ h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
⊢ w = w'
Tactic:
have hmin' := fun u (hu : u ≤d w') ↦ h.trans (hmin u (hu.trans h))
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
⊢ w = w'
Tactic:
have hb := balanced_of_min hw hmin
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
⊢ w = w'
Tactic:
have hb' := balanced_of_min hw' hmin'
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Tactic:
have hE := E_dom_eq hw hw' h₁ h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w' ≤ w
hmin : ∀ u ≤ w, w ≤ u
h₁ : w ≤ w'
hmin' : ∀ u ≤ w', w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Tactic:
exact lec_antisymm
  ((dom_iff_gec_of_balanced hw' hb hE.symm).mp h) ((dom_iff_gec_of_balanced hw hb' hE).mp h₁)
Proof state after:
no goals
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
⊢ w = w'
Tactic:
have hminw := (min_Monotone_iff_min_normalized w).mpr hmin
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
⊢ w = w'
Tactic:
have h₁ := hmin _ hw' h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
⊢ w = w'
Tactic:
have hminw' := fun u (hum : Monotone u) (hu : u ≤d w') ↦ h.trans (hminw u hum (hu.trans h))
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
⊢ w = w'
Tactic:
have hb := balanced_of_min' hw hminw
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
⊢ w = w'
Tactic:
have hb' := balanced_of_min' hw' hminw'
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
⊢ w = w'
Tactic:
have hE := E_dom_eq hw.1 hw'.1 h₁ h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Theorem: Weight.eq_of_dom_and_min'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : normalized w
hw' : normalized w'
h : w' ≤ w
hmin : ∀ (u : Weight n d), normalized u → u ≤ w → w ≤ u
hminw : ∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w'
h₁ : w ≤ w'
hminw' : ∀ (u : Fin (Nat.succ n) → ℕ), Monotone u → u ≤ w' → w' ≤ u
hb : balanced w
hb' : balanced w'
hE : E w = E w'
⊢ w = w'
Tactic:
exact lec_antisymm
  ((dom_iff_gec_of_balanced hw'.1 hb hE.symm).mp h) ((dom_iff_gec_of_balanced hw.1 hb' hE).mp h₁)
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'
⊢ w ≤ sorted w'
Tactic:
refine Tuple.bubble_sort_induction hd (fun (g : Weight n d) i j hij₁ hij₂ hwg ↦ ?_)
Proof 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)
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
hwg : w ≤ g
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)
Tactic:
let g' := g.comp (Equiv.swap i j)
Proof 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)
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
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'
Proof 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'
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
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 ⊢
Proof 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
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
⊢ ∀ 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
Proof 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
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
⊢ ∀ 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
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' 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
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
⊢ ∀ 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
Proof 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
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
⊢ 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)]
Proof 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
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
⊢ 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
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 - 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
Theorem: Weight.dom_of_dom_perm
Proof 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
Proof 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✝
Theorem: Weight.dom_of_dom_perm
Proof 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]
Proof state after:
no goals