internlm/Lean-Github huggingface dataset:
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ False
Tactic:
refine (not_in_M_of_dom_ne ⟨w', ⟨?_, ?_⟩, ?_, ?_⟩) hM
Proof state after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' 0 = 0

case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone w'

case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≤ w

case refine_4
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≠ w
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ 1 < g
Tactic:
refine lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr ?_) (Ne.symm hfg)
Proof state after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ g ≠ 0
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ g ≠ 0
Tactic:
by_contra! hg
Proof state after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ False
Tactic:
have h₀' : w = 0
Proof state after:
case h₀'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ w = 0

case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
h₀' : w = 0
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
h₀' : w = 0
⊢ False
Tactic:
exact h₀ h₀'
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case h₀'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ w = 0
Tactic:
ext
Proof state after:
case h₀'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
i✝ : Fin (Nat.succ n)
⊢ w i✝ = 0 i✝
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case h₀'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
i✝ : Fin (Nat.succ n)
⊢ w i✝ = 0 i✝
Tactic:
simp only [Finset.mem_univ, Finset.gcd_eq_zero_iff.mp hg, zero_apply]
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hww'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ w = g • w'
Tactic:
ext i
Proof state after:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (g • w') i
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (g • w') i
Tactic:
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul]
Proof state after:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (Finset.gcd Finset.univ w • fun i => w i / Finset.gcd Finset.univ w) i
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (Finset.gcd Finset.univ w • fun i => w i / Finset.gcd Finset.univ w) i
Tactic:
exact (Nat.mul_div_cancel_left' (Finset.gcd_dvd (Finset.mem_univ i))).symm
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' 0 = 0
Tactic:
simp only
Proof state after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w 0 / Finset.gcd Finset.univ w = 0
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w 0 / Finset.gcd Finset.univ w = 0
Tactic:
rw [hM.1.1, Nat.zero_div]
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone w'
Tactic:
simp only
Proof state after:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone fun i => w i / Finset.gcd Finset.univ w
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone fun i => w i / Finset.gcd Finset.univ w
Tactic:
exact fun i j hij ↦ Nat.div_le_div_right (hM.1.2 hij)
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≤ w
Tactic:
rw [hww', dom_iff]
Proof state after:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ f w' ≤ f (g • w')
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ f w' ≤ f (g • w')
Tactic:
have := f_le_mul w' g.pred
Proof state after:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
this : f w' ≤ f (Nat.succ (Nat.pred g) • w')
⊢ f w' ≤ f (g • w')
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
this : f w' ≤ f (Nat.succ (Nat.pred g) • w')
⊢ f w' ≤ f (g • w')
Tactic:
rwa [Nat.succ_pred_eq_of_pos (zero_lt_one.trans hg)] at this
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≠ w
Tactic:
obtain ⟨i, hi⟩ : ∃ i, w i ≠ 0 := by by_contra! hf; exact h₀ (funext hf)
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
⊢ w' ≠ w
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
⊢ w' ≠ w
Tactic:
have hi' : w' i ≠ 0 := fun hf ↦ hi <| mul_zero g ▸ hf ▸ hww'i i
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
⊢ w' ≠ w
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
⊢ w' ≠ w
Tactic:
intro hf
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = w
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = w
⊢ False
Tactic:
rw [hww'] at hf
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
⊢ False
Tactic:
have h₁ := congr_fun hf i
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = (g • w') i
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = (g • w') i
⊢ False
Tactic:
rw [smul_apply] at h₁
Proof state after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = g * w' i
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = g * w' i
⊢ False
Tactic:
exact hfg (mul_right_cancel₀ hi' ((one_mul _).trans h₁)).symm
Proof state after:
no goals
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ ∃ i, w i ≠ 0
Tactic:
by_contra! hf
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
hf : ∀ (i : Fin (Nat.succ n)), w i = 0
⊢ False
Theorem: Weight.gcd_eq_one_of_in_M
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
hf : ∀ (i : Fin (Nat.succ n)), w i = 0
⊢ False
Tactic:
exact h₀ (funext hf)
Proof state after:
no goals
Theorem: Weight.comp_comp
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp (Weight.comp w σ) τ = Weight.comp w (σ * τ)
Tactic:
simp only [Weight.comp, Equiv.Perm.coe_mul]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ (w ∘ ⇑σ) ∘ ⇑τ = w ∘ ⇑σ ∘ ⇑τ
Theorem: Weight.comp_comp
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ τ : Equiv.Perm (Fin (Nat.succ n))
⊢ (w ∘ ⇑σ) ∘ ⇑τ = w ∘ ⇑σ ∘ ⇑τ
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.sum_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.sum (Weight.comp w σ) = Weight.sum w
Tactic:
simp only [Weight.sum, Function.comp_apply]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ j : Fin (Nat.succ n), Weight.comp w σ j = ∑ j : Fin (Nat.succ n), w j
Theorem: Weight.sum_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ j : Fin (Nat.succ n), Weight.comp w σ j = ∑ j : Fin (Nat.succ n), w j
Tactic:
exact Fintype.sum_bijective σ (Equiv.bijective σ) _ _ (fun i ↦ rfl)
Proof state after:
no goals
Theorem: Weight.sum_smul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ Weight.sum (k • w) = k * Weight.sum w
Tactic:
simp only [Weight.sum, Finset.mul_sum]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∑ j : Fin (Nat.succ n), (k • w) j = ∑ i : Fin (Nat.succ n), k * w i
Theorem: Weight.sum_smul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∑ j : Fin (Nat.succ n), (k • w) j = ∑ i : Fin (Nat.succ n), k * w i
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.sum_add
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
⊢ Weight.sum (w + w') = Weight.sum w + Weight.sum w'
Tactic:
simp only [Weight.sum, add_apply, Finset.sum_add_distrib]
Proof state after:
no goals
Theorem: Weight.mul_le_pair
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ pair w a
Tactic:
simp [pair]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ ∑ j : Fin (Nat.succ n), a j * w j
Theorem: Weight.mul_le_pair
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ k)]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ a k * w k + ∑ x in Finset.univ \ {k}, a x * w x
Theorem: Weight.mul_le_pair
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ a k * w k + ∑ x in Finset.univ \ {k}, a x * w x
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: Weight.pair_add_left
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' a : Weight n d
⊢ pair (w + w') a = pair w a + pair w' a
Tactic:
simp only [pair, add_apply, mul_add, Finset.sum_add_distrib]
Proof state after:
no goals
Theorem: Weight.pair_smul_left
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ pair (k • w) a = k * pair w a
Tactic:
simp_rw [pair, smul_apply, mul_left_comm]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), k * (a x * w x) = k * ∑ j : Fin (Nat.succ n), a j * w j
Theorem: Weight.pair_smul_left
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), k * (a x * w x) = k * ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
exact (Finset.mul_sum Finset.univ (fun i ↦ a i * w i) k).symm
Proof state after:
no goals
Theorem: Weight.pair_swap_le
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
cases' eq_or_ne i j with h h
Proof state after:
case inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i = j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Theorem: Weight.pair_swap_le
Proof state before:
case inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i = j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
simp only [Weight.comp, h, Equiv.swap_self, Equiv.coe_refl, Function.comp_id, le_refl]
Proof state after:
no goals
Theorem: Weight.pair_swap_le
Proof state before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
Tactic:
have haij {k} (hk : k ∈ (univ.erase j).erase i) : (a.comp (Equiv.swap i j)) k = a k
Proof state after:
case haij
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
k : Fin (Nat.succ n)
hk : k ∈ erase (erase univ j) i
⊢ Weight.comp a (Equiv.swap i j) k = a k

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