Theorem: H_P4_1 (FormalBook/Chapter_01.lean)

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
⊢ p / (p - 1) ≤ (k + 1) / k
Tactic:
have h_k_nonzero: k ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr hk)
State after:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k
Tactic:
have h_p_pred_pos: p - 1 > 0 := by linarith
State after:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
⊢ p / (p - 1) ≤ (k + 1) / k

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
⊢ p / (p - 1) ≤ (k + 1) / k
Tactic:
have h_p_pred_nonzero: p - 1 ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr h_p_pred_pos)
State after:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
⊢ p / (p - 1) ≤ (k + 1) / k
Tactic:
have h₁: p / (p - 1) = 1 + 1 / (p - 1) := by
  rw [one_add_div h_p_pred_nonzero, sub_add_cancel]
State after:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
h₁ : p / (p - 1) = 1 + 1 / (p - 1)
⊢ p / (p - 1) ≤ (k + 1) / k

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
h₁ : p / (p - 1) = 1 + 1 / (p - 1)
⊢ p / (p - 1) ≤ (k + 1) / k
Tactic:
rw [← one_add_div h_k_nonzero, h₁, add_le_add_iff_left,
  one_div_le_one_div h_p_pred_pos hk, @le_sub_iff_add_le]
State after:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
h₁ : p / (p - 1) = 1 + 1 / (p - 1)
⊢ k + 1 ≤ p

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
h₁ : p / (p - 1) = 1 + 1 / (p - 1)
⊢ k + 1 ≤ p
Tactic:
exact hp
State after:
no goals

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
⊢ p - 1 > 0
Tactic:
linarith
State after:
no goals

State before:
k p : ℝ
hk : k > 0
hp : p ≥ k + 1
h_k_nonzero : k ≠ 0
h_p_pred_pos : p - 1 > 0
h_p_pred_nonzero : p - 1 ≠ 0
⊢ p / (p - 1) = 1 + 1 / (p - 1)
Tactic:
rw [one_add_div h_p_pred_nonzero, sub_add_cancel]
State after:
no goals