mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
⊢ Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y →
    Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))

Tactic:
intro hS

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : (Opens ↑X)ᵒᵖ
φ ψ : ((pullback C f).obj F).obj U ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop U ≤ (Opens.map f).obj V),
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
⊢ ∀ (j : CostructuredArrow (Opens.map f).op U),
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                U).ι.app
          j ≫
        φ =
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
                U).ι.app
          j ≫
        ψ

Tactic:
rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
Z : C
f : X ⟶ Y
F : Presheaf C Y
U : (Opens ↑X)ᵒᵖ
φ ψ : ((pullback C f).obj F).obj U ⟶ Z
h :
  ∀ (V : Opens ↑Y) (hV : unop U ≤ (Opens.map f).obj V),
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
      ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ
V : Opens ↑Y
as✝ : PUnit.{1}
b : unop ((fromPUnit U).obj { as := as✝ }) ⟶ unop ((Opens.map f).op.obj (op V))
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt U).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      φ =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension F) ((Opens.map f).op.leftKanExtensionUnit F)).coconeAt
              U).ι.app
        { left := op V, right := { as := as✝ }, hom := op b } ≫
      ψ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝¹ : ContinuousAdd A
this✝ : ContinuousAdd B'
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
clear! τB

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this : ContinuousAdd A
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ) inst✝³
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : s.topologicalClosure = ⊤
⊢ (Submodule.map (↑f) s).topologicalClosure = ⊤

Tactic:
SetLike.ext'_iff

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₁ M₁
inst✝⁷ : Module R₂ M₂
inst✝⁶ : RingHomSurjective σ₁₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : TopologicalSpace R₂
inst✝³ : ContinuousSMul R₁ M₁
inst✝² : ContinuousAdd M₁
inst✝¹ : ContinuousSMul R₂ M₂
inst✝ : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
hf' : DenseRange ⇑f
s : Submodule R₁ M₁
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ f.inverse = (↑e.symm ∘SL f)⁻¹ʳ ∘SL ↑e.symm

Tactic:
← he'

Goal state after:
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (↑e.symm ∘SL ↑e')⁻¹ʳ ∘SL ↑e.symm
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsColimit (((const C).obj A).mapCocone c)

Tactic:
by
            have h := isFiltered_of_isCardinalFiltered J κ
            have (j : J) : IsIso ((((const C).obj A).mapCocone c).ι.app j) := by
              dsimp
              infer_instance
            exact Functor.IsEventuallyConstantFrom.isColimitOfIsIso
              (i₀ := h.nonempty.some) (fun _ _ ↦ by dsimp; infer_instance) _

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i : J
f g : D.obj i ⟶ X
h : c.π.app i ≫ f = c.π.app i ≫ g
j : Jᵒᵖ
a : op i ⟶ j
ha : (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map a)) f = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map a)) g
⊢ ∃ j a, D.map a ≫ f = D.map a ≫ g

Tactic:
exact ⟨j.unop, a.unop, ha⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨j, hj⟩ := h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
        hasCardinalLT_of_hasCardinalLT_arrow hA)

Goal state after:
J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (k : A), F.obj k ≤ j
⊢ Nonempty (Cocone F)
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
⊢ Exact ⇑F ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Tactic:
have H₁ : ∀ x, f₂ (σ x) = x := congr_fun hσ
  have H₂ := δ_aux i₂ i₃ f₂ g₁ g₂ hg h₂ σ hσ ρ hρ ι₃ hι₃
  intro x
  constructor
  · intro H
    obtain ⟨y, hy⟩ := (hπ₁ _).mp H
    obtain ⟨k, hk⟩ : σ (ι₃ x) - f₁ y ∈ Set.range ι₂ := by
      rw [← hι₂, map_sub, ← H₂, ← hy, sub_eq_zero]; exact congr($h₁ y)
    refine ⟨k, h ?_⟩
    rw [← ι₃.comp_apply, ← hF, f₂.comp_apply, hk, map_sub, H₁, hf.apply_apply_eq_zero, sub_zero]
  · rintro ⟨y, rfl⟩
    exact (δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ (ι₂ y) congr($hF y)
      _ (by rw [map_zero, hι₂.apply_apply_eq_zero])).trans π₁.map_zero

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

Goal state before:
pp: case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
f : ((coyoneda.obj (Opposite.op S)).mapCocone c).pt
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi

Tactic:
obtain ⟨i, g, h₁, h₂⟩ := RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit
       R (F ⋙ Under.forget R) { app i := (F.obj i).hom } S.hom ((Under.forget R).mapCocone c)
      (PreservesColimit.preserves hc).some hS f.right (by simp)

Goal state after:
case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
f : ((coyoneda.obj (Opposite.op S)).mapCocone c).pt
i : J
g : S.right ⟶ (F ⋙ Under.forget R).obj i
h₁ : S.hom ≫ g = { app := fun i ↦ (F.obj i).hom, naturality := ⋯ }.app i
h₂ : Under.Hom.right f = g ≫ ((Under.forget R).mapCocone c).ι.app i
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi
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:
by
    dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']
    apply CommRingCat.mkUnder_ext
    intro c
    induction c
    · simp only [map_zero, Under.comp_right]
    · simp only [AlgHom.toUnder_right, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        Pi.evalAlgHom_apply, Under.comp_right, comp_apply, AlgEquiv.toUnder_hom_right_apply,
        Algebra.TensorProduct.piRight_tmul]
    · simp_all

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✝³ : 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:
by
    rintro X p
    let t : IsTerminal X := (ObjectProperty.limitsOfShape_isEmpty_iff _ _ _ |>.mp p).some
    let e : X ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) := t.uniqueUpToIso CostructuredArrow.mkIdTerminal
    simpa [MorphismProperty.costructuredArrowObj_iff,
      P.costructuredArrow_iso_iff e] using P.id_mem (L.obj Y)

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

Goal state before:
pp: case some.some.id
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
c : Cone F
val✝ : J
⊢ 𝟙 c.pt.left ≫ Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) =
    Option.rec c.pt.hom (fun val ↦ Hom.left (c.π.app { as := val })) (some val✝) ≫
      WidePullbackShape.Hom.rec (motive := fun a a_1 x ↦
        some val✝ = a →
          some val✝ = a_1 →
            WidePullbackShape.Hom.id (some val✝) ≍ x →
              (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
        (fun X h ↦
          Eq.rec (motive := fun x x_1 ↦
            some val✝ = x →
              WidePullbackShape.Hom.id (some val✝) ≍ 𝟙 x →
                (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                  Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some val✝ ⟶ x) →
                  f ≍ 𝟙 (some val✝) →
                    (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝) ⟶
                      Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ 𝟙 (Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝))) ⋯
                (WidePullbackShape.Hom.id (some val✝)))
            h)
        (fun j h ↦
          Eq.rec (motive := fun x x_1 ↦
            (f : x ⟶ some val✝) →
              some val✝ = none →
                f ≍ WidePullbackShape.Hom.term j →
                  (Option.rec B (fun val ↦ (F.obj { as := val }).left) x ⟶
                    Option.rec B (fun val ↦ (F.obj { as := val }).left) (some val✝)))
            (fun f h ↦
              Eq.rec (motive := fun x x_1 ↦
                (f : some j ⟶ x) →
                  f ≍ WidePullbackShape.Hom.term j →
                    ((F.obj { as := j }).left ⟶ Option.rec B (fun val ↦ (F.obj { as := val }).left) x))
                (fun f h ↦ (F.obj { as := j }).hom) ⋯ f)
            ⋯ (WidePullbackShape.Hom.id (some val✝)))
        (WidePullbackShape.Hom.id (some val✝)) ⋯ ⋯ ⋯

