-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_div_ceil_inv_sub_one (ha : 1 ≤ a) : ⌈⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
refine le_antisymm (ceil_le.2 <| div_le_self (by positivity) ha.le) <| ?_

Result:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ⌈(a - 1)⁻¹⌉ ≤ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉

Proof state:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
ha : 1 ≤ 1
⊢ ⌈↑⌈(1 - 1)⁻¹⌉ / 1⌉ = ⌈(1 - 1)⁻¹⌉

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_4
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1

Tactic:
field_simp

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ 0 < (a - 1)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
obtain rfl | ha := ha.eq_or_lt

Result:
case inl
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
ha : 1 ≤ 1
⊢ ⌈↑⌈(1 - 1)⁻¹⌉ / 1⌉ = ⌈(1 - 1)⁻¹⌉

case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ↑⌈(a - 1)⁻¹⌉ < 1 / (1 - a⁻¹)

Tactic:
convert ceil_lt_add_one _ using 1

Result:
case h.e'_4
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ 1 / (1 - a⁻¹) = (a - 1)⁻¹ + 1

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
have : 0 < a - 1 := by linarith

Result:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ 0 ≤ ↑⌈(a - 1)⁻¹⌉

Tactic:
positivity

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
⊢ 0 < a - 1

Tactic:
linarith

Result:
no goals

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ⌈(a - 1)⁻¹⌉ ≤ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉

Tactic:
rw [le_ceil_iff, sub_lt_comm, div_eq_mul_inv, ← mul_one_sub,
  ← lt_div_iff₀ (sub_pos.2 <| inv_lt_one_of_one_lt₀ ha)]

Result:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ↑⌈(a - 1)⁻¹⌉ < 1 / (1 - a⁻¹)

Proof state:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

Tactic:
have : 0 < ⌈(a - 1)⁻¹⌉ := ceil_pos.2 <| by positivity

Result:
case inr
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this✝ : 0 < a - 1
this : 0 < ⌈(a - 1)⁻¹⌉
⊢ ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