Theorem: monotone_primeCountingReal (FormalBook/Chapter_01.lean)

State before:
⊢ Monotone primeCountingReal
Tactic:
intro a b hab
State after:
a b : ℝ
hab : a ≤ b
⊢ primeCountingReal a ≤ primeCountingReal b

State before:
a b : ℝ
hab : a ≤ b
⊢ primeCountingReal a ≤ primeCountingReal b
Tactic:
unfold primeCountingReal
State after:
a b : ℝ
hab : a ≤ b
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

State before:
a b : ℝ
hab : a ≤ b
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
by_cases ha : a ≤ 0
State after:
case pos
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

State before:
case pos
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
by_cases hb : b ≤ 0
State after:
case pos
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

case neg
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
hb : ¬b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

State before:
case pos
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
hb : b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
simp [ha, hb]
State after:
no goals

State before:
case neg
a b : ℝ
hab : a ≤ b
ha : a ≤ 0
hb : ¬b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
simp [ha, hb]
State after:
no goals

State before:
case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
by_cases hb : b ≤ 0
State after:
case pos
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : ¬b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting

State before:
case pos
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
linarith
State after:
no goals

State before:
case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : ¬b ≤ 0
⊢ (if a ≤ 0 then 0 else ⌊a⌋₊.primeCounting) ≤ if b ≤ 0 then 0 else ⌊b⌋₊.primeCounting
Tactic:
simp [ha, hb]
State after:
case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : ¬b ≤ 0
⊢ ⌊a⌋₊.primeCounting ≤ ⌊b⌋₊.primeCounting

State before:
case neg
a b : ℝ
hab : a ≤ b
ha : ¬a ≤ 0
hb : ¬b ≤ 0
⊢ ⌊a⌋₊.primeCounting ≤ ⌊b⌋₊.primeCounting
Tactic:
exact monotone_primeCounting <| Nat.floor_mono hab
State after:
no goals