Tactic:
· rw [Category.id_comp, Category.comp_id]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
F : Discrete J ⥤ Over B
x✝ : Cone (widePullbackDiagramOfDiagramOver B F)
⊢ ∀ (j : WidePullbackShape J),
    ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app j =
      { hom := 𝟙 ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).pt,
            inv := 𝟙 ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).pt, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }.hom ≫
        ((conesEquivFunctor B F ⋙ conesEquivInverse B F).obj x✝).π.app j

Tactic:
by rintro (j | j) <;> cat_disch

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
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯)

Tactic:
by
    apply Q.of_postcomp (W' := Q)
    · exact Q.pullback_fst _ _ hQf
    · simpa using Q.of_isIso _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
⊢ IsPrimePow q

Tactic:
rcases CharP.char_is_prime_or_zero K r with r_prime | r_zero

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
⊢ IsPrimePow q

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_zero : r = 0
⊢ IsPrimePow q
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ r ∣ p

Tactic:
← CharP.cast_eq_zero_iff (R ⧸ M) r p

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ ↑p = 0
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.head = Prod.fst <$> s.destruct

Tactic:
by
  unfold destruct head; cases get? s 0 <;> rfl

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

Goal state before:
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:
· assumption

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

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

Tactic:
head_map

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

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)

Tactic:
rw [← Stream'.eta (iterate f a)]

Goal state after:
α : Type u
f : α → α
a : α
⊢ (iterate f a).head :: (iterate f a).tail = a :: iterate f (f a)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive s

Tactic:
destruct_eq_pure H

Goal state after:
α : Type u
β : Type v
γ : Type w
motive : Computation α → Sort v
s : Computation α
pure : (a : α) → motive (Computation.pure a)
think : (s : Computation α) → motive s.think
v : α
H : s.destruct = Sum.inl v
⊢ motive (Computation.pure v)
Module: Mathlib.Data.Seq.Computation

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

Tactic:
by cases s'; rfl

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

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.even.tail.get n = s.tail.get (2 * n + 1)

Tactic:
tail_even,

Goal state after:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.even.get n = s.tail.get (2 * n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (∀ (h : s.Terminates), n < s.length h) ↔ ∃ a, a ∈ s.get? n

Tactic:
by
  simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
    ← Option.ne_none_iff_exists', ne_eq]
  refine ⟨?_, ?_⟩
  · intro h hn
    exact h n hn n le_rfl hn
  · intro hn _ _ k hkn hk
    exact hn <| le_stable s hkn hk

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : s.head = some p
n : ℕ
⊢ convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n)

Tactic:
by
  simp [convs'Aux, h]

Goal state after:
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 ∈ Finset.range (n + 1), -1 = (-1) ^ (n + 1)

Tactic:
by rw [Finset.prod_const, Finset.card_range]

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 : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ convs'Aux (of v).s.tail n = convs'Aux (of (fract v)⁻¹).s n

Tactic:
of_s_tail

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ convs'Aux (of (fract v)⁻¹).s n = convs'Aux (of (fract v)⁻¹).s n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_1
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ map f s, p x
x✝ : α
hx : x✝ ∈ s
⊢ (p ∘ f) x✝

pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝

Tactic:
· solve_by_elim [mem_map f hx]

Goal state after:
case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1) + fib (n + 1 + 1) - fib (n + 2)

Tactic:
add_tsub_cancel_right,

Goal state after:
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct

Tactic:
cases s <;> simp [ret]

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

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
v_eq_q

Goal state after:
case succ
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ (C P.b * X ^ 2 + C P.c * X + C P.d).leadingCoeff = P.b

Tactic:
leadingCoeff_quadratic hb

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.b = P.b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ (of v).dens n

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]
  have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
    cases n with
    | zero => exact Or.inl <| le_refl 1
    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)
  exact fib_le_of_contsAux_b this

Goal state after: