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

Goal state before:
pp: case refine_1.refine_2
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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.map f ≫
        ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to Y))) (RingCat.Hom.hom (φ.hom.app Y))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).hom =
      ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to X_1))) (RingCat.Hom.hom (φ.hom.app X_1))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).hom ≫
        ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
                    sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                      F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
                M).obj.map
          f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_2
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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
⊢ ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y),
    (pushforward φ ⋙ forgetToSheafModuleCat S X hX).map f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj U))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj U))
              ⋯)).hom ≫
        (forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
              sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).map
          f

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
⊢ ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
    (cocone U).op.π.app j =
      (Iso.refl (cocone U).op.pt).hom ≫
        ((Cone.postcomposeEquivalence (NatIso.op (pairwiseDiagramIso U))).functor.obj
                (Cone.whisker (pairwiseToOpensLeCover U).op (opensLeCoverCocone U).op)).π.app
          j

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Tannaka

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    ObjectProperty.homMk
        { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) (x * y)), naturality := ⋯ } =
      ObjectProperty.homMk { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) x), naturality := ⋯ } *
        ObjectProperty.homMk { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) y), naturality := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Tannaka

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ∀ (x y : R),
    ObjectProperty.homMk
        { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) (x + y)), naturality := ⋯ } =
      ObjectProperty.homMk { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) x), naturality := ⋯ } +
        ObjectProperty.homMk { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) y), naturality := ⋯ }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughProjectives C
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
x✝ : Epi f
⊢ Epi (G.map f)

Tactic:
suffices ∃ h, h ≫ G.map f = Projective.π (G.obj Y) from epi_of_epi_fac this.choose_spec
    refine ⟨adj.unit.app (Projective.over (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π _) ≫ adj.counit.app Y) f), ?_⟩
    rw [Category.assoc, ← Functor.map_comp]
    simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
x : ULift.{u_1, v} ↑S.X₂
⊢ ULift.moduleEquiv x ∈ Set.range ⇑(ConcreteCategory.hom S.f) ↔
    ∃ y, (Hom.hom S.f) (ULift.moduleEquiv y) = ULift.moduleEquiv x

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: M N : AddCommMonCat
f : M ⟶ N
⊢ Finsupp.liftAddHom.symm
      (Hom.hom ((forget AddCommMonCat ⋙ free).map f ≫ ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑N)))) =
    Finsupp.liftAddHom.symm (Hom.hom (ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑M)) ≫ (𝟭 AddCommMonCat).map f))

Tactic:
cat_disch

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible

Tactic:
rintro ⟨M, rfl⟩
    simp

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible

Tactic:
rintro ⟨M, rfl⟩
    simp

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
⊢ (Iso.refl (of ↑S)).hom ≫ (pushoutCocone ↑R ↑S ↑S).inl =
    (pushoutCocone ↑R ↑S ↑S).inl ≫ (Iso.refl (pushoutCocone ↑R ↑S ↑S).pt).hom

Tactic:
cat_disch

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
⊢ (Iso.refl (of ↑S)).hom ≫ (pushoutCocone ↑R ↑S ↑S).inr =
    (pushoutCocone ↑R ↑S ↑S).inr ≫ (Iso.refl (pushoutCocone ↑R ↑S ↑S).pt).hom

Tactic:
cat_disch

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

Goal state before:
pp: 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₂
h₁ : ¬f.IsInvertible
this : ¬IsUnit (↑e.symm ∘SL f)
⊢ f.inverse = (↑e.symm ∘SL f)⁻¹ʳ ∘SL ↑e.symm

Tactic:
simp [this, h₁]

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
fork : Fork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr := Fork.ofι (ofHom (algebraMap ↑R ↑S)) ⋯
isPushout : IsPushout (ofHom (algebraMap ↑R ↑S)) (ofHom (algebraMap ↑R ↑S)) (pushoutCocone ↑R ↑S ↑S).inl
  (pushoutCocone ↑R ↑S ↑S).inr :=
  { w := PushoutCocone.condition (pushoutCocone ↑R ↑S ↑S),
    isColimit' := Nonempty.intro (pushoutCoconeIsColimit ↑R ↑S ↑S) }
⊢ (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone ↑R ↑S) ⋯).toCommRingCatIso.hom ≫
      (equalizerFork (pushoutCocone ↑R ↑S ↑S).inl (pushoutCocone ↑R ↑S ↑S).inr).ι =
    fork.ι ≫ (Iso.refl (of ↑S)).hom

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : X ≅ Y
x : ↑X.toModuleCat
⊢ (Hom.hom e.inv) ((↑(Hom.hom e.hom)).toFun x) = x

