Theorem: s₂ (Fl.lean)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
cases Nat.le_total (2 * b) a with
| inr hba' => have hf : round (a - b) = a - b := by
    apply hfaithful₀
    exact sterbenz hfa hfb hba hba'
  rewrite [hf, tsub_tsub_cancel_of_le hba]
  exact hfb
| inl hab' => apply sterbenz
  . exact hfa
  . exact trunc_round npos hfaithful₁ (a - b)
  . exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
  . have h : a ≤ 2 * (a - b) := by
      rewrite [Nat.mul_sub_left_distrib]
      rewrite [Nat.two_mul]
      rewrite [add_tsub_assoc_of_le hab']
      exact Nat.le_add_right _ _
    calc
      a = trunc n a             := by rw [hfa]
      _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
      _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
      _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
State after:
no goals

State before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
have hf : round (a - b) = a - b := by
  apply hfaithful₀
  exact sterbenz hfa hfb hba hba'
State after:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n (a - round (a - b)) = a - round (a - b)

State before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
rewrite [hf, tsub_tsub_cancel_of_le hba]
State after:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n b = b

State before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n b = b
Tactic:
exact hfb
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ round (a - b) = a - b
Tactic:
apply hfaithful₀
State after:
case a
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - b) = a - b

State before:
case a
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
Tactic:
exact sterbenz hfa hfb hba hba'
State after:
no goals

State before:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
apply sterbenz
State after:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a

case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)

State before:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a

case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact hfa
State after:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)

State before:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact trunc_round npos hfaithful₁ (a - b)
State after:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)

State before:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
State after:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)

State before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. have h : a ≤ 2 * (a - b) := by
    rewrite [Nat.mul_sub_left_distrib]
    rewrite [Nat.two_mul]
    rewrite [add_tsub_assoc_of_le hab']
    exact Nat.le_add_right _ _
  calc
    a = trunc n a             := by rw [hfa]
    _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
    _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
    _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
State after:
no goals

State before:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a
Tactic:
exact hfa
State after:
no goals

State before:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)
Tactic:
exact trunc_round npos hfaithful₁ (a - b)
State after:
no goals

State before:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a
Tactic:
exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
State after:
no goals

State before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
have h : a ≤ 2 * (a - b) := by
  rewrite [Nat.mul_sub_left_distrib]
  rewrite [Nat.two_mul]
  rewrite [add_tsub_assoc_of_le hab']
  exact Nat.le_add_right _ _
State after:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)

State before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)
Tactic:
calc
  a = trunc n a             := by rw [hfa]
  _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
  _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
  _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * (a - b)
Tactic:
rewrite [Nat.mul_sub_left_distrib]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * a - 2 * b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * a - 2 * b
Tactic:
rewrite [Nat.two_mul]
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + a - 2 * b

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + a - 2 * b
Tactic:
rewrite [add_tsub_assoc_of_le hab']
State after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + (a - 2 * b)

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + (a - 2 * b)
Tactic:
exact Nat.le_add_right _ _
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a = trunc n a
Tactic:
rw [hfa]
State after:
no goals

State before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ trunc n (2 * (a - b)) = 2 * trunc n (a - b)
Tactic:
rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
State after:
no goals