mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (x.mul y)) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) (x.mul y))

Tactic:
| mul x y hx hy =>

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

Goal state before:
pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
⊢ f = g

Tactic:
let g' : S →ₐ[R] T := ⟨g.hom, fun _ ↦ rfl⟩

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
g' : S →ₐ[R] ↑T := { toRingHom := Hom.hom g, commutes' := ⋯ }
⊢ f = g
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 ⟶ j'
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j' = ((h.isoMap α ⋯).inv ≫ F.map β) ≫ F.map φ

Tactic:
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 ⟶ j'
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j' = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ
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
s : Cone F
j : J
⊢ (s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToLeft i₀ j)) ≫
      (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j)

Tactic:
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
s : Cone F
j : J
⊢ s.π.app (IsCofiltered.min i₀ j) ≫
      F.map (minToLeft i₀ j) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j)
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
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ (c.π.app i ≫ F.map α) ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β

Tactic:
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
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ c.π.app i ≫ F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ (F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv) ≫ (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ (h.isoMap β ⋯).hom =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ (F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β) ≫ F.map δ = F.map α ≫ F.map δ

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ ((h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β) ≫ F.map δ = F.map α ≫ F.map δ
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ ((h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β) ≫ F.map δ = F.map α ≫ F.map δ

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map β ≫ F.map δ = F.map α ≫ F.map δ
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
j : J
⊢ (F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv) ≫
      F.map (leftToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j) =
    F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j)

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
j : J
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j) =
    F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j)
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.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ (F.map β ≫ (h.isoMap α ⋯).inv) ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i

Tactic:
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.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ F.map β ≫ (h.isoMap α ⋯).inv ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ C'
inst✝ : F.IsEquivalence
⊢ IsCardinalPresentable X κ → IsCardinalPresentable (F.obj X) κ

Tactic:
intro
    infer_instance

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

Goal state before:
pp: case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set ↑S),
    Ideal.span s = ⊤ → (∀ f ∈ s, Q (of (Localization.Away f))) → s.Finite → (ObjectProperty.ofObj f).isoClosure S
hs' : ¬s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S

pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
· obtain ⟨s', hs's, hs'⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
    exact this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet

Goal state after:
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
⊢ PreservesFilteredColimits (coyoneda.obj (Opposite.op S))

Tactic:
exact preservesFilteredColimits_coyoneda R S hS

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

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
⊢ ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f = ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g

Tactic:
by rw [equalizer_comp]

Goal state after:
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✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P Y.hom

Tactic:
show Y.hom = L.map (pres.π.app .left).left ≫ (pres.diag.obj .left).hom by simp

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✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.π.app WalkingCospan.left).left ≫ (pres.diag.obj WalkingCospan.left).hom)
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'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
⊢ x⁻¹ ∈ S

Tactic:
by_cases hx0 : x = 0
    · rw [hx0, inv_zero]
      exact S.zero_mem
    let hS' := hS.toField
    obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)
    rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy
    exact hy.symm ▸ y.2

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
v : Seq1 α
H : s.destruct = some v
⊢ motive s

Tactic:
obtain ⟨a, s'⟩ := v

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
a : α
s' : Seq α
H : s.destruct = some (a, s')
⊢ motive s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)

Tactic:
ih,

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ f ((iterate f (f a)).get n) = (iterate f (f a)).get (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b

Tactic:
· rw [al e]; exact h

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

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h

Tactic:
rw [cycle_eq]; exact mem_append_stream_left _ ainl

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

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (initsCore (l ++ [s.head]) s.tail).get n = (initsCore (a :: l) s).get (n + 1)

Tactic:
ih,

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = (initsCore (a :: l) s).get (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partNums.get? n = none ↔ none = none

Tactic:
simp [partNums, s_nth_eq]

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

Goal state before:
pp: case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partNums.get? n = none ↔ some val✝ = none

Tactic:
simp [partNums, s_nth_eq]

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
gp : Pair α
s_nth_eq : g.s.get? n = some gp
⊢ g.partNums.get? n = some gp.a

Tactic:
simp [partNums, s_nth_eq]

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

Goal state before:
pp: α : Type u
⊢ nil.toList ⋯ = []

Tactic:
by
  ext; simp [nil, toList, const]

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

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, (pure a).Results a m → ((pure a).bind f).Results b (n + m)

pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)

Tactic:
· intro _ h1
    rw [ret_bind]
    rw [h1.len_unique (results_pure _)]
    exact h2

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ (s : Computation α),
    (∀ {m : ℕ}, s.Results a m → (s.bind f).Results b (n + m)) →
      ∀ {m : ℕ}, s.think.Results a m → (s.think.bind f).Results b (n + m)
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.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)

Tactic:
refine (contsAux_stable_step_of_terminated ?_).trans hk

Goal state after:
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)
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
⊢ (g.contsAux (n + 1)).a * (g.contsAux (n + 1 + 1)).b - (g.contsAux (n + 1)).b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
let conts := contsAux g (n + 2)

Goal state after:
case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
⊢ (g.contsAux (n + 1)).a * (g.contsAux (n + 1 + 1)).b - (g.contsAux (n + 1)).b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -(some gp.a).getD 0

Tactic:
Option.getD_some

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
b : β
k : ℕ
⊢ (s.bind f).Results b k → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ k = n + m

Tactic:
induction k generalizing s with | zero | succ n IH <;>
  induction s using recOn with intro h | pure a | think s'

Goal state after:
case zero.pure
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ a_1 m n, (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m

case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m

case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s).s.get? i = some gp
⊢ -(some 1).getD 0 = -1

Tactic:
Option.getD_some

Goal state after:
K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s).s.get? i = some gp
⊢ -1 = -1