mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ η ≫ f ▷ Z = η

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ η ≫ f ▷ Z = η
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ f ▷ Z = (f ▷ Z ⊗ₘ f ▷ Z) ≫ μ

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : MonoidalCategory C
M N O X✝ : C
inst✝⁸ : MonObj M
inst✝⁷ : MonObj N
inst✝⁶ : MonObj O
inst✝⁵ : BraidedCategory C
X Y Z W : C
inst✝⁴ : MonObj X
inst✝³ : MonObj Y
inst✝² : MonObj Z
inst✝¹ : MonObj W
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ f ▷ Z = (f ▷ Z ⊗ₘ f ▷ Z) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Mon C
f : F.mapMon.obj X ⟶ F.mapMon.obj Y
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ F.map (η ≫ g) = F.map η

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Mon C
f : F.mapMon.obj X ⟶ F.mapMon.obj Y
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ F.map η ≫ F.map g = F.map η
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Mon C
f : F.mapMon.obj X ⟶ F.mapMon.obj Y
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ F.map (μ ≫ g) = F.map ((g ⊗ₘ g) ≫ μ)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : Mon C
f : F.mapMon.obj X ⟶ F.mapMon.obj Y
g : X.X ⟶ Y.X
hg : F.map g = f.hom
⊢ F.map μ ≫ F.map g = F.map (g ⊗ₘ g) ≫ F.map μ
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.fst = l₁ ≫ t₁.fst

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.fst = s.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ (m ≫ t₁.snd) ≫ t₂.snd = (l₁ ≫ t₁.snd) ≫ t₂.snd

Tactic:
simpa using

Goal state after:
case h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.snd ≫ t₂.snd = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1.h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ (l ≫ t₁.snd) ≫ t₂.snd = s.snd ≫ t₂.snd

Tactic:
simpa using

Goal state after:
case refine_1.h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ l ≫ t₁.snd ≫ t₂.snd = s.snd ≫ t₂.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.fst = prod.lift s.fst (s.snd ≫ prod.snd) ≫ prod.fst

Tactic:
simpa using

Goal state after:
case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.fst = s.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m ≫ (t₂.pasteHoriz t₁ hi₂).fst = l ≫ (t₂.pasteHoriz t₁ hi₂).fst

Tactic:
simpa using

Goal state after:
case refine_2.h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ s.fst = l ≫ t₁.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m ≫ (t₂.pasteHoriz t₁ hi₂).snd = l ≫ (t₂.pasteHoriz t₁ hi₂).snd

Tactic:
simpa using

Goal state after:
case refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
m : s.pt ⟶ t₁.pt
hm₁ : m ≫ t₁.fst = s.fst
hm₂ : m ≫ t₁.snd = s.snd
⊢ m ≫ t₁.snd ≫ t₂.snd = l ≫ t₁.snd ≫ t₂.snd
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap A T)
⊢ algebraMapSubmonoid T (algebraMapSubmonoid A (IsUnit.submonoid R)) ≤ IsUnit.submonoid T

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
T : Type u_5
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra A T
inst✝ : IsScalarTower R A T
H : Function.Bijective ⇑(algebraMap A T)
⊢ algebraMapSubmonoid T (IsUnit.submonoid R) ≤ IsUnit.submonoid T
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' :=
  LinearEquiv.restrictScalars R (LocalizedModule.equivTensorProduct S M).symm ≪≫ₗ IsLocalizedModule.iso S f
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' :=
  finsuppRight R R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
a : α
m : M
⊢ ((↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a) m =
    ((mk R (Localization S) (α →₀ M)) 1 ∘ₗ Finsupp.lsingle a) m

Tactic:
apply (finsuppRight R R (Localization S) M α).injective

Goal state after:
R : Type u_1
inst✝¹⁸ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁷ : CommSemiring A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : IsLocalization S A
M : Type u_3
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
M' : Type u_4
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : Module A M'
inst✝⁹ : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
α : Type u_7
inst✝ : IsLocalizedModule S f
e : Localization S ⊗[R] M ≃ₗ[R] M' := ⋯
e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] α →₀ M' := ⋯
a : α
m : M
⊢ (finsuppRight R R (Localization S) M α) (((↑e'.symm ∘ₗ Finsupp.mapRange.linearMap f) ∘ₗ Finsupp.lsingle a) m) =
    (finsuppRight R R (Localization S) M α) (((mk R (Localization S) (α →₀ M)) 1 ∘ₗ Finsupp.lsingle a) m)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inr ≫ m = t₂.inr ≫ l₂

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
l₁ : t₁.pt ⟶ s.pt
hl₁ : t₁.inl ≫ l₁ = s.inl
hl₁' : t₁.inr ≫ l₁ = f₂ ≫ s.inr
l₂ : t₂.pt ⟶ s.pt
hl₂ : t₂.inl ≫ l₂ = l₁
hl₂' : t₂.inr ≫ l₂ = s.inr
m : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hm₁ : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = s.inl
hm₂ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = s.inr
⊢ t₂.inr ≫ m = s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inl ≫ m = coprod.inl ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
simpa using

Goal state after:
case refine_3.h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inl ≫ m = s.inr
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x : LocalizedModule S M
f : M × ↥S → α
wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'
⊢ ∀ (a b : M × ↥S), a ≈ b → f a = f b

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x : LocalizedModule S M
f : M × ↥S → α
wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'
⊢ ∀ (a b : M × ↥S), a ≈ b → f a = f b
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x y : LocalizedModule S M
f : M × ↥S → M × ↥S → α
wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
⊢ ∀ (a₁ b₁ a₂ b₂ : M × ↥S), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂

Tactic:
simpa using

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
α : Type u_3
x y : LocalizedModule S M
f : M × ↥S → M × ↥S → α
wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
⊢ ∀ (a₁ b₁ a₂ b₂ : M × ↥S), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l

Tactic:
simpa using

Goal state after:
case refine_2.h₀
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ t₁.inl ≫ t₂.inl ≫ m = t₁.inl ≫ t₂.inl ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l

Tactic:
simpa using

Goal state after:
case refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ t₂.inr ≫ m = t₂.inr ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : F.Faithful
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : F.Faithful
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : F.Faithful
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : F.Faithful
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
X : C
⊢ (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
X : C
⊢ f₁.app X ≫ f₃.app X = f₂.app X ≫ f₄.app X
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
X : C
⊢ (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F₁ F₂ F₃ F₄ : C ⥤ D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
X : C
⊢ f₁.app X ≫ f₃.app X = f₂.app X ≫ f₄.app X
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ ((Over.forget X).mapIso e).hom ≫ pullback.fst f g = p ≫ (Iso.refl X).hom

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullbacksAlong g
P : C
p : P ⟶ X
e : Over.mk p ≅ Over.mk (pullback.fst f g)
⊢ Over.Hom.left e.hom ≫ pullback.fst f g = p
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) = IsLocalization.mk' T ?m.144 ?m.145 • ?m.147

Tactic:
IsLocalization.mk'_sec (M := S) T

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • mk (t • m + s • n) (s * t) = ?m.167 • ?m.147

R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ T
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
this : X.coeff 1 = (C w).coeff 1
⊢ 1 = 0

Tactic:
rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z Z' : C
f : X ⟶ Z
g : Y ⟶ Z'
i : Z ⟶ Z'
inst✝¹ : IsIso i
inst✝ : HasPullback (f ≫ i) g
⊢ HasPullback f (g ≫ inv i)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z Z' : C
f : X ⟶ Z
g : Y ⟶ Z'
i : Z ⟶ Z'
inst✝¹ : IsIso i
inst✝ : HasPullback (f ≫ i) g
⊢ HasPullback f (g ≫ inv i)