mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules R
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (adj.counit.app (F.obj (Opposite.unop U))).op ≫
          X.val.presheaf.map (F.map (adj.unit.app (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward φ).obj X)).val.app U)) x

Tactic:
dsimp only [id_obj]

Goal state after:
C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules R
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (adj.counit.app (F.obj (Opposite.unop U))).op ≫
          X.val.presheaf.map (F.map (adj.unit.app (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward φ).obj X)).val.app U)) x
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case single.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := single i, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

Tactic:
refine
          ⟨[{ left := ⟨⟨⟩⟩
              right := pair i i'
              hom := ObjectProperty.homMk (homOfLE
                (by simpa using le_inf a.hom.le b.hom.le)) }, _], ?_, rfl⟩

Goal state after:
case single.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit }, right := single i, hom := a },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := single i', hom := b }]
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
⊢ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op = F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op

Tactic:
rw [← F.1.map_comp, ← F.1.map_comp]
    congr 1

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
r : R
m : A
⊢ (↑φ).toFun (r • m) = (RingHom.id R) r • (↑φ).toFun m

Tactic:
simp [Algebra.smul_def]

Goal state after:
R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
r : R
m : A
⊢ φ ((algebraMap R A) r) * φ m = r • φ m
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ Continuous (↑(Hom.hom φ)).range.mkQ.toFun

Tactic:
tauto

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget MagmaCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toMagmaCatIso.isIso_hom

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
x : ↑(ofCocone c).pt.toModuleCat
⊢ (hom m) x =
    (hom
        (ofHom
          { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
            cont := ⋯ }))
      x

