mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso
            (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
            (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
              (Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                  (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
            Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
x✝² x✝¹ x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.associator x✝² x✝¹ x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝² x✝¹))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso
              (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                    (equivalenceSemimoduleCat.functor.obj x✝¹))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.associator (equivalenceSemimoduleCat.functor.obj x✝²)
              (equivalenceSemimoduleCat.functor.obj x✝¹) (equivalenceSemimoduleCat.functor.obj x✝) ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝²))
                (Iso.refl
                  (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝¹)
                    (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
              Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝²)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorObj x✝¹ x✝)))).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
            (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
        MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.leftUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R)))
                  (equivalenceSemimoduleCat.functor.obj x✝))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm
              (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))) ≪≫
          MonoidalCategoryStruct.leftUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom =
    (((Iso.refl
              (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
          MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
            (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
        MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom

Tactic:
ext1

Goal state after:
R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ SemimoduleCat.Hom.hom (equivalenceSemimoduleCat.functor.map (MonoidalCategoryStruct.rightUnitor x✝).hom) =
    SemimoduleCat.Hom.hom
      (((Iso.refl
                (MonoidalCategoryStruct.tensorObj (equivalenceSemimoduleCat.functor.obj x✝)
                  (equivalenceSemimoduleCat.functor.obj (MonoidalCategoryStruct.tensorUnit (ModuleCat R))))).symm ≪≫
            MonoidalCategory.tensorIso (Iso.refl (equivalenceSemimoduleCat.functor.obj x✝))
              (Iso.refl (MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))).symm) ≪≫
          MonoidalCategoryStruct.rightUnitor (equivalenceSemimoduleCat.functor.obj x✝)).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
⊢ CategoryTheory.inv (ε F) = η F

Tactic:
by simp [← inv_η]

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

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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ a = b

Tactic:
ext1

Goal state after:
case ε
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ ε F = ε F

case μ
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ μ F = μ F

case η
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ η F = η F

case δ
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
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
⊢ δ F = δ F
Module: Mathlib.CategoryTheory.Monoidal.Functor

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
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ a = b

Tactic:
ext1

Goal state after:
case ε
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
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F = ε F

case μ
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
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ μ F = μ F

case η
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
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ η F = η F

case δ
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
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
⊢ δ F = δ F
Module: Mathlib.CategoryTheory.Limits.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeLeftOpOfCone s)).op

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
    simpa only [Quiver.Hom.unop_op, IsColimit.fac, coneOfCoconeLeftOp_π_app] using! w (unop j)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasWidePullbacks C
⊢ HasWidePushouts Cᵒᵖ

Tactic:
by
  intro ι
  rw [hasColimitsOfShape_opposite_iff]
  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (pullbackComparison G f g)

Tactic:
rw [← PreservesPullback.iso_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : HasPullback f g
inst✝¹ : HasPullback (G.map f) (G.map g)
inst✝ : PreservesLimit (cospan f g) G
⊢ IsIso (PreservesPullback.iso G f g).hom
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).inv ≫
      (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom

Tactic:
← braiding_tensor_right_hom_assoc X Y Z,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
    X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ ((G ⋙ L₂).map (adj₁.unit.app X✝) ≫ α.natTrans.app (R₁.obj (L₁.obj X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) =
    α.natTrans.app X✝

Tactic:
α.natTrans.naturality,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ (α.natTrans.app X✝ ≫ (L₁ ⋙ H).map (adj₁.unit.app X✝)) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) = α.natTrans.app X✝
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (op x₂.1 + op x₃.1) •> x₁.2 =
    x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)

Tactic:
add_smul,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₂.2 + x₁.1 •> x₃.2 + (x₁.2 <• x₂.1 + x₁.2 <• x₃.1) =
    x₁.1 •> x₂.2 + x₁.2 <• x₂.1 + (x₁.1 •> x₃.2 + x₁.2 <• x₃.1)
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)

Tactic:
add_smul,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x₁.1 •> x₃.2 + x₂.1 •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

Tactic:
have := sum_counit_tmul_eq repr
  apply_fun LinearMap.lTensor R (f : A →ₗ[R] B) at this
  simp_all only [map_sum, LinearMap.lTensor_tmul, LinearMap.coe_coe]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.snd R A B ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
snd_comp_inr,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul ∘ₗ LinearMap.id = (TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul) ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map (LinearMap.snd R A B ∘ₗ inr R A B) (LinearMap.snd R A B ∘ₗ inr R A B) ∘ₗ comul

Tactic:
snd_comp_inr,

Goal state after:
case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ comul = TensorProduct.map LinearMap.id LinearMap.id ∘ₗ comul
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
obtain hb0 | hb := eq_or_ne (fst b) 0

Goal state after:
case h2.inr.inl
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb0 : b.fst = 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

case h2.inr.inr
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
ha : a.fst ≠ 0
hb : b.fst ≠ 0
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) +
      -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹)) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ f 1 + 0 = 1

Tactic:
map_one,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ 1 + 0 = 1
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
⊢ _root_.TensorProduct.map ↑(AlgebraTensorModule.assoc R S S M N P) ↑(AlgebraTensorModule.assoc R S S M N P) ∘ₗ comul =
    comul ∘ₗ ↑(AlgebraTensorModule.assoc R S S M N P)

Tactic:
ext x y z
      dsimp
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := S) y with y₁ y₂
      hopf_tensor_induction comul (R := R) z with z₁ z₂
      simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
x : R
inst✝ : Away x S
g : R →+* P
hg : IsUnit (g x)
y : ↥(Submonoid.powers x)
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ↑y
⊢ IsUnit (g x ^ n)

Tactic:
exact IsUnit.map (powMonoidHom n : P →* P) hg

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ Away (y * x) T

Tactic:
refine mk _ ?_ (fun z ↦ ?_) (fun a b h ↦ ?_)

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ IsUnit ((algebraMap R T) (y * x))

case refine_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
z : T
⊢ ∃ n a, z * (algebraMap R T) (y * x) ^ n = (algebraMap R T) a

case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
span_eq : Ideal.span s = ⊤
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
clear span_eq

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ⇑f
h : IsLocalHom f
⊢ Function.Surjective ⇑(Units.map ↑f)

Tactic:
by
  intro a
  obtain ⟨b, hb⟩ := hf (a : S)
  use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
  ext
  exact hb

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ (tensorμ (𝟙_ C) (𝟙_ C) M N ≫ (η ▷ M ⊗ₘ η ▷ N)) ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom

Tactic:
slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (λ_ (𝟙_ C)).inv ▷ (M ⊗ N) ≫ tensorμ (𝟙_ C) (𝟙_ C) M N ≫ ((λ_ M).hom ⊗ₘ (λ_ N).hom) = (λ_ (M ⊗ N)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2.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
⊢ (prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd) ≫ prod.fst =
    s.snd ≫ prod.fst

pp: case 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
⊢ (prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd) ≫ prod.snd =
    s.snd ≫ prod.snd

Tactic:
· simp [PullbackCone.condition]

Goal state after:
case 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
⊢ (prod.lift s.fst (s.snd ≫ prod.snd) ≫ (PullbackCone.mk prod.fst (prod.map f (𝟙 X)) ⋯).snd) ≫ prod.snd =
    s.snd ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π

Tactic:
exact H.isColimit.fac _ _

Goal state after: