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

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
⊢ ∀ (f : G.obj W ⟶ X),
    (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)) =
      (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂))

Tactic:
i

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
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₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
⊢ (ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁)) =
    (ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂))
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
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i'✝ j✝ j'✝ : E.I₀
hii'✝ : i✝ = i'✝
hjj'✝ : j✝ = j'✝
i i' j j' : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ F.Y (u₁ i' j' ((congrIndexOneOfEq hii' hjj') k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))

Tactic:
subst hii' hjj'; simp [congrIndexOneOfEq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.leftOp

Tactic:
by
    apply +allowSynthFailures createsLimitsOfShapeLeftOp
    exact createsColimitsOfShapeOfEquiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f →
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)

Tactic:
· rintro h _ ⟨R, rfl⟩
    exact (h₂ R).2 (h _ ⟨R, rfl⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
⊢ ∀ (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
i

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
i : I
⊢ ∀ (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) = (ConcreteCategory.hom (P.map Z₂.hom)) (↑t Z₂.left)

Tactic:
← t.property φ.left

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
Y : D
Z₁ Z₂ : CostructuredArrow F Y
φ : Z₁ ⟶ Z₂
⊢ (ConcreteCategory.hom (P.map Z₁.hom)) (↑t Z₁.left) =
    (ConcreteCategory.hom (P.map Z₂.hom)) ((ConcreteCategory.hom ((F ⋙ P).map φ.left)) (↑t Z₁.left))
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Simple (of R M) ↔ IsSimpleModule R M

Tactic:
by
  rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (ψ.hom.app U)

Tactic:
subst e; rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X : SheafOfModules R
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((forget S).obj ((pushforward φ).obj X)).map x✝ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map x✝))).map
        ((ModuleCat.restrictScalarsCongr ⋯).app
            (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝¹)).hom =
    ((ModuleCat.restrictScalarsCongr ⋯).app
          (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝²)).hom ≫
      ((forget S).obj ((pushforward ψ).obj X)).map x✝

Tactic:
subst e; rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ✝ φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
e : φ = ψ
X✝ Y✝ : SheafOfModules R
x✝ : X✝ ⟶ Y✝
⊢ (pushforward φ).map x✝ ≫
      ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y✝.val).obj U))
            ⋯)).hom =
    ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X✝.val).obj U))
            ⋯)).hom ≫
      (pushforward ψ).map x✝

Tactic:
subst e; rfl

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = Finset.univ.sup f

Tactic:
by
  trans
  · exact
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
          (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq
  change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f
  simp only [← Finset.sup_map, Finset.univ_map_equiv_to_embedding]
  rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f g : X ⟶ Y
h : f = g
ℱ : Presheaf C X
U : (Opens ↑Y)ᵒᵖ
⊢ (pushforwardEq h ℱ).hom.app U = ℱ.map (eqToHom ⋯)

Tactic:
by
  simp [pushforwardEq]

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
⊢ (V ⟶ hf.functor.obj U) → (c' : Opens ↑X) × (hf.functor.obj c' ≅ V)

Tactic:
i

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ hf.functor.obj U
⊢ (c' : Opens ↑X) × (hf.functor.obj c' ≅ V)
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
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫ F.map (unop j).obj.hom.op =
    F.map ((opensLeCoverCocone U).ι.app ((generateEquivalenceOpensLe_functor' U).obj (unop j))).op

Tactic:
← F.map_comp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯ ≫ (unop j).obj.hom.op) =
    F.map ((opensLeCoverCocone U).ι.app ((generateEquivalenceOpensLe_functor' U).obj (unop j))).op
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
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯) ≫ F.map ((opensLeCoverCocone U).ι.app ((generateEquivalenceOpensLe_functor' U).obj (unop j))).op =
    F.map (unop j).obj.hom.op

Tactic:
← F.map_comp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
j : (ObjectProperty.FullSubcategory fun f ↦ (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)ᵒᵖ
⊢ F.map (eqToHom ⋯ ≫ ((opensLeCoverCocone U).ι.app ((generateEquivalenceOpensLe_functor' U).obj (unop j))).op) =
    F.map (unop j).obj.hom.op
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₂

Tactic:
by
    induction U with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
⊢ ∀ (f : U ⟶ V),
    (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).map f ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩) ≫
        ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).map f

Tactic:
i

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U V : (OpenNhds y)ᵒᵖ
i : U ⟶ V
⊢ (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).map i ≫
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop V), ⋯⟩) =
    colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop U), ⋯⟩) ≫
      ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).map i
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
⊢ (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty

Tactic:
rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ (U ∩ ↑(⨆ i, map (LinearMap.single R M i) (s i))).Nonempty
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
ι : Type u_4
φ : ι → Type u_5
inst✝⁴ : (i : ι) → TopologicalSpace (φ i)
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
L : ((i : ι) → φ i) →L[R] M
v : (i : ι) → φ i
⊢ ∑ i, (L ∘SL single R φ i) (v i) = L v

Tactic:
by
  simp [← map_sum, LinearMap.sum_single_apply]

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

Goal state before:
pp: case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a

pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))

Tactic:
· intro H
    have := H.1 (CommRingCat.ofHom <| Algebra.TensorProduct.includeLeftRingHom)
      (CommRingCat.ofHom <| (Algebra.TensorProduct.includeRight (R := R) (A := S)).toRingHom)
      (by ext r; change algebraMap R S r ⊗ₜ 1 = 1 ⊗ₜ algebraMap R S r;
          simp only [Algebra.algebraMap_eq_smul_one, smul_tmul])
    exact RingHom.congr_fun (congrArg Hom.hom this)

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
inst✝⁴ : Semiring R₁
M₁ : Type u_4
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R₁ M₁
inst✝ : TopologicalSpace R₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ f (x * 1) = g (x * 1)

Tactic:
by rw [← smul_eq_mul, map_smul, h, map_smul]

Goal state after:
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
h : IsFiltered J
⊢ IsColimit (((const C).obj A).mapCocone c)

Tactic:
have (j : J) : IsIso ((((const C).obj A).mapCocone c).ι.app j) := by
              dsimp
              infer_instance

Goal state after:
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
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
⊢ IsColimit (((const C).obj A).mapCocone c)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F

Tactic:
have := hA.small
  have := small_of_small_arrow.{w} A
  have := locallySmall_of_small_arrow.{w} A
  let e := (Shrink.equivalence.{w} A).trans (ShrinkHoms.equivalence.{w} (Shrink.{w} A))
  exact (Cocone.equivalenceOfReindexing e.symm (Iso.refl _)).inverse.obj
    (nonempty_cocone (κ := κ) (e.inverse ⋙ F) (by simpa)).some

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

Goal state before:
pp: case h₁
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)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := ⋯
D : MulticospanIndex J' J := ⋯
c' : Cocone D.multicospan
⊢ (CommRingCat.Hom.hom (a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ()))))).comp (CommRingCat.Hom.hom f) =
    (CommRingCat.Hom.hom (b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))).comp (CommRingCat.Hom.hom f)

Tactic:
rw [← CommRingCat.hom_comp, ← CommRingCat.hom_comp, reassoc_of% ha, reassoc_of% hb]

Goal state after:
case h₁
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)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (α.app i ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (α.app j ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
this : HasFiniteProducts (Over B)
⊢ HasFiniteLimits (Over B)

Tactic:
have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
this✝ : HasFiniteProducts (Over B)
this : HasEqualizers (Over B)
⊢ HasFiniteLimits (Over B)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
this : HasBinaryProducts (Over B)
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over B)

Tactic:
have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePullbacks C
this✝ : HasBinaryProducts (Over B)
this : HasEqualizers (Over B)
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over B)
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)
⊢ MorphismProperty.costructuredArrowObj L P Y

Tactic:
rw [MorphismProperty.costructuredArrowObj_iff]

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 Y.hom
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
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ Hom.left (Y✝.π.app { as := j }) = Hom.left (X✝.π.app { as := j })

Tactic:
← f.w ⟨j⟩

Goal state after:
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ Hom.left (Y✝.π.app { as := j }) = Hom.left (f.hom ≫ Y✝.π.app { as := j })
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
q : ℕ
h : CharP R q
⊢ CharP R p

Tactic:
exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h

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

Goal state before:
pp: case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
⊢ ExpChar R p

Tactic:
have := f.charP H p

Goal state after:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
this : CharP R p
⊢ ExpChar R p