Tactic:
refine congr($(hc.uniq ((forget₂ _ _).mapCocone s) ((forget₂ _ _).map m) fun j ↦ ?_).hom x)

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
x : ↑(ofCocone c).pt.toModuleCat
j : J
⊢ c.ι.app j ≫ (forget₂ (TopModuleCat R) (ModuleCat R)).map m =
    ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app j
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 : ι
⊢ (tensorProductFan S P).proj i =
    (Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫ (tensorProductFan' S P).proj i

Tactic:
dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']

Goal state after:
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder =
    (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
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (MorphismProperty.costructuredArrowObj L P).limitsOfShape (Discrete PEmpty.{1}) ≤
    MorphismProperty.costructuredArrowObj L P

Tactic:
rintro X p

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
X : CostructuredArrow L (L.obj Y)
p : (MorphismProperty.costructuredArrowObj L P).limitsOfShape (Discrete PEmpty.{1}) X
⊢ MorphismProperty.costructuredArrowObj L P X
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (MorphismProperty.structuredArrowObj L P).colimitsOfShape (Discrete PEmpty.{1}) ≤
    MorphismProperty.structuredArrowObj L P

Tactic:
rintro X p

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
X : StructuredArrow (L.obj Y) L
p : (MorphismProperty.structuredArrowObj L P).colimitsOfShape (Discrete PEmpty.{1}) X
⊢ MorphismProperty.structuredArrowObj L P X
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
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsMultiplicative
inst✝ : Q.RespectsIso
X : T
⊢ P (𝟙 X)

Tactic:
exact P.id_mem X

Goal state after:
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
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Module.Flat R M
x : ↥((AlgebraTensorModule.lTensor S M) f).ker
⊢ ((AlgebraTensorModule.lTensor S M) f.ker.subtype) ((tensorKerInv S M f) x) = ↑x

Tactic:
simp [LinearMap.tensorKerInv]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
n : ℕ
inst✝ : Invertible ↑n
h : n.Coprime p
⊢ ⅟↑n = ↑(n.gcdA p)

Tactic:
by
  let : Invertible (n : R) := invertibleOfCoprime h
  convert! (rfl : ⅟(n : R) = _)

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

Goal state before:
pp: α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (corec f b).destruct = rmap (corec f) (f b)

Tactic:
dsimp [corec, destruct]

Goal state after:
α : Type u
β : Type v
f : β → α ⊕ β
b : β
⊢ (match Stream'.corec' (Corec.f f) (Sum.inr b) 0 with
    | none => Sum.inr (tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩)
    | some a => Sum.inl a) =
    match f b with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩
Module: Mathlib.Algebra.ContinuedFractions.Basic

Goal state before:
pp: α : Type u_1
inst✝ : One α
a : α
n : ℕ
aₙ : α
h : (GenContFract.ofInteger a).partNums.get? n = some aₙ
⊢ aₙ = 1

Tactic:
cases h

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

Goal state before:
pp: α : Type u_1
inst✝² : One α
inst✝¹ : Zero α
inst✝ : LT α
a : α
n : ℕ
bₙ : α
h : (↑(SimpContFract.ofInteger a)).partDens.get? n = some bₙ
⊢ 0 < bₙ

Tactic:
cases h

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

Goal state before:
pp: case zero.think
α : Type u
a : α
s : Computation α
h✝ : s.think.Results a 0
n : ℕ
h : s.Results a n ∧ 0 = n + 1
⊢ s.think = (pure a).thinkN 0

Tactic:
cases h

Goal state after:
case zero.think.intro
α : Type u
a : α
s : Computation α
h : s.think.Results a 0
n : ℕ
left✝ : s.Results a n
right✝ : 0 = n + 1
⊢ s.think = (pure a).thinkN 0
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
· intro hn _ _ k hkn hk
    exact hn <| le_stable s hkn hk

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

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
simpa [length'_of_terminates h] using lt_length_iff

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

Goal state before:
pp: K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
induction n_le_m with

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
succ_nth_fr_eq_zero : ifp_succ_n.fr = 0
⊢ ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
by
  -- get the witness from `succ_nth_stream_eq_some_iff` and prove that it has the additional
  -- properties
  rcases succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq with
    ⟨ifp_n, seq_nth_eq, _, rfl⟩
  refine ⟨ifp_n, seq_nth_eq, ?_⟩
  simpa only [IntFractPair.of, Int.fract, sub_eq_zero] using succ_nth_fr_eq_zero

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
⊢ (match IntFractPair.seq1 v with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      0 =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
IntFractPair.seq1

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

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

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

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

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

Tactic:
simpa using ⟨s, S, rfl, rfl⟩

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : gp = { a := 1, b := ↑ifp.b }
⊢ gp.a = 1 ∧ ∃ z, gp.b = ↑z

Tactic:
simp [this]

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

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
suffices g.convs (n + 1) = g'.convs n by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
      -- now the result follows from the fact that the convergents coincide at the squashed position
      -- as established in `succ_nth_conv_eq_squashGCF_nth_conv`.
      have : ∀ ⦃b⦄, g.partDens.get? n = some b → b ≠ 0 := by
        intro _ nth_partDen_eq
        grind [exists_s_b_of_partDen nth_partDen_eq]
      exact succ_nth_conv_eq_squashGCF_nth_conv @this

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True

Tactic:
tauto

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Prod

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
sb : Submodule R M
sc : Submodule R P
hsb : sb.FG
hsc : sc.FG
tb : Set M
htb : tb.Finite ∧ span R tb = sb
tc : Set P
htc : tc.Finite ∧ span R tc = sc
⊢ (span R tb).prod (span R tc) = sb.prod sc

Tactic:
htb.2,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
sb : Submodule R M
sc : Submodule R P
hsb : sb.FG
hsc : sc.FG
tb : Set M
htb : tb.Finite ∧ span R tb = sb
tc : Set P
htc : tc.Finite ∧ span R tc = sc
⊢ sb.prod (span R tc) = sb.prod sc
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.inr.succ.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
h✝¹ : Nontrivial R
h✝ : Nontrivial S
n : ℕ
e : Fin (n + 1) → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin (n + 1) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e
this : ∀ (i : Fin (n + 1)), f (e' i) = e i
i : Fin n
⊢ (⇑f ∘ (fun x ↦ x.elim (1 - ∑ i, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) i.succ =
    e i.succ

Tactic:
simp [this]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})

Tactic:
Ideal.isCoprime_span_singleton_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ IsCoprime (1 - e i) (1 - e j)
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
hi : σ ↑i ∉ s
this : f ↑((b i) k) = 0
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0

Tactic:
simp [this]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (∃ y, e * y * e = r) ↔ ∃ y, e * y = r

Tactic:
← (hc.comm _).eq,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ (∃ y, e * (e * y) = r) ↔ ∃ y, e * y = r
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x ↦
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite R ↥(N' i)
_i2 : ∀ (i : ↥s), Free R ↥(N' i)
this : ∀ (i : ↥s), restrict f ⋯ = (e i).conj ((restrict f hp').restrict ⋯)
⊢ ∑ i, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (restrict f ⋯)

Tactic:
simp [this]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) =
    ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V).ker

Tactic:
by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case pos.mk.mk
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
h : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 = !(fst✝, snd✝).2
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2

Tactic:
cases h

Goal state after:
case pos.mk.mk.intro
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
right✝ : (fst✝¹, snd✝¹).2 = !(fst✝, snd✝).2
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
Module: Mathlib.Algebra.Free

Goal state before:
pp: case intro
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
c d e : α
⊢ f (c * d * e) = f (c * (d * e))

Tactic:
simp only [map_mul, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: case left
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝¹ f✝ : α →ₙ* β
x : AssocQuotient α
c d e f : α
⊢ f✝ (c * (d * e * f)) = f✝ (c * (d * (e * f)))

Tactic:
simp only [map_mul, mul_assoc]

Goal state after: