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

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
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
E' : Type u₄
inst✝⁸ : Category.{v₄, u₄} E'
inst✝⁷ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁶ : F₁.LaxMonoidal
inst✝⁵ : F₂.LaxMonoidal
inst✝⁴ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝³ : G₁.LaxMonoidal
inst✝² : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝¹ : IsMonoidal τ
inst✝ : IsMonoidal τ'
X Y : C
⊢ μ (F₁ ⋙ G₁) X Y ≫ (τ ◫ τ').app (X ⊗ Y) = ((τ ◫ τ').app X ⊗ₘ (τ ◫ τ').app Y) ≫ μ (F₂ ⋙ G₂) X Y

Tactic:
simp only [comp_obj, comp_μ, hcomp_app, assoc, naturality_assoc,
      tensor_assoc, ← tensorHom_comp_tensorHom, μ_natural_assoc]

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
E : Type u₃
inst✝¹⁰ : Category.{v₃, u₃} E
inst✝⁹ : MonoidalCategory E
E' : Type u₄
inst✝⁸ : Category.{v₄, u₄} E'
inst✝⁷ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁶ : F₁.LaxMonoidal
inst✝⁵ : F₂.LaxMonoidal
inst✝⁴ : F₃.LaxMonoidal
G₁ G₂ : D ⥤ E
inst✝³ : G₁.LaxMonoidal
inst✝² : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝¹ : IsMonoidal τ
inst✝ : IsMonoidal τ'
X Y : C
⊢ (τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫ μ G₂ (F₁.obj X) (F₁.obj Y) ≫ G₂.map (μ F₁ X Y) ≫ G₂.map (τ.app (X ⊗ Y)) =
    (τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
      μ G₂ (F₁.obj X) (F₁.obj Y) ≫ G₂.map (τ.app X ⊗ₘ τ.app Y) ≫ G₂.map (μ F₂ X Y)
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommRingCat).sections
this✝¹ : (forget₂ CommRingCat RingCat).ReflectsIsomorphisms
this✝ : Small.{u, max u v} ↑((F ⋙ forget₂ CommRingCat RingCat) ⋙ forget RingCat).sections
F' : J ⥤ SemiRingCat := F ⋙ forget₂ CommRingCat RingCat ⋙ forget₂ RingCat SemiRingCat
this : Small.{u, max u v} ↑(F' ⋙ forget SemiRingCat).sections
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj (of (Types.Small.limitCone (F ⋙ forget CommRingCat)).pt)).map f ≫
      ofHom (SemiRingCat.limitπRingHom F' x✝) =
    ofHom (SemiRingCat.limitπRingHom F' x✝¹) ≫ F.map f

Tactic:
ext
            simpa using! (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

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
inst✝ : F.OplaxMonoidal
X Y Z : C
⊢ (δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z) ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv =
    F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z

Tactic:
Iso.comp_inv_eq,

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.OplaxMonoidal
X Y Z : C
⊢ δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z =
    (F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z) ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: 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

Tactic:
exact TensorProduct.ext rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: 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

Tactic:
exact TensorProduct.ext rfl

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
εIso : 𝟙_ D ≅ F.obj (𝟙_ C)
μIso : (X Y : C) → F.obj X ⊗ F.obj Y ≅ F.obj (X ⊗ Y)
μIso_inv_natural_left :
  ∀ {X Y : C} (f : X ⟶ Y) (X' : C), (μIso X X').inv ≫ F.map f ▷ F.obj X' = F.map (f ▷ X') ≫ (μIso Y X').inv
μIso_inv_natural_right :
  ∀ {X Y : C} (X' : C) (f : X ⟶ Y), (μIso X' X).inv ≫ F.obj X' ◁ F.map f = F.map (X' ◁ f) ≫ (μIso X' Y).inv
oplax_associativity :
  ∀ (X Y Z : C),
    (μIso (X ⊗ Y) Z).inv ≫ (μIso X Y).inv ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
      F.map (α_ X Y Z).hom ≫ (μIso X (Y ⊗ Z)).inv ≫ F.obj X ◁ (μIso Y Z).inv
oplax_left_unitality : ∀ (X : C), (λ_ (F.obj X)).inv = F.map (λ_ X).inv ≫ (μIso (𝟙_ C) X).inv ≫ εIso.inv ▷ F.obj X
oplax_right_unitality : ∀ (X : C), (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ (μIso X (𝟙_ C)).inv ≫ F.obj X ◁ εIso.inv
X : C
⊢ (λ_ (F.obj X)).hom = εIso.hom ▷ F.obj X ≫ (μIso (𝟙_ C) X).hom ≫ F.map (λ_ X).hom

Tactic:
by
    rw [← cancel_mono (λ_ (F.obj X)).inv, Iso.hom_inv_id, oplax_left_unitality]
    simp

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).inv = F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
← cancel_epi (ρ_ _).hom,

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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).hom ≫ (ρ_ (F.obj x✝)).inv =
    (ρ_ (F.obj x✝)).hom ≫ F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv
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
j : J
⊢ ((hc.desc (coconeLeftOpOfCone s)).op ≫ (coneOfCoconeLeftOp c).π.app j).unop = (s.π.app j).unop

Tactic:
by
      simp only [coneOfCoconeLeftOp_π_app, unop_comp, Quiver.Hom.unop_op, IsColimit.fac,
        coconeLeftOpOfCone_ι_app, unop_op]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f.op g.op).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((span f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((span f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((span f.op g.op).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.op g.op).obj WalkingSpan.right)).hom ≫
        (walkingCospanOpEquiv.inverse ⋙ (cospan f g).op).map f_1

Tactic:
by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingSpan} (f_1 : X_1 ⟶ Y_1),
    (span f.unop g.unop).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((span f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((span f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((span f.unop g.unop).obj WalkingSpan.left)
          | some WalkingPair.right => Iso.refl ((span f.unop g.unop).obj WalkingSpan.right)).hom ≫
        (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp).map f_1

Tactic:
by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f.op g.op).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((cospan f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((cospan f.op g.op).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.op g.op).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.op g.op).obj WalkingCospan.right)).hom ≫
        (walkingSpanOpEquiv.inverse ⋙ (span f g).op).map f_1

Tactic:
by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : X ⟶ Z
⊢ ∀ {X_1 Y_1 : WalkingCospan} (f_1 : X_1 ⟶ Y_1),
    (cospan f.unop g.unop).map f_1 ≫
        (match Y_1 with
          | none => Iso.refl ((cospan f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom =
      (match X_1 with
          | none => Iso.refl ((cospan f.unop g.unop).obj none)
          | some WalkingPair.left => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.left)
          | some WalkingPair.right => Iso.refl ((cospan f.unop g.unop).obj WalkingCospan.right)).hom ≫
        (walkingSpanOpEquiv.inverse ⋙ (span f g).leftOp).map f_1

Tactic:
by rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

Goal state after:
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 : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C

Tactic:
braiding_leftUnitor_aux₂

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (ρ_ X).hom ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
this✝ : Invertible x.fst
this : Invertible x
⊢ x * x⁻¹ = 1

Tactic:
rw [← invOf_eq_inv, mul_invOf_self]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: 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
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
mul_assoc,

Goal state after:
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
x : tsze R M
hx : x.fst ≠ 0
⊢ x * (x⁻¹ * x⁻¹⁻¹) = x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hl
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
x : A
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul x) + (TensorProduct.map (inr R A B) (inr R A B)) (comul 0))

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
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) + (TensorProduct.map (inr R A B) (inr R A B)) (comul x))

Tactic:
· simp only [map_zero, add_zero]
      simp_rw [← comp_apply, ← comp_assoc, rTensor_comp_map, lTensor_comp_map, coprod_inl,
        ← map_comp_rTensor, ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc,
        TensorProduct.map_map_comp_assoc_eq, comp_apply, LinearEquiv.coe_coe]

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
x : B
⊢ (TensorProduct.assoc R (A × B) (A × B) (A × B))
      ((rTensor (A × B)
          ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
            (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
        ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) +
          (TensorProduct.map (inr R A B) (inr R A B)) (comul x))) =
    (lTensor (A × B)
        ((TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul).coprod
          (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul)))
      ((TensorProduct.map (inl R A B) (inl R A B)) (comul 0) + (TensorProduct.map (inr R A B) (inr R A B)) (comul x))
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)

Tactic:
rw [le_sup_inf_aux, add_self, mul_self, zero_add]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a * a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)

Tactic:
mul_assoc,

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a * (a ^ n * c) = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a ^ (n + 1) * c)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a * a ^ n * c)

Tactic:
mul_assoc,

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors (a * (a ^ n * c))
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
x : R
inst✝ : Away x S
s : S
⊢ Associated ((algebraMap R S) (sec x s).1) s

Tactic:
← IsLocalization.Away.sec_spec,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
s : S
⊢ Associated (s * (algebraMap R S) (x ^ (sec x s).2)) s
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ↑u ^ n * r ^ n * a = ↑u ^ n * r ^ n * b

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ↑u ^ n * (r ^ n * a) = ↑u ^ n * r ^ n * b
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ↑u ^ n * (r ^ n * a) = ↑u ^ n * r ^ n * b

Tactic:
mul_assoc,

Goal state after:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ↑u ^ n * (r ^ n * a) = ↑u ^ n * (r ^ n * b)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ span s → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I

Tactic:
delta span

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ { ringCon := ringConGen fun a b ↦ a - b ∈ s } → ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → x ∈ I
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
le : N ≤ jacobson R M
⊢ N.mkQ.ker ≤ jacobson R M

Tactic:
rwa [ker_mkQ]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * (y * x) + r - 1 ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M

Tactic:
mul_assoc,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * (-y * x) + z ∈ M
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_4
inst✝ : CommSemiring A
f : R →+* A
r a : R
v : A
hv : f r * v = 1
j : ℕ
⊢ (awayLift f r ⋯) (mk a ⟨r ^ j, ⋯⟩) = f a * v ^ j

Tactic:
simp [Localization.mk_eq_mk', awayLift, Away.lift, IsLocalization.lift_mk',
    Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight, mul_assoc, ← mul_pow, (mul_comm _ _).trans hv]

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

Goal state before:
pp: 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
finset_eq : ∃ t, ↑t = s
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
have span_eq := (Ideal.eq_top_iff_one _).mpr mem

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
finset_eq : ∃ t, ↑t = s
span_eq : Ideal.span s = ⊤
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ I_1

Tactic:
intro 𝔪

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
⊢ 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ 𝔪