internlm/Lean-Github huggingface dataset:
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (a - round (a - b) - b) = a - b
Tactic:
rewrite [tsub_right_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (a - b - round (a - b)) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (a - b - round (a - b)) = a - b
Tactic:
rewrite [hfr]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + (a - b - round (a - b)) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + (a - b - round (a - b)) = a - b
Tactic:
rewrite [Nat.add_comm]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ a - b - round (a - b) + round (a - b) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ a - b - round (a - b) + round (a - b) = a - b
Tactic:
exact tsub_add_cancel_of_le round_le
Proof state after:
no goals
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - round (a - b)) = a - round (a - b)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
no goals
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Tactic:
have ⟨_, hfr₂⟩ := b₁ npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Tactic:
have hfe : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Tactic:
have hca : round (a - b) ≤ a := round_sub_le npos hfaithful₀ hfaithful₁ b hfa
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Tactic:
have h : b - (a - round (a - b)) = round (a - b) - (a - b) := by
  apply tsub_eq_of_eq_add
  rewrite [tsub_add_eq_add_tsub le_round]
  rewrite [add_tsub_cancel_of_le hca]
  exact Eq.symm $ tsub_tsub_cancel_of_le hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - round (a - round (a - b))) = a - b
Tactic:
rewrite [hfe]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - (a - round (a - b))) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (b - (a - round (a - b))) = a - b
Tactic:
rewrite [h]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (round (a - b) - (a - b)) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - round (round (a - b) - (a - b)) = a - b
Tactic:
rewrite [round_eq_of_trunc_eq npos hfaithful₀ hfr₂]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - (round (a - b) - (a - b)) = a - b
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
h : b - (a - round (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) - (round (a - b) - (a - b)) = a - b
Tactic:
exact tsub_tsub_cancel_of_le le_round
Proof state after:
no goals
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - round (a - b)) = a - round (a - b)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
no goals
Theorem: sum_and_error₂_hi
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b - (a - round (a - b)) = round (a - b) - (a - b)
Tactic:
apply tsub_eq_of_eq_add
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = round (a - b) - (a - b) + (a - round (a - b))
Theorem: sum_and_error₂_hi
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = round (a - b) - (a - b) + (a - round (a - b))
Tactic:
rewrite [tsub_add_eq_add_tsub le_round]
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = round (a - b) + (a - round (a - b)) - (a - b)
Theorem: sum_and_error₂_hi
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = round (a - b) + (a - round (a - b)) - (a - b)
Tactic:
rewrite [add_tsub_cancel_of_le hca]
Proof state after:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = a - (a - b)
Theorem: sum_and_error₂_hi
Proof state before:
case h
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
le_round : a - b ≤ round (a - b)
left✝ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
hfr₂ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hca : round (a - b) ≤ a
⊢ b = a - (a - b)
Tactic:
exact Eq.symm $ tsub_tsub_cancel_of_le hba
Proof state after:
no goals
Theorem: add_tsub_assoc'
Proof state before:
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b = a - (b - c)
Tactic:
apply eq_tsub_of_add_eq
Proof state after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + (b - c) = a
Theorem: add_tsub_assoc'
Proof state before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + (b - c) = a
Tactic:
rewrite [← add_tsub_assoc_of_le h₂]
Proof state after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + b - c = a
Theorem: add_tsub_assoc'
Proof state before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - b + b - c = a
Tactic:
rewrite [Nat.add_comm a c]
Proof state after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - b + b - c = a
Theorem: add_tsub_assoc'
Proof state before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - b + b - c = a
Tactic:
rewrite [tsub_add_cancel_of_le h₁]
Proof state after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - c = a
Theorem: add_tsub_assoc'
Proof state before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ c + a - c = a
Tactic:
rewrite [Nat.add_comm c a]
Proof state after:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - c = a
Theorem: add_tsub_assoc'
Proof state before:
case h
a b c : ℕ
h₁ : b ≤ c + a
h₂ : c ≤ b
⊢ a + c - c = a
Tactic:
exact add_tsub_cancel_right a c
Proof state after:
no goals
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
⊢ x - x / d = (d - 1) * x / d
Tactic:
have hdvd' : d ∣ (d - 1) * x := Nat.dvd_trans hdvd (Nat.dvd_mul_left _ _)
Proof state after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x - x / d = (d - 1) * x / d
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x - x / d = (d - 1) * x / d
Tactic:
apply Nat.eq_of_mul_eq_mul_right hpos
Proof state after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ (x - x / d) * d = (d - 1) * x / d * d
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ (x - x / d) * d = (d - 1) * x / d * d
Tactic:
rewrite [Nat.mul_sub_right_distrib]
Proof state after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x / d * d = (d - 1) * x / d * d
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x / d * d = (d - 1) * x / d * d
Tactic:
rewrite [Nat.div_mul_cancel hdvd, Nat.div_mul_cancel hdvd']
Proof state after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = (d - 1) * x
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = (d - 1) * x
Tactic:
rewrite [Nat.sub_one, Nat.mul_pred_left]
Proof state after:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = d * x - x
Theorem: sub_div_of_pos_of_dvd
Proof state before:
x d : ℕ
hpos : 0 < d
hdvd : d ∣ x
hdvd' : d ∣ (d - 1) * x
⊢ x * d - x = d * x - x
Tactic:
rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: sub_half_of_even
Proof state before:
x : ℕ
d : 2 ∣ x
⊢ x - x / 2 = x / 2
Tactic:
have h₀ : 2 - 1 = 1 := by rw [← one_add_one_eq_two, add_tsub_cancel_right]
Proof state after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
⊢ x - x / 2 = x / 2
Theorem: sub_half_of_even
Proof state before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
⊢ x - x / 2 = x / 2
Tactic:
have h₁ := sub_div_of_pos_of_dvd two_pos d
Proof state after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = (2 - 1) * x / 2
⊢ x - x / 2 = x / 2
Theorem: sub_half_of_even
Proof state before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = (2 - 1) * x / 2
⊢ x - x / 2 = x / 2
Tactic:
rewrite [h₀, one_mul] at h₁
Proof state after:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = x / 2
⊢ x - x / 2 = x / 2
Theorem: sub_half_of_even
Proof state before:
x : ℕ
d : 2 ∣ x
h₀ : 2 - 1 = 1
h₁ : x - x / 2 = x / 2
⊢ x - x / 2 = x / 2
Tactic:
exact h₁
Proof state after:
no goals
Theorem: sub_half_of_even
Proof state before:
x : ℕ
d : 2 ∣ x
⊢ 2 - 1 = 1
Tactic:
rw [← one_add_one_eq_two, add_tsub_cancel_right]
Proof state after:
no goals
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k ≤ n
Tactic:
apply Nat.le_of_lt_add_of_dvd
Proof state after:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ n

case n
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ℕ
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ n

case n
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ℕ
Tactic:
. exact Nat.add_lt_add_right h₃ k
Proof state after:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Theorem: add_le_of_dvd_of_dvd_of_lt
Proof state before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
. exact Nat.dvd_add h₂ (Nat.dvd_refl _)
Proof state after:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n