-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉₊ < b * a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ 0 ≤ (b - 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
calc
  ⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
  _ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
  _ ≤ a + (b - 1) * a := by gcongr; positivity
  _ = b * a := by rw [sub_one_mul, add_sub_cancel]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ < b * a

Tactic:
calc
  ⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : α) := by gcongr
  _ < b * a := by rwa [← div_lt_iff₀']; positivity

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * a = b * a

Tactic:
rw [sub_one_mul, add_sub_cancel]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
rw [← sub_pos] at hb

Result:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ < b * a

Tactic:
obtain hab | hba := le_total a (b - 1)⁻¹

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ < b * a

case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉₊ < b * a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈(b - 1)⁻¹⌉₊ < b * a

Tactic:
rwa [← div_lt_iff₀']

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ ≤ ↑⌈(b - 1)⁻¹⌉₊

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + 1 = a + (b - 1) * (b - 1)⁻¹

Tactic:
rw [mul_inv_cancel₀]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a

Tactic:
gcongr

Result:
case bc.a0
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ 0 ≤ b - 1

Proof state:
case bc.a0
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ 0 ≤ b - 1

Tactic:
positivity

Result:
no goals