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

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
preservesLimit_iff_isLimit_mapCone hc,

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ Nonempty (IsLimit ((R.tensorProd S).mapCone c)) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A B : P.Under Q X
g : A ⟶ B
⊢ A.hom ≫ g.right ≫ pushout.inl B.hom f = f ≫ pushout.inr B.hom f

Tactic:
simp [pushout.condition]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
g : X ⟶ Y
h : f = g
⊢ P.HasPushoutsAlong g

Tactic:
subst h

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.HasPushoutsAlong f
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
g : X ⟶ Y
h : f = g
this : P.HasPushoutsAlong g
⊢ P.IsStableUnderCobaseChangeAlong g

Tactic:
subst h

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
this : P.HasPushoutsAlong f
⊢ P.IsStableUnderCobaseChangeAlong f
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
g : X ⟶ Y
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
⊢ P.HasPushoutsAlong g

Tactic:
subst h

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A : P.Under Q X
⊢ P.HasPushoutsAlong f
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
g : X ⟶ Y
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
h : f = g
A : P.Under Q X
⊢ pushout.inl A.hom f ≫ ((pushoutCongr h).hom.app A).right = pushout.inl A.hom g

Tactic:
subst h

Goal state after:
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A : P.Under Q X
⊢ pushout.inl A.hom f ≫ ((pushoutCongr ⋯).hom.app A).right = pushout.inl A.hom f
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.destruct = none → s = nil

Tactic:
dsimp [destruct]

Goal state after:
α : Type u
s : Seq α
⊢ (fun a' ↦ (a', s.tail)) <$> s.get? 0 = none → s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
a : α
s' : Seq α
⊢ s.destruct = some (a, s') → s = cons a s'

Tactic:
dsimp [destruct]

Goal state after:
α : Type u
s : Seq α
a : α
s' : Seq α
⊢ (fun a' ↦ (a', s.tail)) <$> s.get? 0 = some (a, s') → s = cons a s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
h : (Corec.f f none).fst = none
⊢ (Corec.f f (Corec.f f none).snd).fst = none

pp: case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h : (Corec.f f (some b)).fst = none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
· rfl

Goal state after:
case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h : (Corec.f f (some b)).fst = none
⊢ (Corec.f f (Corec.f f (some b)).snd).fst = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
h :
  (match none with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match none with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none

Tactic:
· rfl

Goal state after:
case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
h :
  (match some s with
      | none => (none, none)
      | some (a, b') => (some a, some b')).fst =
    none
⊢ (match
        (match some s with
          | none => (none, none)
          | some (a, b') => (some a, some b')).snd with
      | none => (none, none)
      | some b =>
        match f b with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match none with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

pp: case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
s : α × β
h : f b = some s
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some s with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)

Tactic:
· rfl

Goal state after:
case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
s : α × β
h : f b = some s
⊢ Option.map (fun a' ↦ (a', tail ⟨corec' (Corec.f f) (some b), ⋯⟩))
      (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
    match some s with
    | none => none
    | some (a, b) => some (a, ⟨corec' (Corec.f f) (some b), ⋯⟩)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil.nil.left
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head

pp: case nil.nil.right
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail

Tactic:
· rfl

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
⊢ s.destruct = Sum.inl a → s = pure a

Tactic:
dsimp [destruct]

Goal state after:
α : Type u
s : Computation α
a : α
⊢ (match s.val 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s s' : Computation α
⊢ s.destruct = Sum.inr s' → s = s'.think

Tactic:
dsimp [destruct]

Goal state after:
α : Type u
s s' : Computation α
⊢ (match s.val 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case inl
α : Type u
β : Type v
f : β → α ⊕ β
b : β
a : α
h : f b = Sum.inl a
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inl a) with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inl a with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩

Tactic:
· rfl

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (match Sum.rec some (fun x ↦ none) (Sum.inr b') with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match Sum.inr b' with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case left
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (s₁ ⋈ s₂).even.head = s₁.head

pp: case right
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail

Tactic:
· rfl

Goal state after:
case right
α : Type u
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = (s₁ ⋈ s₂).even
⊢ (fun s₁' s₁ ↦ ∃ s₂, s₁' = (s₁ ⋈ s₂).even) (s₁ ⋈ s₂).even.tail s₁.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case left
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (s.even ⋈ s.odd).head = s.head

pp: case right
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail

Tactic:
· rfl

Goal state after:
case right
α : Type u
s₁ s' s : Stream' α
h : s' = s.even ⋈ s.odd
⊢ (fun s' s ↦ s' = s.even ⋈ s.odd) (s.even ⋈ s.odd).tail s.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
h : s.val n = none
⊢ none = (empty α).val n

pp: case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n

Tactic:
· rfl

Goal state after:
case some
α : Type u
s : Computation α
H : ¬s.Terminates
n : ℕ
val✝ : α
h : s.val n = some val✝
⊢ some val✝ = (empty α).val n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s : Stream' α
⊢ s.inits.get 0 = ([s.head] :: map (List.cons s.head) s.tail.inits).get 0

pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)

Tactic:
· rfl

Goal state after:
case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ s.inits.get (n✝ + 1) = ([s.head] :: map (List.cons s.head) s.tail.inits).get (n✝ + 1)
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
⊢ nats.get 0 = (0 :: map succ nats).get 0

pp: case succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)

Tactic:
· rfl

Goal state after:
case succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)
Module: Mathlib.Data.Seq.Basic

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

Tactic:
| cons _ t =>

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

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

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap R]

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: α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ map f (s.append t) = (map f s).append (map f t)

Tactic:
refine eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t))
    ?_ ⟨s, t, rfl, rfl⟩

Goal state after:
α : Type u
β : Type v
f : α → β
s t : Seq α
⊢ IsBisimulation fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (nil.append (cons x✝ t))).destruct ((map f nil).append (map f (cons x✝ t))).destruct

Tactic:
| cons _ t =>

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
h : fract v ≠ 0
⊢ (some (IntFractPair.of (IntFractPair.of v).fr⁻¹)).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
Option.bind

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.bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) = none

