mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ map f (span R (Set.range ⇑b)) = f.range

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
⊢ span R (Set.range ⇑(ofIsLocalizedModule Rₛ S f b)) = f.range

Tactic:
by

Goal state after:
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
A : Mon C
f : trivial C ⟶ A
⊢ f = { hom := η, isMonHom_hom := ⋯ }

Tactic:
by

Goal state after:
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₁ X₂ Y₂ : Mon C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), f ⊗ₘ g = f ▷ X₂ ≫ Y₁ ◁ g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ ∀ (x y : M →ₗ[R] N),
    extendScalarsOfIsLocalization S A (x + y) =
      extendScalarsOfIsLocalization S A x + extendScalarsOfIsLocalization S A y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ ∀ (m : A) (x : M →ₗ[R] N),
    extendScalarsOfIsLocalization S A (m • x) = (RingHom.id A) m • extendScalarsOfIsLocalization S A x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ Function.LeftInverse (↑R) (extendScalarsOfIsLocalization S A)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
⊢ Function.RightInverse (↑R) (extendScalarsOfIsLocalization S A)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
f : M ≃ₗ[R] N
⊢ LinearMap.extendScalarsOfIsLocalization S A ↑f.symm ∘ₗ LinearMap.extendScalarsOfIsLocalization S A ↑f = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[R] N
⊢ (fun e ↦ restrictScalars R e) ((fun e ↦ extendScalarsOfIsLocalization S A e) e) = e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R✝ : Type u_1
Rₛ : Type u_2
R : Type u_3
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_4
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
M : Type u_5
N : Type u_6
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
e : M ≃ₗ[A] N
⊢ (fun e ↦ extendScalarsOfIsLocalization S A e) ((fun e ↦ restrictScalars R e) e) = e

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M
inst✝¹³ : Module R M'
f : M →ₗ[R] M'
inst✝¹² : IsLocalizedModule S f
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ (mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M
inst✝¹³ : Module R M'
f : M →ₗ[R] M'
inst✝¹² : IsLocalizedModule S f
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ (mapExtendScalars S g f Rₛ) ↑e.symm ∘ₗ (mapExtendScalars S f g Rₛ) ↑e = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (mk x y) = mk (f x) y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ↑R ((map S) l) =
    ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ⇑((map S) l) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ Function.Injective ⇑((map S g₁ g₂) l) ↔ Function.Injective ⇑((LocalizedModule.map S) l)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ Function.Surjective ⇑((map S g₁ g₂) l) ↔ Function.Surjective ⇑((LocalizedModule.map S) l)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_4
N' : Type u_5
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ Function.Bijective ⇑((map S g₁ g₂) l) ↔ Function.Bijective ⇑((LocalizedModule.map S) l)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : SymmetricCategory C
X Y : C
inst✝¹ : MonObj X
inst✝ : MonObj Y
⊢ μ ≫ (β_ X Y).hom = ((β_ X Y).hom ⊗ₘ (β_ X Y).hom) ≫ μ

Tactic:
by

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ (ε F ≫ F.map η) ▷ F.obj X ≫ «μ» F X X ≫ F.map μ = (λ_ (F.obj X)).hom

Tactic:
by

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ F.obj X ◁ (ε F ≫ F.map η) ≫ «μ» F X X ≫ F.map μ = (ρ_ (F.obj X)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
⊢ m = hc.lift (PullbackCone.mk (s.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.right }) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

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 : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (PullbackCone.mk h k ⋯)
⊢ IsLimit (BinaryFan.mk h k)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

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 : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsTerminal Z
H₂ : IsLimit (BinaryFan.mk h k)
⊢ IsLimit (PullbackCone.mk h k ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit (F.mapCone (limitConeOfTerminalAndPullbacks K).cone)

Tactic:
by

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ («μ» F X X ≫ F.map μ) ▷ F.obj X ≫ «μ» F X X ≫ F.map μ =
    (α_ (F.obj X) (F.obj X) (F.obj X)).hom ≫ F.obj X ◁ («μ» F X X ≫ F.map μ) ≫ «μ» F X X ≫ F.map μ

Tactic:
by

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ η ≫ F.map f = η

Tactic:
by

Goal state after:
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.LaxMonoidal
inst✝⁴ : F'.LaxMonoidal
inst✝³ : G.LaxMonoidal
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : X ⟶ Y
inst✝ : IsMonHom f
⊢ μ ≫ F.map f = (F.map f ⊗ₘ F.map f) ≫ μ

Tactic:
by

Goal state after:
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.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst✝ : MonObj (F.obj X)
⊢ F.map (hF.preimage («η» F ≫ η) ▷ X ≫ hF.preimage (δ F X X ≫ μ)) = F.map (λ_ X).hom

Tactic:
by

Goal state after:
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.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst✝ : MonObj (F.obj X)
⊢ F.map (X ◁ hF.preimage («η» F ≫ η) ≫ hF.preimage (δ F X X ≫ μ)) = F.map (ρ_ X).hom

Tactic:
by

Goal state after:
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.OplaxMonoidal
hF : F.FullyFaithful
X : C
inst✝ : MonObj (F.obj X)
⊢ F.map (hF.preimage (δ F X X ≫ μ) ▷ X ≫ hF.preimage (δ F X X ≫ μ)) =
    F.map ((α_ X X X).hom ≫ X ◁ hF.preimage (δ F X X ≫ μ) ≫ hF.preimage (δ F X X ≫ μ))

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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
hF : F.FullyFaithful
X Y : C
inst✝² : AddMonObj X
inst✝¹ : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsAddMonHom f
⊢ F.map (AddMonObj.zero ≫ hF.preimage f) = F.map AddMonObj.zero

Tactic:
by

Goal state after:
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
hF : F.FullyFaithful
X Y : C
inst✝² : AddMonObj X
inst✝¹ : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsAddMonHom f
⊢ F.map (AddMonObj.add ≫ hF.preimage f) = F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ AddMonObj.add)

Tactic:
by

Goal state after:
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
hF : F.FullyFaithful
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsMonHom f
⊢ F.map (η ≫ hF.preimage f) = F.map η

Tactic:
by

Goal state after:
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
hF : F.FullyFaithful
X Y : C
inst✝² : MonObj X
inst✝¹ : MonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsMonHom f
⊢ F.map (μ ≫ hF.preimage f) = F.map ((hF.preimage f ⊗ₘ hF.preimage f) ≫ μ)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
⊢ F.mapMon.essImage M → F.essImage M.X

Tactic:
rintro ⟨N, ⟨e⟩⟩

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
N : Mon C
e : F.mapMon.obj N ≅ M
⊢ F.essImage M.X
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
⊢ F.mapMon.essImage M → F.essImage M.X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
⊢ F.essImage M.X → F.mapMon.essImage M

Tactic:
rintro ⟨N, ⟨e⟩⟩

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
N : C
e : F.obj N ≅ M.X
⊢ F.mapMon.essImage M
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
M : Mon D
⊢ F.essImage M.X → F.mapMon.essImage M

Tactic:
by

Goal state after:
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✝⁴ : BraidedCategory C
inst✝³ : BraidedCategory D
inst✝² : F.LaxBraided
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ η ≫ «μ» F M N = η

Tactic:
by

Goal state after: