mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ K.W (G.op.whiskerLeft f) ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
← Presheaf.isLocallyInjective_whisker_iff K J G f hG,

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
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
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ K.W (G.op.whiskerLeft f) ↔ Presheaf.IsLocallyInjective K (G.op.whiskerLeft f) ∧ Presheaf.IsLocallySurjective J f
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Z : C
f : Z ⟶ X
i : I
φ : Z ⟶ Y i
⊢ x.familyOfElements X f ⋯ = (ConcreteCategory.hom (F.map φ.op)) (x i)

Tactic:
by
  apply hx

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

Goal state before:
pp: case hex
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)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map (φ ≫ f).op)) (s Y₁)

Tactic:
op_comp,

Goal state after:
case hex
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)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map (f.op ≫ φ.op))) (s Y₁)
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₁ ⋯
⊢ f₂ ≫ Y₂.hom = W'.hom

Tactic:
by simpa using! h.symm =≫ Z.hom

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝ : Set (Opens ↑Y)
⊢ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝), is_open' := ⋯ } =
    sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝)

Tactic:
by ext; simp

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

Goal state before:
pp: case e'_2.pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Tactic:
· exact (hs <| op <| Pairwise.Hom.left i j).symm

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

Goal state before:
pp: case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t = (ConcreteCategory.hom (F.obj.map (i₁ x).op)) t

Tactic:
Subsingleton.elim (i₁ x) (i₂ x)

Goal state after:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t = (ConcreteCategory.hom (F.obj.map (i₂ x).op)) t
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_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ) inst✝⁵
module : moduleTopology R (A ⧸ S) = TopologicalSpace.coinduced (⇑S.mkQ) inferInstance
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)

Tactic:
rw [quot, module]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
f : M₁ →L[R] S
⊢ f.smulRight 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
x : M₂
⊢ smulRight 0 x = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

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₁
inst✝ : ContinuousSMul R₁ M₁
⊢ toSpanSingleton R₁ 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ x✝ : U →L[R] V
⊢ lcomp W (x✝¹ + x✝) = lcomp W x✝¹ + lcomp W x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝¹ : R
x✝ : U →L[R] V
⊢ lcomp W (x✝¹ • x✝) = (RingHom.id R) x✝¹ • lcomp W x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousAdd M
inst✝² : ContinuousConstSMul S M
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M
f : R →L[R] M
⊢ toSpanSingleton R ((fun f ↦ f 1) f) = f

Tactic:
by ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom) = MulHom.id ↑X

Tactic:
by ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
⊢ (MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
by ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) = MulHom.id ↑X

Tactic:
by ext; simp

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
⊢ (Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
by ext; simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ e.trans (α • f) = α • e.trans f

Tactic:
by ext; simp

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.IsCardinalAccessible κ
inst✝ : G.IsCardinalAccessible κ
this✝ : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
this : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J G
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:
(Tactic.exact
 "exact"
 (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: case e_n
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ∑ a, Pi.single a (m a) = m

Tactic:
ext j

Goal state after:
case e_n
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
j : ι
⊢ (∑ a, Pi.single a (m a)) j = m j
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
⊢ Pi.single i (x ⊗ₜ[R] m) = fun j ↦ x ⊗ₜ[R] Pi.single i m j

Tactic:
ext j

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
m : M i
j : ι
⊢ Pi.single i (x ⊗ₜ[R] m) j = x ⊗ₜ[R] Pi.single i m j
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) = fun j ↦ f j • x

Tactic:
ext j

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
j : ι
⊢ (piScalarRightHom R S N ι) (x ⊗ₜ[R] f) j = f j • x
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ piScalarRightHom R S N ι ∘ₗ piScalarRightInv R S N ι = LinearMap.id

Tactic:
by ext i x j; simp [Pi.single_apply]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

Tactic:
ext j

Goal state after:
case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
j : ι
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) j =
    ((piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)) j
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 : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
        X).fst =
    (Over.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.left)
          ⋯).hom ≫
      ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).fst

Tactic:
by ext; simp

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 : C
f : Y ⟶ X✝
g : Z ⟶ X✝
X : BinaryFan (Over.mk f) (Over.mk g)
⊢ (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
        X).snd =
    (Over.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.left)
          ⋯).hom ≫
      ((𝟭 (BinaryFan (Over.mk f) (Over.mk g))).obj X).snd

Tactic:
by ext; simp

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 : C
f✝ : X ⟶ Y
g : X ⟶ Z
X✝ Y✝ : PushoutCocone f✝ g
f : X✝ ⟶ Y✝
⊢ (𝟭 (PushoutCocone f✝ g)).map f ≫ Y✝.eta.hom =
    X✝.eta.hom ≫
      ({ obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
by ext; simp

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 : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).inl ≫
      (Under.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.right)
          ⋯).hom =
    ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inl

Tactic:
by ext; simp

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 : C
f : X✝ ⟶ Y
g : X✝ ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
          X).inr ≫
      (Under.isoMk
          (Iso.refl
            (({ obj := fun c ↦ PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂} a ↦ { hom := Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                      { obj := fun c ↦ BinaryCofan.mk (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂} a ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                  X).pt.right)
          ⋯).hom =
    ((𝟭 (BinaryCofan (Under.mk f) (Under.mk g))).obj X).inr

Tactic:
by ext; simp

Goal state after: