mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑R
⊢ (CommRingCat.Hom.hom
        ((iP ≫ π) ≫
          CommRingCat.ofHom
            (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩)))
      x =
    (CommRingCat.Hom.hom (α.app c'.pt)) x

Tactic:
suffices (iP ≫ g' ≫ F.map (c'.ι.app none)) x = α.app c'.pt x by
      simpa [RingHom.liftOfRightInverse_comp_apply] using! this

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑R
⊢ (ConcreteCategory.hom (iP ≫ g' ≫ F.map (c'.ι.app none))) x = (ConcreteCategory.hom (α.app c'.pt)) x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).FinitePresentation
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
⊢ ∃ i g', f ≫ g' = α.app i ∧ g = g' ≫ c.ι.app i

Tactic:
have hc' := isColimitOfPreserves (forget _) hc
  let := f.hom.toAlgebra
  obtain ⟨n, hn⟩ := hf
  let P := CommRingCat.of (MvPolynomial (Fin n) R)
  let iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
  obtain ⟨π, rfl, hπ, s, hs⟩ :
      ∃ π : P ⟶ S, iP ≫ π = f ∧ Function.Surjective π ∧ (RingHom.ker π.hom).FG := by
    obtain ⟨π, h₁, h₂⟩ := hn
    exact ⟨CommRingCat.ofHom π, by ext1; exact π.comp_algebraMap, h₁, h₂⟩
  obtain ⟨i, g', hg', hg''⟩ : ∃ (i : J) (g' : P ⟶ F.obj i),
      π ≫ g = g' ≫ c.ι.app i ∧ iP ≫ g' = α.app i := by
    choose j x h using fun i ↦ Types.jointly_surjective_of_isColimit hc' ((π ≫ g) (.X i))
    obtain ⟨i, ⟨hi⟩⟩ : ∃ i, Nonempty (∀ a, (j a ⟶ i)) := by
      have : ∃ i, ∀ a, Nonempty (j a ⟶ i) := by
        simpa using! IsFiltered.sup_objs_exists (Finset.univ.image j)
      simpa [← exists_true_iff_nonempty, Classical.skolem, -exists_const_iff] using! this
    refine ⟨i, CommRingCat.ofHom (MvPolynomial.eval₂Hom
      (α.app i).hom (F.map (hi _) <| x ·)), ?_, ?_⟩
    · ext1
      apply MvPolynomial.ringHom_ext
      · simpa using! fun x ↦ congr($(hg i).hom x)
      · intro i
        simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
          Functor.const_obj_obj, CommRingCat.hom_ofHom, MvPolynomial.coe_eval₂Hom,
          MvPolynomial.eval₂_X]
        exact (congr($(c.w (hi i)).hom (x i)).trans (h i)).symm
    · ext x
      simp [P, iP]
  have : ∀ r : s, ∃ (i' : J) (hi' : i ⟶ i'), F.map hi' (g' r) = 0 := by
    intro r
    have := Types.FilteredColimit.isColimit_eq_iff _ hc' (xi := g' r) (j := i) (xj := (0 : F.obj i))
    suffices H : (g' ≫ c.ι.app i) r = 0 by
      obtain ⟨k, f, g, e⟩ := this.mp (by simpa using! H)
      exact ⟨k, f, by simpa using! e⟩
    rw [← hg']
    simp [show π r = 0 from hs.le (Ideal.subset_span r.2)]
  choose i' hi' hi'' using this
  obtain ⟨c'⟩ := IsFiltered.cocone_nonempty (WidePushoutShape.wideSpan i i' hi')
  refine ⟨c'.pt, CommRingCat.ofHom (RingHom.liftOfSurjective π.hom hπ
    ⟨(g' ≫ F.map (c'.ι.app none)).hom, ?_⟩), ?_, ?_⟩
  · rw [← hs, Ideal.span_le]
    intro r hr
    rw [← c'.w (.init ⟨r, hr⟩)]
    simp [hi'']
  · ext x
    suffices (iP ≫ g' ≫ F.map (c'.ι.app none)) x = α.app c'.pt x by
      simpa [RingHom.liftOfRightInverse_comp_apply] using! this
    rw [← Category.assoc, hg'', ← NatTrans.naturality]
    simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp]
  · ext x
    obtain ⟨x, rfl⟩ := hπ x
    suffices (π ≫ g) x = (g' ≫ F.map (c'.ι.app none) ≫ c.ι.app _) x by
      simpa only [CommRingCat.hom_comp, CommRingCat.hom_ofHom,
        RingHom.liftOfRightInverse_comp_apply, coe_comp, Function.comp_apply] using! this
    rw [c.w, hg']
    rfl

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
c : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      c =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      c

Tactic:
induction c

Goal state after:
case zero
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      0 =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      0

case tmul
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ : ↑S
y✝ : (i : ι) → ↑(P i).right
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ ⊗ₜ[↑R] y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ ⊗ₜ[↑R] y✝)

case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫
            (Pi.evalAlgHom (↑S) (fun i ↦ ↑S ⊗[↑R] ↑(P i).right) i).toUnder)))
      (x✝ + y✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.right }).hom
⊢ Over.Hom.left (hc.lift (pullbackConeEquivBinaryFan.functor.obj s)) ≫ Over.Hom.left c.fst = s.fst

