internlm/Lean-Github huggingface dataset:
Theorem: monotonic
Proof state before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ sub_left_monotonic n round ∧ sub_right_monotonic n round
Tactic:
unfold sub_left_monotonic
Proof state after:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    sub_right_monotonic n round
Theorem: monotonic
Proof state before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    sub_right_monotonic n round
Tactic:
unfold sub_right_monotonic
Proof state after:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Theorem: monotonic
Proof state before:
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ (∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)) ∧
    ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
constructor
Proof state after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)

case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Theorem: monotonic
Proof state before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)

case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
.   intro a b c _ _ _ hab
    apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
    exact tsub_le_tsub_left hab _
Proof state after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Theorem: monotonic
Proof state before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
.   intro a b c _ _ _ hba
    apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
    exact tsub_le_tsub_right hba _
Proof state after:
no goals
Theorem: monotonic
Proof state before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (c - b) ≤ round (c - a)
Tactic:
intro a b c _ _ _ hab
Proof state after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ round (c - b) ≤ round (c - a)
Theorem: monotonic
Proof state before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ round (c - b) ≤ round (c - a)
Tactic:
apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
Proof state after:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ c - b ≤ c - a
Theorem: monotonic
Proof state before:
case left
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hab : a ≤ b
⊢ c - b ≤ c - a
Tactic:
exact tsub_le_tsub_left hab _
Proof state after:
no goals
Theorem: monotonic
Proof state before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
⊢ ∀ {a b c : ℕ}, trunc n a = a → trunc n b = b → trunc n c = c → a ≤ b → round (a - c) ≤ round (b - c)
Tactic:
intro a b c _ _ _ hba
Proof state after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ round (a - c) ≤ round (b - c)
Theorem: monotonic
Proof state before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ round (a - c) ≤ round (b - c)
Tactic:
apply round_le_round npos hfaithful₁ hcorrect₀ hcorrect₁
Proof state after:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ a - c ≤ b - c
Theorem: monotonic
Proof state before:
case right
n : ℕ
round : ℕ → ℕ
npos : 0 < n
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hcorrect₁ : correct₁ n round
a b c : ℕ
a✝² : trunc n a = a
a✝¹ : trunc n b = b
a✝ : trunc n c = c
hba : a ≤ b
⊢ a - c ≤ b - c
Tactic:
exact tsub_le_tsub_right hba _
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
a b c d : ℕ
h : a * d = b * c
h' : Coprime a b
⊢ ∃ m, c = m * a ∧ d = m * b
Tactic:
obtain ⟨c₁, rfl⟩ := (Coprime.dvd_mul_left h').mp <| Dvd.intro d h
Proof state after:
case intro
a b d : ℕ
h' : Coprime a b
c₁ : ℕ
h : a * d = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ d = m * b
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro
a b d : ℕ
h' : Coprime a b
c₁ : ℕ
h : a * d = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ d = m * b
Tactic:
obtain ⟨d₁, rfl⟩ := (Coprime.dvd_mul_left h'.symm).mp <| Dvd.intro _ h.symm
Proof state after:
case intro.intro
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
cases' eq_or_ne (a * b) 0 with H H
Proof state after:
case intro.intro.inl
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b = 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b

case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inl
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b = 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
rcases mul_eq_zero.mp H with rfl | rfl
Proof state after:
case intro.intro.inl.inl
b c₁ d₁ : ℕ
h' : Coprime 0 b
h : 0 * (b * d₁) = b * (0 * c₁)
H : 0 * b = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ b * d₁ = m * b

case intro.intro.inl.inr
a c₁ d₁ : ℕ
h' : Coprime a 0
h : a * (0 * d₁) = 0 * (a * c₁)
H : a * 0 = 0
⊢ ∃ m, a * c₁ = m * a ∧ 0 * d₁ = m * 0
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inl.inl
b c₁ d₁ : ℕ
h' : Coprime 0 b
h : 0 * (b * d₁) = b * (0 * c₁)
H : 0 * b = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ b * d₁ = m * b
Tactic:
obtain rfl : b = 1 := h'
Proof state after:
case intro.intro.inl.inl
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ 1 * d₁ = m * 1
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inl.inl
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ ∃ m, 0 * c₁ = m * 0 ∧ 1 * d₁ = m * 1
Tactic:
exact ⟨d₁, by simp⟩
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
c₁ d₁ : ℕ
h : 0 * (1 * d₁) = 1 * (0 * c₁)
H : 0 * 1 = 0
⊢ 0 * c₁ = d₁ * 0 ∧ 1 * d₁ = d₁ * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inl.inr
a c₁ d₁ : ℕ
h' : Coprime a 0
h : a * (0 * d₁) = 0 * (a * c₁)
H : a * 0 = 0
⊢ ∃ m, a * c₁ = m * a ∧ 0 * d₁ = m * 0
Tactic:
obtain rfl : a = 1 := h'.symm
Proof state after:
case intro.intro.inl.inr
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ ∃ m, 1 * c₁ = m * 1 ∧ 0 * d₁ = m * 0
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inl.inr
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ ∃ m, 1 * c₁ = m * 1 ∧ 0 * d₁ = m * 0
Tactic:
exact ⟨c₁, by simp⟩
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
c₁ d₁ : ℕ
h' : Coprime 1 0
h : 1 * (0 * d₁) = 0 * (1 * c₁)
H : 1 * 0 = 0
⊢ 1 * c₁ = c₁ * 1 ∧ 0 * d₁ = c₁ * 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * (b * d₁) = b * (a * c₁)
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
rw [← mul_assoc, ← mul_assoc, mul_comm b] at h
Proof state after:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * b * d₁ = a * b * c₁
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
c₁ d₁ : ℕ
h : a * b * d₁ = a * b * c₁
H : a * b ≠ 0
⊢ ∃ m, a * c₁ = m * a ∧ b * d₁ = m * b
Tactic:
obtain rfl := mul_left_cancel₀ H h
Proof state after:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ ∃ m, a * d₁ = m * a ∧ b * d₁ = m * b
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
case intro.intro.inr
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ ∃ m, a * d₁ = m * a ∧ b * d₁ = m * b
Tactic:
exact ⟨d₁, by simp [mul_comm d₁]⟩
Proof state after:
no goals
Theorem: Nat.proportional_of_mul_eq_mul_of_coprime
Proof state before:
a b : ℕ
h' : Coprime a b
d₁ : ℕ
H : a * b ≠ 0
h : a * b * d₁ = a * b * d₁
⊢ a * d₁ = d₁ * a ∧ b * d₁ = d₁ * b
Tactic:
simp [mul_comm d₁]
Proof state after:
no goals
Theorem: Weight.trunc_mono_lec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ trunc w ≤ trunc w'
Tactic:
simp only [lec_iff, trunc_apply]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ min (w' j) (E w')
Theorem: Weight.trunc_mono_lec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ min (w' j) (E w')
Tactic:
exact fun j ↦ min_le_min (h j) (E_lec_mono h)
Proof state after:
no goals
Theorem: Weight.trunc_lec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ trunc w ≤ w
Tactic:
simp_rw [lec_iff, trunc_apply]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ w j
Theorem: Weight.trunc_lec
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ w j
Tactic:
exact (fun j ↦ min_le_left _ _)
Proof state after:
no goals
Theorem: Weight.trunc_le_E
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
j : Fin (Nat.succ n)
⊢ trunc w j ≤ E w
Tactic:
simp only [trunc, min_le_iff, le_refl, or_true]
Proof state after:
no goals
Theorem: Weight.trunc_zero
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ trunc w 0 = 0
Tactic:
simp only [trunc_apply, Nat.min_eq_zero_iff] at h ⊢
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ w 0 = 0 ∨ E w = 0
Theorem: Weight.trunc_zero
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : w 0 = 0
⊢ w 0 = 0 ∨ E w = 0
Tactic:
exact Or.inl h
Proof state after:
no goals
Theorem: Weight.trunc_Monotone
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
⊢ Monotone (trunc w)
Tactic:
intro i j hij
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ trunc w i ≤ trunc w j
Theorem: Weight.trunc_Monotone
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ trunc w i ≤ trunc w j
Tactic:
simp only [trunc_apply, min_le_iff, le_min_iff, le_refl, and_true, or_true]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ w i ≤ w j ∨ E w ≤ w j
Theorem: Weight.trunc_Monotone
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ w i ≤ w j ∨ E w ≤ w j
Tactic:
exact Or.inl (h hij)
Proof state after:
no goals
Theorem: Weight.trunc_pair_lb
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∃ j, E w < w j ∧ 0 < a j
⊢ E w ≤ pair (trunc w) a
Tactic:
obtain ⟨j, hj, ha⟩ := h
Proof state after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
⊢ E w ≤ pair (trunc w) a
Theorem: Weight.trunc_pair_lb
Proof state before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
⊢ E w ≤ pair (trunc w) a
Tactic:
have hm := mul_le_pair w.trunc a j
Proof state after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * trunc w j ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Theorem: Weight.trunc_pair_lb
Proof state before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * trunc w j ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Tactic:
rw [trunc_apply, min_eq_right_of_lt hj] at hm
Proof state after:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * E w ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Theorem: Weight.trunc_pair_lb
Proof state before:
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * E w ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
Tactic:
exact (Nat.le_mul_of_pos_left _ ha).trans hm
Proof state after:
no goals
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ pair (trunc w) a = pair w a
Tactic:
simp only [pair, trunc_apply]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ ∑ x : Fin (Nat.succ n), a x * min (w x) (E w) = ∑ j : Fin (Nat.succ n), a j * w j
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ ∑ x : Fin (Nat.succ n), a x * min (w x) (E w) = ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
congr
Proof state after:
case e_f
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ (fun x => a x * min (w x) (E w)) = fun j => a j * w j
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
case e_f
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ (fun x => a x * min (w x) (E w)) = fun j => a j * w j
Tactic:
ext j
Proof state after:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ a j * min (w j) (E w) = a j * w j
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ a j * min (w j) (E w) = a j * w j
Tactic:
simp only [mul_eq_mul_left_iff, min_eq_left_iff]
Proof state after:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ w j ≤ E w ∨ a j = 0
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
case e_f.h
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
⊢ w j ≤ E w ∨ a j = 0
Tactic:
cases' le_or_lt (w j) w.E with h' h'
Proof state after:
case e_f.h.inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : w j ≤ E w
⊢ w j ≤ E w ∨ a j = 0

case e_f.h.inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : E w < w j
⊢ w j ≤ E w ∨ a j = 0
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
case e_f.h.inl
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : w j ≤ E w
⊢ w j ≤ E w ∨ a j = 0
Tactic:
exact Or.inl h'
Proof state after:
no goals
Theorem: Weight.trunc_pair_eq_pair
Proof state before:
case e_f.h.inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
j : Fin (Nat.succ n)
h' : E w < w j
⊢ w j ≤ E w ∨ a j = 0
Tactic:
exact Or.inr <| Nat.eq_zero_of_le_zero (h j h')
Proof state after:
no goals
Theorem: Weight.trunc_dom
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ trunc w ≤ w
Tactic:
rw [dom_iff, f_le_iff]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (a : ↑(testvecs n d)), f (trunc w) a ≤ f w a
Theorem: Weight.trunc_dom
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ ∀ (a : ↑(testvecs n d)), f (trunc w) a ≤ f w a
Tactic:
intro a
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ f (trunc w) a ≤ f w a
Theorem: Weight.trunc_dom
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ f (trunc w) a ≤ f w a
Tactic:
simp_rw [f]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E (trunc w) - pair (trunc w) ↑a ≤ E w - pair w ↑a
Theorem: Weight.trunc_dom
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E (trunc w) - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
refine (Nat.sub_le_sub_right (E_trunc_le_E w) _).trans ?_
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Theorem: Weight.trunc_dom
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
by_cases h : ∃ j, w.E < w j ∧ 0 < a.1 j
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a

case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ¬∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Theorem: Weight.trunc_dom
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
rw [Nat.sub_eq_zero_of_le (trunc_pair_lb w a h)]
Proof state after:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ 0 ≤ E w - pair w ↑a
Theorem: Weight.trunc_dom
Proof state before:
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ 0 ≤ E w - pair w ↑a
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Weight.trunc_dom
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ¬∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
push_neg at h
Proof state after:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∀ (j : Fin (Nat.succ n)), E w < w j → ↑a j ≤ 0
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Theorem: Weight.trunc_dom
Proof state before:
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∀ (j : Fin (Nat.succ n)), E w < w j → ↑a j ≤ 0
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
Tactic:
rw [trunc_pair_eq_pair w a h]
Proof state after:
no goals
Theorem: Weight.trunc_dom'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ w ≤ trunc w
Tactic:
rw [dom_iff, f_le_iff]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f (trunc w) a
Theorem: Weight.trunc_dom'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (a : ↑(testvecs n d)), f w a ≤ f (trunc w) a
Tactic:
intro a
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ f w a ≤ f (trunc w) a
Theorem: Weight.trunc_dom'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ f w a ≤ f (trunc w) a
Tactic:
simp_rw [f, ← hE]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ E (trunc w) - pair w ↑a ≤ E (trunc w) - pair (trunc w) ↑a
Theorem: Weight.trunc_dom'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ E (trunc w) - pair w ↑a ≤ E (trunc w) - pair (trunc w) ↑a
Tactic:
exact Nat.sub_le_sub_left (trunc_pair_le_pair w a) _
Proof state after:
no goals
Theorem: Weight.balanced_iff_eq_trunc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ balanced w ↔ trunc w = w
Tactic:
simp_rw [balanced]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (j : Fin (Nat.succ n)), w j ≤ E w) ↔ trunc w = w
Theorem: Weight.balanced_iff_eq_trunc
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ (∀ (j : Fin (Nat.succ n)), w j ≤ E w) ↔ trunc w = w
Tactic:
constructor <;> intro h
Proof state after:
case mp
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
⊢ trunc w = w

case mpr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : trunc w = w
⊢ ∀ (j : Fin (Nat.succ n)), w j ≤ E w
Theorem: Weight.balanced_iff_eq_trunc
Proof state before:
case mp
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
⊢ trunc w = w
Tactic:
ext j
Proof state after:
case mp.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
j : Fin (Nat.succ n)
⊢ trunc w j = w j
Theorem: Weight.balanced_iff_eq_trunc
Proof state before:
case mp.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : ∀ (j : Fin (Nat.succ n)), w j ≤ E w
j : Fin (Nat.succ n)
⊢ trunc w j = w j
Tactic:
exact min_eq_left_iff.mpr (h j)
Proof state after:
no goals
Theorem: Weight.balanced_iff_eq_trunc
Proof state before:
case mpr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : trunc w = w
⊢ ∀ (j : Fin (Nat.succ n)), w j ≤ E w
Tactic:
exact fun j ↦ min_eq_left_iff.mp (congr_fun h j)
Proof state after:
no goals
Theorem: Weight.balanced_iff_lec_E
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ balanced w ↔ w ≤ ↑(E w)
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.trunc_balanced
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ balanced (trunc w)
Tactic:
rw [balanced_iff_lec_E, hE, lec_iff]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (j : Fin (Nat.succ n)), trunc w j ≤ ↑(E w) j