Tactic:
cat_disch

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : X ≅ Y
x : ↑Y.toModuleCat
⊢ (↑(Hom.hom e.hom)).toFun ((Hom.hom e.inv) x) = x

Tactic:
cat_disch

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

Goal state before:
pp: A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
⊢ Nontrivial ↑D

Tactic:
let : Field A := hA.toField
  algebraize [f.hom, g.hom]
  let e : D ≅ .of (B ⊗[A] C) :=
    IsColimit.coconePointUniqueUpToIso h.isColimit (CommRingCat.pushoutCoconeIsColimit A B C)
  let e' : D ≃ B ⊗[A] C := e.commRingCatIsoToRingEquiv.toEquiv
  exact e'.nontrivial

Goal state after:
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
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := ⋯
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom ↑π) = CommRingCat.Hom.hom f

Tactic:
exact π.comp_algebraMap

Goal state after:
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
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ z₁ = i₂ (f₁ d) + i₂ y₂
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
← hz₂,

Goal state after:
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
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₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ z₁ = i₂ (f₁ d) + g₁ z₂
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.left } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.left }

Tactic:
cat_disch

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

Goal state before:
pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app { as := WalkingPair.right } =
    (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app { as := WalkingPair.right }

Tactic:
cat_disch

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

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.left } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.left }

Tactic:
cat_disch

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

Goal state before:
pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app { as := WalkingPair.right } ≫
      Under.homMk a.hom ⋯ =
    (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app { as := WalkingPair.right }

Tactic:
cat_disch

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
J : Type w
F : Discrete J ⥤ Over B
c : Cone (widePullbackDiagramOfDiagramOver B F)
x✝² x✝¹ : Discrete J
X Y : J
x✝ : { as := X } ⟶ { as := Y }
f : X = Y
⊢ 𝟙 (mk (c.π.app none)) ≫ homMk (c.π.app (some Y)) ⋯ = homMk (c.π.app (some X)) ⋯ ≫ F.map { down := { down := f } }

Tactic:
cat_disch

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

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.IsClosedUnderFiniteProducts

Tactic:
by
  refine .of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
  let e : A ≅ CommRingCat.mkUnder R (Π i, pres.diag.obj ⟨i⟩) :=
    (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
      HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso <| by simp) ≪≫
      limit.isoLimitCone ⟨CommRingCat.Under.piFan <| fun i ↦ (pres.diag.obj ⟨i⟩),
        CommRingCat.Under.piFanIsLimit <| fun i ↦ (pres.diag.obj ⟨i⟩)⟩
  have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
  rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]
  exact hQp _ fun i ↦ hpres _

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

Goal state before:
pp: case none
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)
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app none =
    { 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 none

Tactic:
cat_disch

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

Goal state before:
pp: case some
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 : J
⊢ ((𝟭 (Cone (widePullbackDiagramOfDiagramOver B F))).obj x✝).π.app (some 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 (some j)

Tactic:
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.RespectsIso
X Y : T
f g : X ⟶ Y
hfg : f = g
hf : P f
⊢ P g

Tactic:
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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ fg ≫ 𝟙 Z = f ≫ g

Tactic:
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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : X ⟶ Z
hfg : f ≫ g = fg
A : P.Over Q Z
⊢ fg = f ≫ g

Tactic:
cat_disch

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
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
⊢ False

Tactic:
have r_dvd_a := (ringChar.spec K a).1 a_cast_zero

Goal state after:
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
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
g : ↑a ∈ IsLocalRing.maximalIdeal R
a_cast_zero : ↑a = 0
r_dvd_a : ringChar K ∣ a
⊢ False
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)

Tactic:
· let y : E := ⟨x, h hx⟩
    exact (mem_lift y).2 ((mem_restrict h y).2 hx)

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ corec' (Corec.f f) o (n + 1) = none → corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o (n + 1) = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'

Tactic:
rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
    exact IH (Corec.f f o).2

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι), Function.Injective ⇑(g i)
⊢ Function.Injective ⇑(lift G f P g Hg)

Tactic:
injective_iff_map_eq_zero

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
⊢ ∀ (a : DirectLimit G f), (lift G f P g Hg) a = 0 → a = 0