-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem stream_succ (h : Int.fract v ≠ 0) (n : ℕ) :
    IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
rw [stream_zero, stream_succ_of_some (stream_zero v) (ne_of_eq_of_ne H h), H]

Result:
no goals

Proof state:
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rcases eq_or_ne p.fr 0 with hz | hnz

Result:
case succ.inr.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

case succ.inr.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Proof state:
case succ.inr.intro.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hz : p.fr = 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_eq_none_of_fr_eq_zero hp hz, stream_eq_none_of_fr_eq_zero ih hz]

Result:
no goals

Proof state:
case succ.inr.intro.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
hnz : p.fr ≠ 0
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [stream_succ_of_some hp hnz, stream_succ_of_some ih hnz]

Result:
no goals

Proof state:
case succ.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp hsome

Result:
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Proof state:
case succ
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rcases eq_or_ne (IntFractPair.stream (Int.fract v)⁻¹ n) none with hnone | hsome

Result:
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

case succ.inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Proof state:
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [succ_nth_stream_eq_none_iff.mpr (Or.inl hnone),
  succ_nth_stream_eq_none_iff.mpr (Or.inl ih)]

Result:
no goals

Proof state:
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [hnone] at ih

Result:
case succ.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = none
hnone : IntFractPair.stream (Int.fract v)⁻¹ n = none
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Proof state:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Tactic:
have H : (IntFractPair.of v).fr = Int.fract v := by simp [IntFractPair.of]

Result:
case zero
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ IntFractPair.stream v (0 + 1) = IntFractPair.stream (Int.fract v)⁻¹ 0

Proof state:
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
ih : IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Tactic:
rw [hp] at ih

Result:
case succ.inr.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
hsome : IntFractPair.stream (Int.fract v)⁻¹ n ≠ none
p : IntFractPair K
ih : IntFractPair.stream v (n + 1) = some p
hp : IntFractPair.stream (Int.fract v)⁻¹ n = some p
⊢ IntFractPair.stream v (n + 1 + 1) = IntFractPair.stream (Int.fract v)⁻¹ (n + 1)

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
⊢ (IntFractPair.of v).fr = Int.fract v

Tactic:
simp [IntFractPair.of]

Result:
no goals