mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯).op))
      (x g₁ hg₁) =
    (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
conv_rhs => rw [eq₂]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯).op))
      (x g₁ hg₁) =
    (ConcreteCategory.hom (ℱ.obj.map ((c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯).op))
      (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
hd' : IsLimit d' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.Y' i)) (fun i ↦ (d.inj i).op) (Cofan.IsColimit.op hd)
⊢ (Iso.refl c'.pt).hom ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op =
    (E.multicospanIndex F).sndPiMapOfIsLimit c' hd' ≫ (Iso.refl d'.pt).hom

Tactic:
refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
    simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
    rw [MulticospanIndex.sndPiMapOfIsLimit_proj]
    simp [c', d', ← F.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve (G.obj U✝)
hS : S✝ ∈ K (G.obj U✝)
⊢ Sieve.functorPullback G S✝ ∈ (G.restrictedTopology K) U✝

Tactic:
apply G.mem_restrictedTopology_of_functorPushforward_mem

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve (G.obj U✝)
hS : S✝ ∈ K (G.obj U✝)
⊢ Sieve.functorPushforward G (Sieve.functorPullback G S✝) ∈ K (G.obj U✝)
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf K (e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
replace hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F) :=
      e.functor.op_comp_isSheaf _ _ ⟨_, hP'⟩

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝³ : IsDenseSubsite K J e.inverse
A : Type u_1
inst✝² : Category.{v_1, u_1} A
B : Type u_2
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
inst✝ : K.HasSheafCompose F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
hP' : Presheaf.IsSheaf J (e.functor.op ⋙ e.inverse.op ⋙ P ⋙ F)
⊢ Presheaf.IsSheaf J (P ⋙ F)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
⊢ ∀ (E_1 : Multifork (E.multicospanIndex F.obj)) (m : E_1.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = E_1.ι i) → m = multiforkLift E_1

Tactic:
intro c m hm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
hm : ∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i
⊢ m = multiforkLift c
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
⊢ g₁' ≫ g₁ = g₂' ≫ g₂

Tactic:
ext; exact h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : S ∈ (K.over (F.obj X)) ((Over.post F).obj U)
⊢ Sieve.functorPullback (Over.post F) S ∈ (J.over X) U

Tactic:
rw [GrothendieckTopology.mem_over_iff] at hS ⊢
    rw [Sieve.overEquiv_functorPullback_post]
    exact F.cover_lift J K hS

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ { toFun := Sieve.functorPushforward (Over.forget X), invFun := Sieve.functorPullback (Over.forget X), left_inv := ⋯,
        right_inv := ⋯, map_rel_iff' := ⋯ }
      (Sieve.generate R) ∈
    K.toGrothendieck Y.left

Tactic:
RelIso.coe_fn_mk,

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : Presieve.map (Over.forget X) R ∈ K.coverings ((Over.forget X).obj Y)
⊢ { toFun := Sieve.functorPushforward (Over.forget X), invFun := Sieve.functorPullback (Over.forget X), left_inv := ⋯,
        right_inv := ⋯ }
      (Sieve.generate R) ∈
    K.toGrothendieck Y.left
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
⊢ c.pt ∈ upperBounds (Set.range F.obj)

Tactic:
by
  intro x ⟨i, p⟩; rw [← p]; exact (c.ι.app i).le

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (diagramIsoPair F)

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

Goal state before:
pp: case refine_1
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
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj ≅
    ((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

Tactic:
refine NatIso.ofComponents (fun U ↦ ?_) ?_

Goal state after:
case refine_1.refine_1
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
U : Cᵒᵖ
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.obj U ≅
    ((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.obj
      U

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 ≫ Iso.hom ?refine_1.refine_1 =
      Iso.hom ?refine_1.refine_1 ≫
        ((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
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y Z : D
g : Z ⟶ Y
i : P.I
v : G.obj Z ⟶ P.X i
⊢ (Sieve.ofObjects (fun i ↦ i.fst) Y).arrows g

Tactic:
exact ⟨⟨Z, i, v⟩, ⟨𝟙 _⟩⟩

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

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

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

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

Goal state before:
pp: case a.mul_1
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝¹ y✝ x x' y : Prequotient F
x✝ : Relation F x x'
h : descFunLift F s x = descFunLift F s x'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x'.mul y)

Tactic:
exact congr_arg (· * _) h

Goal state after:
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'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)

Tactic:
rw [comp_id]

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'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
⊢ Nonempty (Cocone F)

Tactic:
have := ((Arrow.finite_iff A).1 hA).some

Goal state after:
case mpr
J : Type u
inst✝¹ : Category.{v, u} J
a✝ : IsFiltered J
A : Type w
inst✝ : SmallCategory A
F : A ⥤ J
hA : Finite (Arrow A)
this : FinCategory A
⊢ Nonempty (Cocone F)
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : Algebra R S
inst✝⁶ : Module R M₁
inst✝⁵ : Module S M₁
inst✝⁴ : IsScalarTower R S M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module S M₂
inst✝ : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ ∀ (x y : (M₁ × M₂) ⊗[R] M₃),
    (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
              (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
          (c • x) =
        c •
          (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            x →
      (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            (c • y) =
          c •
            (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                  (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
              y →
        (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
            (c • (x + y)) =
          c •
            (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
                  (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
              (x + y)

Tactic:
simp_all

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

Goal state before:
pp: case add
R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x✝ y✝ : ↑S ⊗[↑R] ((i : ι) → ↑(P i).right)
a✝¹ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      x✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((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)))
      x✝
a✝ :
  (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      y✝ =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((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)))
      y✝
⊢ (ConcreteCategory.hom
        (Under.Hom.right
          (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (Pi.evalAlgHom (↑R) (fun j ↦ ↑(P j).right) i)).toUnder))
      (x✝ + y✝) =
    (ConcreteCategory.hom
        (Under.Hom.right
          ((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)))
      (x✝ + y✝)

Tactic:
simp_all

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

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

Tactic:
rcases (hp.coprime_iff_not_dvd.mpr h).isCoprime with ⟨a, b, hab⟩

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

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

Tactic:
push_cast at hab

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p
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✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f).ker = ((AlgebraTensorModule.lTensor S M) f.ker.subtype).range

Tactic:
by
  rw [← LinearMap.exact_iff]
  exact Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case zero
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
⊢ ↑((tensorKer S M f) 0) = (lTensor M f.ker.subtype) 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul
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
x✝ : M
y✝ : ↥f.ker
⊢ ↑((tensorKer S M f) (x✝ ⊗ₜ[R] y✝)) = (lTensor M f.ker.subtype) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case add
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
x✝ y✝ : M ⊗[R] ↥f.ker
a✝¹ : ↑((tensorKer S M f) x✝) = (lTensor M f.ker.subtype) x✝
a✝ : ↑((tensorKer S M f) y✝) = (lTensor M f.ker.subtype) y✝
⊢ ↑((tensorKer S M f) (x✝ + y✝)) = (lTensor M f.ker.subtype) (x✝ + y✝)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case zero
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 g : N →ₗ[R] P
⊢ ↑((tensorEqLocus S M f g) 0) = (lTensor M (f.eqLocus g).subtype) 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul
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 g : N →ₗ[R] P
x✝ : M
y✝ : ↥(f.eqLocus g)
⊢ ↑((tensorEqLocus S M f g) (x✝ ⊗ₜ[R] y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case add
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 g : N →ₗ[R] P
x✝ y✝ : M ⊗[R] ↥(f.eqLocus g)
a✝¹ : ↑((tensorEqLocus S M f g) x✝) = (lTensor M (f.eqLocus g).subtype) x✝
a✝ : ↑((tensorEqLocus S M f g) y✝) = (lTensor M (f.eqLocus g).subtype) y✝
⊢ ↑((tensorEqLocus S M f g) (x✝ + y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ + y✝)

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
h : n.Coprime p
⊢ ↑(n.gcdA p) * ↑n = 1

Tactic:
CharP.natCast_gcdA_mul_intCast_eq_gcd,

Goal state after:
R : Type u_1
K : Type u_2
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
h : n.Coprime p
⊢ ↑(n.gcd p) = 1