Tactic:
Option.bind

Goal state after:
case zero
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ none = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case zero.inl
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 = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) (IntFractPair.of v).fr

Tactic:
| inl fract_eq_zero =>

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

Goal state before:
pp: case neg
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : ¬m = n
⊢ s.get? m = s.get? m

Tactic:
· rfl

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
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
⊢ (map (fun x ↦ ↑(e x)) he).comp (map (fun i ↦ ↑(e i).symm) ⋯) = RingHom.id (DirectLimit G' fun x x_1 h ↦ ⇑(f' x x_1 h))

Tactic:
simp [map_comp]

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
e : (i : ι) → G i ≃+* G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)
⊢ (map (fun i ↦ ↑(e i).symm) ⋯).comp (map (fun x ↦ ↑(e x)) he) = RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))

Tactic:
simp [map_comp]

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

Goal state before:
pp: case succ
n : ℕ
ih : (fib n).Coprime (fib (n + 1))
⊢ (fib (n + 1)).Coprime (fib (n + 1 + 1))

Tactic:
simp only [fib_add_two, coprime_add_self_right, Coprime, ih.symm]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)

Tactic:
| cons x s_1 =>

Goal state after:
case cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.inr
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

Tactic:
cases s_succ_mth_eq : s.get? (m + 1)

Goal state after:
case some.inr.none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
s_succ_mth_eq : s.get? (m + 1) = none
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m

case some.inr.some
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
val✝ : Pair K
s_succ_mth_eq : s.get? (m + 1) = some val✝
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case zero
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : 0 ≤ n
⊢ g.contsAux 0 = (g.squashGCF n).contsAux 0

pp: case succ
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)

Tactic:
· rfl

Goal state after:
case succ
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' : ℕ
IH : ∀ m < 0 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : 0 + 1 ≤ n' + 1
⊢ g.contsAux (0 + 1) = (g.squashGCF (n' + 1)).contsAux (0 + 1)

pp: case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)

Tactic:
· rfl

Goal state after:
case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Tactic:
clear m
      intro m IH m_le_n
      rcases m with - | m'
      · rfl
      · rcases n with - | n'
        · exact (m'.not_succ_le_zero m_le_n).elim
        -- 1 ≰ 0
        · rcases m' with - | m''
          · rfl
          · -- get some inequalities to instantiate the IH for m'' and m'' + 1
            have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
            have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
            have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
            have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
            have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
              squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
            simp [contsAux, succ_m''th_contsAux_eq, m''th_contsAux_eq, this]

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

Goal state before:
pp: case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
⊢ |v - (of v).convs n| < ε

Tactic:
let nB := g.dens (n + 1)

Goal state after:
case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
⊢ |v - (of v).convs n| < ε