internlm/Lean-Github huggingface dataset:
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1
Tactic:
rw [sub_eq_add_neg (_ * _), neg_mul_eq_mul_neg, Int.add_mul_ediv_left _ _ (by linarith)]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = ↑d * ↑(Weight.sum w) / (↑n + 1) + -↑(pair w ↑a) + 1
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = ↑d * ↑(Weight.sum w) / (↑n + 1) + -↑(pair w ↑a) + 1
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
Tactic:
zify
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) ≤ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) ≤ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1
Tactic:
refine Int.le_add_one (Int.le_ediv_of_mul_le (by linarith) ?_)
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) * (↑n + 1) ≤ ↑(Weight.sum w) * ↑d
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) * (↑n + 1) ≤ ↑(Weight.sum w) * ↑d
Tactic:
simp only [mul_comm, h]
Proof state after:
no goals
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ 0 < ↑n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑n + 1 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_of_pair_le
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ w ≤ w'
Tactic:
rw [dom_iff, f_le_iff]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
Tactic:
intro a
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
⊢ f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
⊢ f w a ≤ f w' a
Tactic:
by_cases H : 0 ≤ pair' w (v a)
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a

case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : ¬0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a
Tactic:
have h' := h a H
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Tactic:
have H' : 0 ≤ pair' w' (v a) := H.trans h'
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ f w a ≤ f w' a
Tactic:
zify
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ ↑(f w a) ≤ ↑(f w' a)
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ ↑(f w a) ≤ ↑(f w' a)
Tactic:
rw [f_apply_eq_pair'_v_of_nonneg H, f_apply_eq_pair'_v_of_nonneg H']
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) + 1 ≤ pair' w' (v a) / (↑n + 1) + 1
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) + 1 ≤ pair' w' (v a) / (↑n + 1) + 1
Tactic:
simp only [add_le_add_iff_right]
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) ≤ pair' w' (v a) / (↑n + 1)
Theorem: Weight.dom_of_pair_le
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ pair' w (v a) / (↑n + 1) ≤ pair' w' (v a) / (↑n + 1)
Tactic:
exact Int.ediv_le_ediv (by linarith) h'
Proof state after:
no goals
Theorem: Weight.dom_of_pair_le
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : 0 ≤ pair' w (v a)
h' : pair' w (v a) ≤ pair' w' (v a)
H' : 0 ≤ pair' w' (v a)
⊢ 0 < ↑n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.dom_of_pair_le
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : ¬0 ≤ pair' w (v a)
⊢ f w a ≤ f w' a
Tactic:
push_neg at H
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ f w a ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ f w a ≤ f w' a
Tactic:
rw [f_apply_eq_zero_of_neg_pair'_v H]
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ 0 ≤ f w' a
Theorem: Weight.dom_of_pair_le
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ 0 ≤ f w' a
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Weight.dom_dom_of_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ w ≤ w + k • 1 ∧ w + k • 1 ≤ w
Tactic:
simp only [dom_iff, f_eq_on_shift, le_rfl, and_self]
Proof state after:
no goals
Theorem: Weight.dom_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp w σ ≤ Weight.comp w' σ ↔ w ≤ w'
Tactic:
simp [E_perm, pair_perm']
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ (∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)) ↔
    ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' a + pair w a
Theorem: Weight.dom_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ (∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)) ↔
    ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' a + pair w a
Tactic:
refine ⟨fun h a ha ↦ ?_, fun h a ha ↦ h (a.comp σ⁻¹) (testvecs_perm ha σ⁻¹)⟩
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
h : ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w ≤ E w' - pair w' a + pair w a
Theorem: Weight.dom_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
h : ∀ a ∈ testvecs n d, E w ≤ E w' - pair w' (Weight.comp a σ⁻¹) + pair w (Weight.comp a σ⁻¹)
a : Weight n d
ha : a ∈ testvecs n d
⊢ E w ≤ E w' - pair w' a + pair w a
Tactic:
specialize h (a.comp σ) (testvecs_perm ha σ)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
a : Weight n d
ha : a ∈ testvecs n d
h : E w ≤ E w' - pair w' (Weight.comp (Weight.comp a σ) σ⁻¹) + pair w (Weight.comp (Weight.comp a σ) σ⁻¹)
⊢ E w ≤ E w' - pair w' a + pair w a
Theorem: Weight.dom_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
a : Weight n d
ha : a ∈ testvecs n d
h : E w ≤ E w' - pair w' (Weight.comp (Weight.comp a σ) σ⁻¹) + pair w (Weight.comp (Weight.comp a σ) σ⁻¹)
⊢ E w ≤ E w' - pair w' a + pair w a
Tactic:
rwa [comp_comp, mul_right_inv, Weight.comp, Equiv.Perm.coe_one, Function.comp_id] at h
Proof state after:
no goals
Theorem: Weight.E_dom_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : w ≤ w'
⊢ E w ≤ E w'
Tactic:
simp only [dom_iff, f_le_iff] at h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
⊢ E w ≤ E w'
Theorem: Weight.E_dom_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
⊢ E w ≤ E w'
Tactic:
specialize h (tw n d 0)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : f w (tw n d 0) ≤ f w' (tw n d 0)
⊢ E w ≤ E w'
Theorem: Weight.E_dom_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : f w (tw n d 0) ≤ f w' (tw n d 0)
⊢ E w ≤ E w'
Tactic:
simp_rw [eval_f_tw, hw, hw'] at h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : E w - (d - 1) * 0 - 0 ≤ E w' - (d - 1) * 0 - 0
⊢ E w ≤ E w'
Theorem: Weight.E_dom_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : E w - (d - 1) * 0 - 0 ≤ E w' - (d - 1) * 0 - 0
⊢ E w ≤ E w'
Tactic:
simpa only [ge_iff_le, mul_zero, nonpos_iff_eq_zero, tsub_zero] using h
Proof state after:
no goals
Theorem: Weight.lec_iff
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
⊢ w ≤ w' ↔ ∀ (j : Fin (Nat.succ n)), w j ≤ w' j
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.lec_antisymm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
⊢ w = w'
Tactic:
ext j
Proof state after:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
j : Fin (Nat.succ n)
⊢ w j = w' j
Theorem: Weight.lec_antisymm
Proof state before:
case h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h₁ : w ≤ w'
h₂ : w' ≤ w
j : Fin (Nat.succ n)
⊢ w j = w' j
Tactic:
exact le_antisymm ((lec_iff w w').mp h₁ j) ((lec_iff w' w).mp h₂ j)
Proof state after:
no goals
Theorem: Weight.E_lec_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ E w ≤ E w'
Tactic:
simp only [E, add_le_add_iff_right]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ Weight.sum w * d / (n + 1) ≤ Weight.sum w' * d / (n + 1)
Theorem: Weight.E_lec_mono
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ Weight.sum w * d / (n + 1) ≤ Weight.sum w' * d / (n + 1)
Tactic:
exact Nat.div_le_div_right (Nat.mul_le_mul_right _ <| sum_le_sum_of_lec w w' h)
Proof state after:
no goals
Theorem: Weight.normalized_of_Monotone
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'
Tactic:
have h : ∀ i, w 0 ≤ w i := fun _ ↦ hw bot_le
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'
Theorem: Weight.normalized_of_Monotone
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ ∃ k w', w = w' + k • 1 ∧ normalized w'
Tactic:
refine ⟨w 0, fun i ↦ w i - w 0, ?_, ?_, fun i j hij ↦ ?_⟩
Proof state after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ w = (fun i => w i - w 0) + w 0 • 1

case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ (fun i => w i - w 0) 0 = 0

case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (fun i => w i - w 0) i ≤ (fun i => w i - w 0) j
Theorem: Weight.normalized_of_Monotone
Proof state before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ w = (fun i => w i - w 0) + w 0 • 1
Tactic:
ext i
Proof state after:
case refine_1.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i : Fin (Nat.succ n)
⊢ w i = ((fun i => w i - w 0) + w 0 • 1) i
Theorem: Weight.normalized_of_Monotone
Proof state before:
case refine_1.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i : Fin (Nat.succ n)
⊢ w i = ((fun i => w i - w 0) + w 0 • 1) i
Tactic:
simp only [ge_iff_le, add_apply, smul_apply, one_apply, mul_one, Nat.sub_add_cancel (h i)]
Proof state after:
no goals
Theorem: Weight.normalized_of_Monotone
Proof state before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
⊢ (fun i => w i - w 0) 0 = 0
Tactic:
exact Nat.sub_self (w 0)
Proof state after:
no goals
Theorem: Weight.normalized_of_Monotone
Proof state before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (fun i => w i - w 0) i ≤ (fun i => w i - w 0) j
Tactic:
simpa only [ge_iff_le, tsub_le_iff_right, Nat.sub_add_cancel (h j)] using hw hij
Proof state after:
no goals
Theorem: Weight.min_Monotone_iff_min_normalized
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (w' : Weight n d), Monotone w' → w' ≤ w → w ≤ w') ↔ ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
Tactic:
refine ⟨fun h w' hw' hle ↦ h _ hw'.2 hle, fun h w' hw' hle ↦ ?_⟩
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
⊢ w ≤ w'
Theorem: Weight.min_Monotone_iff_min_normalized
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
⊢ w ≤ w'
Tactic:
obtain ⟨k, wr, hwr₁, hwr₂⟩ := normalized_of_Monotone hw'
Proof state after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
⊢ w ≤ w'
Theorem: Weight.min_Monotone_iff_min_normalized
Proof state before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
⊢ w ≤ w'
Tactic:
have h₁ := le_of_le_of_eq (dom_dom_of_shift wr k).1 hwr₁.symm
Proof state after:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
h₁ : wr ≤ w'
⊢ w ≤ w'
Theorem: Weight.min_Monotone_iff_min_normalized
Proof state before:
case intro.intro.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (w' : Weight n d), normalized w' → w' ≤ w → w ≤ w'
w' : Weight n d
hw' : Monotone w'
hle : w' ≤ w
k : ℕ
wr : Weight n d
hwr₁ : w' = wr + k • 1
hwr₂ : normalized wr
h₁ : wr ≤ w'
⊢ w ≤ w'
Tactic:
exact (h wr hwr₂ (h₁.trans hle)).trans h₁
Proof state after:
no goals
Theorem: Weight.normalized_of_sorted
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
⊢ normalized (sorted w)
Tactic:
have hm := sorted_is_Monotone w
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ normalized (sorted w)
Theorem: Weight.normalized_of_sorted
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ normalized (sorted w)
Tactic:
have h₁ : w.sorted ((Tuple.sort w)⁻¹ 0) = 0
Proof state after:
case h₁
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ sorted w ((Tuple.sort w)⁻¹ 0) = 0

n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
h₁ : sorted w ((Tuple.sort w)⁻¹ 0) = 0
⊢ normalized (sorted w)
Theorem: Weight.normalized_of_sorted
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
h₁ : sorted w ((Tuple.sort w)⁻¹ 0) = 0
⊢ normalized (sorted w)
Tactic:
exact ⟨Nat.eq_zero_of_le_zero (le_of_le_of_eq (hm (Fin.zero_le _)) h₁), sorted_is_Monotone w⟩
Proof state after:
no goals
Theorem: Weight.normalized_of_sorted
Proof state before:
case h₁
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ sorted w ((Tuple.sort w)⁻¹ 0) = 0
Tactic:
rwa [sorted, Weight.comp, Function.comp_apply, Equiv.Perm.apply_inv_self]
Proof state after:
no goals
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
⊢ Function.Bijective (tw n 1)
Tactic:
refine ⟨tw_inj n 1, ?_⟩
Proof state after:
n✝ n : ℕ
⊢ Function.Surjective (tw n 1)
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
⊢ Function.Surjective (tw n 1)
Tactic:
intro a
Proof state after:
n✝ n : ℕ
a : ↑(testvecs n 1)
⊢ ∃ a_1, tw n 1 a_1 = a
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
a : ↑(testvecs n 1)
⊢ ∃ a_1, tw n 1 a_1 = a
Tactic:
have h₂ : ∑ k, a.val k = 1 := a.2
Proof state after:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, tw n 1 a_1 = a
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, tw n 1 a_1 = a
Tactic:
simp [tw, tw']
Proof state after:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
have h : ∃ j, a.val j = 1
Proof state after:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, ↑a j = 1

n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h : ∃ j, ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Theorem: Weight.testvecs1
Proof state before:
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h : ∃ j, ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
obtain ⟨j, hj⟩ := h
Proof state after:
case intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Theorem: Weight.testvecs1
Proof state before:
case intro
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∃ a_1, { val := Function.update 0 a_1 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 a_1 1)) } = a
Tactic:
use j
Proof state after:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Tactic:
have h' : ∀ k, k ≠ j → a.val k = 0
Proof state after:
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0

case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Theorem: Weight.testvecs1
Proof state before:
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
Tactic:
ext k
Proof state after:
case h.a.h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
⊢ ↑{ val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } k = ↑a k