mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
⊢ R a b'

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab : R a b'
⊢ R a b'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ pure a
⊢ ∃ b, b ∈ cb ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯

Tactic:
]

Goal state after:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
b : β
⊢ (∃ b_1, b_1 ∈ ca ∧ R b_1 b) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel (swap R) cb.think ca ↔ LiftRel (swap R) cb ca
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ (map f s).length' = s.length'

Tactic:
]

Goal state after:
case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'

Tactic:
]

Goal state after:
case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1 : Computation α
s2 : Computation β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1 s2
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
⊢ LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ ↑(s.length ⋯) = ↑(s.length h')

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 ↦ x1 = x2) (map f s1) (map f s2)

Tactic:
]

Goal state after:
α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ LiftRel (fun x1 x2 ↦ x1 = x2) (map f s1) (map f s2)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ ⊤ = ⊤

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b').destruct

Tactic:
]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb : b' ∈ pure b
h : R a b'
⊢ LiftRelAux R C (Sum.inl a) (pure b').destruct
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x = 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
x : FreeCommRing ((i : ι) × G i)
hx :
  x ∈
    {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}
⊢ (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) x = 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ b, b ∈ cb.think ∧ R a b

Tactic:
]

Goal state after:
case think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) (Sum.inr cb) ↔ ∃ b, b ∈ cb.think ∧ R a b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ((IntFractPair.stream v n).bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ((IntFractPair.stream v n).bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ (∃ b_1, b_1 ∈ ca ∧ Function.swap R b b_1) ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) (some (x✝, s✝))
    (some (x✝, s✝))

Tactic:
]

Goal state after:
case cons
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) (some (x✝, s✝))
    (some (x✝, s✝))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
H : (IntFractPair.of v).fr = Int.fract v
⊢ some (IntFractPair.of (Int.fract v)⁻¹) = some (IntFractPair.of (Int.fract v)⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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:
]

Goal state after:
case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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
⊢ none = none

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0

Tactic:
]

Goal state after:
case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ (of G f i✝) g = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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:
]

Goal state after:
case succ.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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)
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: case ih
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) (f i j hij x) = (g✝ i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g✝ i) a = 0 → a = 0
i✝ : ι
g : G i✝
hz : (g✝ i✝) g = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr.inl
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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
⊢ none = none

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ.inr.inr
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder 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
⊢ some (IntFractPair.of p.fr⁻¹) = some (IntFractPair.of p.fr⁻¹)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ IntFractPair.stream v (n + 1) = none ↔ IntFractPair.stream v (n + 1) = none

Tactic:
]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)

Tactic:
]

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : ∃ i_1, ∃ (h : ⟨i, x⟩.fst ≤ i_1), (f' ⟨i, x⟩.fst i_1 h) ⟨i, x⟩.snd = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0

Tactic:
]

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝ : IsDirectedOrder ι
i : ι
x : G i
this : Nonempty ι
hix : ∃ i_1, ∃ (h : ⟨i, x⟩.fst ≤ i_1), (f' ⟨i, x⟩.fst i_1 h) ⟨i, x⟩.snd = 0
⊢ ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n

Tactic:
]

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some ∘ fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some ∘ fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.of (IntFractPair.of v).fr⁻¹) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ none = none

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝¹ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) (f✝ i j hij x) = (g✝¹ i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g✝ : (i : ι) → G i →+* G' i
hg : ∀ (i j : ι) (h : i ≤ j), (g✝ j).comp (f i j h) = (f' i j h).comp (g✝ i)
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) ((g✝ i) g) = (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) ((g✝ i) g)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ none = none

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of (fract v)⁻¹).s.get? n = none

Tactic:
]

Goal state after:
case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of (fract v)⁻¹).s.get? n = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f✝ i j hij x) = (g i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i j : ι
h : i ≤ j
⊢ (f'' i j h).comp ((g₂ i).comp (g₁ i)) = (f'' i j h).comp ((g₂ i).comp (g₁ i))

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = v

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
]

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) (IntFractPair.of v).fr

Tactic:
cases eq_or_ne (Int.fract v) 0 with
    | inl fract_eq_zero =>
      -- Int.fract v = 0; we must then have `v = ⌊v⌋`
      suffices v = ⌊v⌋ by
        simpa [compExactValue, IntFractPair.of, fract_eq_zero]
      calc
        v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]
    | inr fract_ne_zero =>
      -- Int.fract v ≠ 0; the claim then easily follows by unfolding a single computation step
      simp [field, contsAux, nextConts, nextNum, nextDen, of_h_eq_floor, compExactValue,
        IntFractPair.of, fract_ne_zero]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream v (n + 1 + 1) = some p'
right✝ : ↑p'.b = p.b
Hp : (of (fract v)⁻¹).s.get? n = some { a := 1, b := ↑p'.b }
⊢ some { a := 1, b := ↑p'.b } = some { a := 1, b := ↑p'.b }

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ convs'Aux (of ↑a).s (n✝ + 1) = 0

Tactic:
]

Goal state after:
case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ convs'Aux (of ↑a).s (n✝ + 1) = 0