Tactic:
simpa only using! congr($(hc.fac _ _).left)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Over.mk f) (Over.mk g)).obj { as := WalkingPair.right }).hom
⊢ Over.Hom.left (hc.lift (pullbackConeEquivBinaryFan.functor.obj s)) ≫ Over.Hom.left c.snd = s.snd

Tactic:
simpa only using! congr($(hc.fac _ _).left)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ Limits.HasEqualizers ((toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R)

Tactic:
refine ⟨fun D ↦ ?_⟩
  have := hQe.createsLimitsWalkingParallelPair hQi R
  exact hasLimit_of_created D (Under.forget _ _ R)

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
T : Type u_3
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A →ₐ[R] B
x y : T ⊗[R] ↥(f.equalizer g)
hx : ↑((tensorEqualizerAux S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) x
hy : ↑((tensorEqualizerAux S T f g) y) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) y
⊢ ↑((tensorEqualizerAux S T f g) (x + y)) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) (x + y)

Tactic:
| add x y hx hy =>

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = f s.head :: map f s.tail

Tactic:
← Stream'.eta (map f s),

Goal state after:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ (map f s).head :: (map f s).tail = f s.head :: map f s.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a

Tactic:
exact c.2 h

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

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ s.head = s'.head ∧ R s.tail s'.tail

Tactic:
have h := bisim r

Goal state after:
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
h : BisimO R s.destruct s'.destruct
⊢ s.head = s'.head ∧ R s.tail s'.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.Results a n
⊢ s = (pure a).thinkN n

Tactic:
induction n generalizing s with | zero | succ n IH

Goal state after:
case zero
α : Type u
a : α
s : Computation α
h : s.Results a 0
⊢ s = (pure a).thinkN 0

case succ
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.Results a (n + 1)
⊢ s = (pure a).thinkN (n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ x ∈ take (k + 1 + l) s.tail

Tactic:
apply ih (by lia)

Goal state after:
case succ
α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ s.tail.get? k = some x
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.TerminatedAt (n + k)

Tactic:
exact terminated_stable (Nat.le_add_right _ _) terminatedAt_n

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
⊢ match
    match
      match nil.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    nil.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

pp: case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    (cons x✝ s✝).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
· trivial

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ match
    match
      match (cons x✝ s✝).destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun x ↦
              match x.1.destruct with
              | none =>
                match x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    (cons x✝ s✝).destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Data.Seq.Basic

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

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

Tactic:
· trivial

Goal state after:
case cons
α : Type u
s : Seq α
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = s.append nil ∧ s2 = s) ((cons x✝ s✝).append nil).destruct (cons x✝ s✝).destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : 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)
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) nil.destruct
    nil.destruct

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))
    (cons x✝ s✝).destruct (cons x✝ s✝).destruct

Tactic:
· trivial

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))
    (cons x✝ s✝).destruct (cons x✝ s✝).destruct
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n m : ℕ
s : Seq α
⊢ (s.drop n).get? m = s.get? (n + m)

Tactic:
induction n generalizing m with
  | zero => simp [drop]
  | succ k ih =>
    simp only [drop, get?_tail]
    convert! ih using 2
    lia

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
⊢ Stream'.Seq.nil.get? (n + 1) = (of 0).s.get? n

Tactic:
← cast_zero,

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ Stream'.Seq.nil.get? (n + 1) = (of ↑0).s.get? n
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
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 1 / (of 0).convs' n

Tactic:
← cast_zero,

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 1 / (of ↑0).convs' n
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib n + fib (n + 1) - fib (n + 1) = fib n

Tactic:
add_tsub_cancel_right

Goal state after:
n : ℕ
⊢ fib n = fib n
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n.succ ≤ fib n.succ

Tactic:
succ_le_iff

Goal state after:
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib n.succ
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n

Tactic:
induction five_le_n with
  | refl => rfl -- 5 ≤ fib 5
  | @step n five_le_n IH => -- n + 1 ≤ fib (n + 1) for 5 ≤ n
    rw [succ_le_iff]
    calc
      n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

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

Goal state before:
pp: case pos
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b' : Seq β
this : motive (a.drop (a.length ha)) b'
hb_cons : b' ≠ nil
⊢ False

Tactic:
cases b' with
  | nil =>
    contradiction
  | cons b_hd b_tl =>
    obtain ⟨a_hd, a_tl, ha', _⟩ := step _ _ this _ _ rfl
    apply_fun length' at ha'
    simp only [drop_length', length'_of_terminates ha, tsub_self, length'_cons] at ha'
    generalize a_tl.length' = u at ha'
    enat_to_nat
    lia

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
        squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq

Goal state after:
case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream v (n + 1))

Tactic:
rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) (Option.map (fun p ↦ { a := 1, b := ↑p.b }) (IntFractPair.stream q (n + 1))) =
    Option.map (fun p ↦ { a := 1, b := ↑p.b })
      (Stream'.map (Option.map (IntFractPair.mapFr Rat.cast)) (IntFractPair.stream q) (n + 1))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n

Tactic:
by
  simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
  simp only [Stream'.Seq.get?]
  rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
  rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
    simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

Goal state after: