mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
isoMap_hom_inv_id_assoc,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map β
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
x✝¹ :
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun i ↦ ⋯.some
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨l, b, hb⟩ := isCardinalFiltered_iff_aux₂ h₁ h₂
    (fun (f : Arrow A) ↦ F.map f.hom ≫ a f.right)
    (fun (f : Arrow A) ↦ a f.left) hA

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
x✝¹ :
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun i ↦ ⋯.some
l : J
b : j ⟶ l
hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b
⊢ Nonempty (Cocone F)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
⊢ f₁ i ≫ b = f₂ i ≫ b

Tactic:
by rw [← h i, IsFiltered.coeq_condition_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (x ∈ Set.range fun x ↦ f ≫ x) ↔ x ∈ ⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0}

Tactic:
simp only [Set.mem_range, Set.mem_iInter, Set.mem_ofPred_eq, Subtype.forall, RingHom.mem_ker]

Goal state after:
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
⊢ (∃ y, f ≫ y = x) ↔ ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0
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
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 π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
⊢ ∃ i, Nonempty ((a : Fin n) → j a ⟶ i)

Tactic:
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

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

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
heq : Y.hom = hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ MorphismProperty.structuredArrowObj L P Y

Tactic:
P.structuredArrowObj_iff,

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
heq : Y.hom = hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
⊢ P Y.hom
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 B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : WidePullbackShape J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app j = (conesEquivInverseObj B F X✝).π.app j

Tactic:
obtain - | j := j
        · simp
        · dsimp
          rw [← f.w ⟨j⟩]
          rfl

Goal state after:
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + 0 = 1
⊢ IsUnit ↑p

Tactic:
add_zero,

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p = 1
⊢ IsUnit ↑p
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
⊢ False

Tactic:
have hr₁ := addOrderOf_nsmul_eq_zero r

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : addOrderOf r • r = 0
⊢ False
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout f)

Tactic:
← CommRingCat.ofHom_hom f,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
K : WalkingParallelPair ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).Under ⊤ R
this :
  CreatesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ PreservesLimit (K ⋙ MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ R)
    (CategoryTheory.Under.pushout (CommRingCat.ofHom (CommRingCat.Hom.hom f)))
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: 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)
⊢ (tensorEqualizerAux S T f g) (x * y) = (tensorEqualizerAux S T f g) x * (tensorEqualizerAux S T f g) y

Tactic:
by
  apply Subtype.ext
  rw [AlgHom.coe_tensorEqualizerAux]
  simp

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
⊢ P

Tactic:
let r := ringChar (R ⧸ M)

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ P
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L L'
inst✝ : IsScalarTower K L L'
⊢ ↑(toAlgHom K L L').fieldRange = Set.range ⇑(algebraMap L L')

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • ⟦a✝¹⟧ = z • ⟦a✝⟧ ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
← QuotientAddGroup.mk_zsmul,

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ ↑(z • a✝¹) = ↑(z • a✝) ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.get? 0 = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> s.get? 0

Tactic:
cases get? s 0

Goal state after:
case none
α : Type u
s : Seq α
⊢ none = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> none

case some
α : Type u
s : Seq α
val✝ : α
⊢ some val✝ = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> some val✝
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ (cons a s).head = some a

Tactic:
rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]

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

Goal state before:
pp: α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ : Seq α
⊢ ∀ ⦃s₂ : Seq α⦄, motive s₁ s₂ → BisimO motive s₁.destruct s₂.destruct

Tactic:
s₂

Goal state after:
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
⊢ motive s₁ s₂ → BisimO motive s₁.destruct s₂.destruct
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s₁✝ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ : Seq α
⊢ ∀ (s₂ : Seq α), motive' s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'

Tactic:
s₂

Goal state after:
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step : ∀ (s₁ s₂ : Seq α), motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
s₁ s₂ : Seq α
⊢ motive' s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive' s₁' s₂'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ ∀ m < n, ¬(↑s).get (m + 1) = none

Tactic:
intro m

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
⊢ m < n → ¬(↑s).get (m + 1) = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ nil.append s₂ → nil.append s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂

Tactic:
intro m

Goal state after:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
⊢ nil.append s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
⊢ a ∈ (cons c t₁).append s₂ → (cons c t₁).append s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
intro m

Goal state after:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
⊢ (cons c t₁).append s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂
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
F : DirectLimit G f →+* P
⊢ lift G f P (fun i ↦ F.comp (of G f i)) ⋯ = F

Tactic:
by
  ext; simp

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
⊢ lift G f (DirectLimit G f) (of G f) ⋯ = RingHom.id (DirectLimit G f)

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type u
n : ℕ
s : Seq α
⊢ (s.drop n).length' = s.length' - ↑n

Tactic:
by
  cases n with
  | zero => simp
  | succ n =>
    cases s with
    | nil => simp
    | cons x s =>
      simp only [drop_succ_cons, length'_cons, Nat.cast_add, Nat.cast_one]
      convert! drop_length' using 1
      generalize s.length' = m
      enat_to_nat
      lia

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
⊢ map (fun x ↦ RingHom.id (G x)) ⋯ = RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))

Tactic:
by
  ext; simp

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
this : v = ↑⌊v⌋
⊢ v = compExactValue ((of v).contsAux 0) ((of v).contsAux (0 + 1)) (IntFractPair.of v).fr

Tactic:
simpa [compExactValue, IntFractPair.of, fract_eq_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 }
⊢ (of v).s.get? (n + 1) = some { a := 1, b := ↑p'.b }

Tactic:
get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁

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 }
⊢ some { a := 1, b := ↑p'.b } = some { a := 1, b := ↑p'.b }
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
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)
⊢ (map g₂ hg₂).comp (map g₁ hg₁) = map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯

Tactic:
by
  ext; simp

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
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 0

Tactic:
add_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⌋
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R (cons hd nil)

Tactic:
by
  apply Pairwise.cons <;> simp

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
⊢ Pairwise R s.tail

Tactic:
cases s
  · simp
  · simp [h.cons_elim.right]

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
⊢ ∀ (b : ℕ), n ≤ b → v = (of v).convs b

Tactic:
intro m

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
⊢ n ≤ m → v = (of v).convs m
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ ∀ (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:
intro m

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

Goal state before:
pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n :=
      Option.ne_none_iff_exists'.mp not_terminatedAt_n

Goal state after:
case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
a b : K
s_nth_eq : g.s.get? n = some { a := a, b := b }
⊢ g.convs (n + 1) = (g.squashGCF n).convs n