-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem of_den_mono : (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
case inr.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : 1 ≤ b := of_one_le_get?_partDen nth_partDen_eq

Result:
case inr.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ g.partDens.get? n = none

Tactic:
rwa [Stream'.Seq.TerminatedAt] at terminated

Result:
no goals

Proof state:
case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b :=
  Option.ne_none_iff_exists'.mp not_terminated

Result:
case inr.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.partDens.get? n = none
⊢ g.partDens.get? n = none

Tactic:
rwa [Stream'.Seq.TerminatedAt] at terminated

Result:
no goals

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : g.partDens.get? n = none := by rwa [Stream'.Seq.TerminatedAt] at terminated

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.partDens.get? n = none
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.partDens.get? n = none
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : g.TerminatedAt n :=
  terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this✝ : g.partDens.get? n = none
this : g.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
let g := of v

Result:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ g.dens n ≤ b * g.dens n

Tactic:
simpa using mul_le_mul_of_nonneg_right this zero_le_of_den

Result:
no goals

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this✝ : g.partDens.get? n = none
this : g.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : g.dens (n + 1) = g.dens n :=
  dens_stable_of_terminated n.le_succ this

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this✝¹ : g.partDens.get? n = none
this✝ : g.TerminatedAt n
this : g.dens (n + 1) = g.dens n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Proof state:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this✝¹ : g.partDens.get? n = none
this✝ : g.TerminatedAt n
this : g.dens (n + 1) = g.dens n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rw [this]

Result:
no goals

Proof state:
case inr.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
this : 1 ≤ b
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
calc
  g.dens n ≤ b * g.dens n := by
    simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
  _ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated

Result:
case inl
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

case inr
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)