Theorem: DoubleSys.doubleLe (days/day25.lean)

State before:
b a : Nat
⊢ b > 0 → a < b * 2 → ¬a < b → b * 2 - 1 - a < b
Tactic:
intros u p q
State after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - 1 - a < b

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - 1 - a < b
Tactic:
rw [<-Nat.sub_add_eq]
State after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - (1 + a) < b

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b * 2 - (1 + a) < b
Tactic:
have p₂: b = b * 2 - b := by 
  rw [Nat.mul_add b 1 1]
  simp
State after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b
Tactic:
conv => rhs; rw [p₂]
State after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b * 2 - b

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b * 2 - (1 + a) < b * 2 - b
Tactic:
apply Nat.sub_lt_sub_left
State after:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < b * 2

case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a

State before:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < b * 2

case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Tactic:
. apply Nat.lt_add_of_pos_left
  simp
  assumption
State after:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a

State before:
case a
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
p₂ : b = b * 2 - b
⊢ b < 1 + a
Tactic:
. apply Nat.lt_of_not_le
  intro p
  apply q
  apply Nat.lt_of_succ_le
  rw [Nat.add_comm] at p
  assumption
State after:
no goals

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 2 - b
Tactic:
rw [Nat.mul_add b 1 1]
State after:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 1 + b * 1 - b

State before:
b a : Nat
u : b > 0
p : a < b * 2
q : ¬a < b
⊢ b = b * 1 + b * 1 - b
Tactic:
simp
State after:
no goals