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

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

pp: case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f 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
⊢ (map f s).length' = s.length'

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
a : α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inl a) = LiftRelAux R C (Sum.inl a) b

pp: case inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
ca : Computation α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) b

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
a : α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inl a) = LiftRelAux R C (Sum.inl a) b

case inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β ⊕ Computation β
ca : Computation α
⊢ LiftRelAux (Function.swap R) (Function.swap C) b (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inl.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inl b)

pp: case inl.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inr cb)

pp: case inr.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inl b)

pp: case inr.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inr cb)

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inl b)

case inl.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inl a) = LiftRelAux R C (Sum.inl a) (Sum.inr cb)

case inr.inl
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
b : β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inl b)

case inr.inr
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inr cb) (Sum.inr ca) = LiftRelAux R C (Sum.inr ca) (Sum.inr cb)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

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

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

Tactic:
<;>

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

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C (pure a) cb → LiftRel R (pure a) cb

pp: case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
⊢ ∀ (cb : Computation β), C ca'.think cb → LiftRel R ca'.think cb

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
⊢ ∀ (cb : Computation β), C (pure a) cb → LiftRel R (pure a) cb

case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
⊢ ∀ (cb : Computation β), C ca'.think cb → LiftRel R ca'.think cb
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
⊢ LiftRel R (pure a) cb

pp: case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
⊢ LiftRel R ca'.think cb

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
cb : Computation β
Hc : C (pure a) cb
⊢ LiftRel R (pure a) cb

case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
⊢ LiftRel R ca'.think cb
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

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

pp: case h_2
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
opt✝ : Option (IntFractPair K)
heq✝ : IntFractPair.stream v (Nat.succ 0) = none
⊢ none = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
<;>

Goal state after:
case h_1
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
opt✝ : Option (IntFractPair K)
x✝ : IntFractPair K
heq✝ : IntFractPair.stream v (Nat.succ 0) = some x✝
⊢ some { a := 1, b := ↑x✝.b } = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

case h_2
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
opt✝ : Option (IntFractPair K)
heq✝ : IntFractPair.stream v (Nat.succ 0) = none
⊢ none = (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0

pp: case succ
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n✝ : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? (n✝ + 1) = (cons (f x x') (zipWith f s s')).get? (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
⊢ (zipWith f (cons x s) (cons x' s')).get? 0 = (cons (f x x') (zipWith f s s')).get? 0

case succ
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : α
s : Seq α
x' : β
s' : Seq β
n✝ : ℕ
⊢ (zipWith f (cons x s) (cons x' s')).get? (n✝ + 1) = (cons (f x x') (zipWith f s s')).get? (n✝ + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)

pp: case some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) (s₂.get? n)

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (s₂.get? n)

case some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) (s₂.get? n)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) = Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none none

pp: case none.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : β
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (some val✝)

pp: case some.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) none

pp: case some.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ g (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝¹) (some val✝)

Tactic:
<;>

Goal state after:
case none.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ none) = Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none none

case none.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : β
⊢ Option.map₂ g (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) none (some val✝)

case some.none
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝ : α
⊢ Option.map₂ g (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝) none

case some.some
α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ g (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map₂ (fun a b ↦ g (f₁ a) (f₂ b)) (some val✝¹) (some val✝)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))

pp: case some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) (s₂.get? n))

Tactic:
<;>

Goal state after:
case none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (s₂.get? n))

case some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ (s₂.get? n)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) (s₂.get? n))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case none.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)

pp: case none.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val✝))

pp: case some.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) none)

pp: case some.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝¹) (some val✝))

Tactic:
<;>

Goal state after:
case none.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none none)

case none.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ none) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk none (some val✝))

case some.none
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝ : α
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝)) (Option.map f₂ none) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝) none)

case some.some
α : Type u
β : Type v
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
n : ℕ
val✝¹ : α
val✝ : β
⊢ Option.map₂ Prod.mk (Option.map f₁ (some val✝¹)) (Option.map f₂ (some val✝)) =
    Option.map (Prod.map f₁ f₂) (Option.map₂ Prod.mk (some val✝¹) (some val✝))
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
⊢ Int.fract v + ↑⌊v⌋ = ↑⌊v⌋

Tactic:
simp [fract_eq_zero]

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

Goal state before:
pp: case zero
α : Type u
hd : α
tl : Seq α
f : α → α
⊢ ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0

pp: case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n✝ : ℕ
⊢ ((cons hd tl).update 0 f).get? (n✝ + 1) = (cons (f hd) tl).get? (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
hd : α
tl : Seq α
f : α → α
⊢ ((cons hd tl).update 0 f).get? 0 = (cons (f hd) tl).get? 0

case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n✝ : ℕ
⊢ ((cons hd tl).update 0 f).get? (n✝ + 1) = (cons (f hd) tl).get? (n✝ + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case zero
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? 0 = (cons hd (tl.update n f)).get? 0

pp: case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n n✝ : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? (n✝ + 1) = (cons hd (tl.update n f)).get? (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? 0 = (cons hd (tl.update n f)).get? 0

case succ
α : Type u
hd : α
tl : Seq α
f : α → α
n n✝ : ℕ
⊢ ((cons hd tl).update (n + 1) f).get? (n✝ + 1) = (cons hd (tl.update n f)).get? (n✝ + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_ne_zero : ifp_succ_n.fr ≠ 0
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
suffices
        compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr by grind

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_ne_zero : ifp_succ_n.fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case zero
⊢ fib 0 ≤ fib (0 + 1)

pp: case succ
n✝ : ℕ
⊢ fib (n✝ + 1) ≤ fib (n✝ + 1 + 1)

Tactic:
<;>

Goal state after:
case zero
⊢ fib 0 ≤ fib (0 + 1)

case succ
n✝ : ℕ
⊢ fib (n✝ + 1) ≤ fib (n✝ + 1 + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case h_hd
α : Type u
R : α → α → Prop
hd : α
⊢ ∀ x ∈ nil, R hd x

pp: case h_tl
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R nil

Tactic:
<;>

Goal state after:
case h_hd
α : Type u
R : α → α → Prop
hd : α
⊢ ∀ x ∈ nil, R hd x

case h_tl
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R nil
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_ne_zero : ifp_succ_n.fr ≠ 0
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
| inr ifp_succ_n_fr_ne_zero =>

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case refine_2.false
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit false n').fastFibAux = (fib (bit false n'), fib (bit false n' + 1))

pp: case refine_2.true
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit true n').fastFibAux = (fib (bit true n'), fib (bit true n' + 1))

Tactic:
<;>

Goal state after:
case refine_2.false
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit false n').fastFibAux = (fib (bit false n'), fib (bit false n' + 1))

case refine_2.true
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ (bit true n').fastFibAux = (fib (bit true n'), fib (bit true n' + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case refine_2.false
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit false n' + 1)

pp: case refine_2.true
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit true n') ∧ fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)

Tactic:
<;>

Goal state after:
case refine_2.false
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit false n' + 1)

case refine_2.true
n n' : ℕ
ih : n'.fastFibAux = (fib n', fib (n' + 1))
⊢ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit true n') ∧ fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret nil).join.destruct nil.destruct

pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret (Seq.cons x✝ s✝)).join.destruct
    (Seq.cons x✝ s✝).destruct

Tactic:
<;>

Goal state after:
case nil
α : Type u
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret nil).join.destruct nil.destruct

case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret (Seq.cons x✝ s✝)).join.destruct
    (Seq.cons x✝ s✝).destruct