mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ Relations (F ⋙ uliftFunctor) ≤ (DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker

Tactic:
AddSubgroup.closure_le

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ {x | ∃ j j' u a, x = DFinsupp.single j' ((ConcreteCategory.hom ((F ⋙ uliftFunctor).map u)) a) - DFinsupp.single j a} ⊆
    ↑(DFinsupp.sumAddHom fun j ↦ (Quot.ι F j).comp AddEquiv.ulift.toAddMonoidHom).ker
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝¹ x✝ : Quot F
⊢ (quotToQuotUlift F) (x✝¹ + x✝) = (quotToQuotUlift F) x✝¹ + (quotToQuotUlift F) x✝

Tactic:
by simp

Goal state after:
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
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂) α).app d) ≫ adj₂.counit.app (H.obj d) = α.app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : Cᵒᵖ
f : x✝¹ ⟶ x✝
⊢ (X ◁ f ≫ (β_ (Opposite.unop x✝) (Opposite.unop X)).op.hom).unop =
    ((β_ (Opposite.unop x✝¹) (Opposite.unop X)).op.hom ≫ f ▷ X).unop

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : Cᵒᵖ
f : x✝¹ ⟶ x✝
Z : Cᵒᵖ
⊢ (f ▷ Z ≫ (β_ (Opposite.unop Z) (Opposite.unop x✝)).op.hom).unop =
    ((β_ (Opposite.unop Z) (Opposite.unop x✝¹)).op.hom ≫ Z ◁ f).unop

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : Cᴹᵒᵖ
f : x✝¹ ⟶ x✝
⊢ (X ◁ f ≫ (β_ x✝.unmop X.unmop).mop.hom).unmop = ((β_ x✝¹.unmop X.unmop).mop.hom ≫ f ▷ X).unmop

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : Cᴹᵒᵖ
f : x✝¹ ⟶ x✝
Z : Cᴹᵒᵖ
⊢ (f ▷ Z ≫ (β_ Z.unmop x✝.unmop).mop.hom).unmop = ((β_ Z.unmop x✝¹.unmop).mop.hom ≫ Z ◁ f).unmop

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
X x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ X ◁ f ≫ (β_ x✝ X).symm.hom = (β_ x✝¹ X).symm.hom ≫ f ▷ X

Tactic:
by simp

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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
Z : C
⊢ f ▷ Z ≫ (β_ Z x✝).symm.hom = (β_ Z x✝¹).symm.hom ≫ Z ◁ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ reverseBraiding C = i.toBraidedCategory

Tactic:
dsimp only [reverseBraiding]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
i : SymmetricCategory C
⊢ { braiding := fun X Y ↦ (β_ Y X).symm, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯,
      hexagon_forward := ⋯, hexagon_reverse := ⋯ } =
    i.toBraidedCategory
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 L₁

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 L₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 R₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 R₁

Tactic:
by simp

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⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
rw [one_mul]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : ↑M →ₛₗ[f] ↑N
⊢ ∀ (x y : ↑M), g (x + y) = g x + g y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : ↑M →ₛₗ[f] ↑N
⊢ ∀ (m : R) (x : ↑M), g (m • x) = (RingHom.id R) m • g x

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : M ⟶ (restrictScalars f).obj N
⊢ ∀ (x y : ↑M), (ConcreteCategory.hom g) (x + y) = (ConcreteCategory.hom g) x + (ConcreteCategory.hom g) y

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
s : S
⊢ (1 • g) s = g s

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : S
⊢ (x✝¹ • 0) x✝ = 0 x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x✝ : S
⊢ (s • (g + h)) x✝ = (s • g + s • h) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y1 y2 : ↑Y
s : S
⊢ ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
          { toFun := fun s ↦ (ConcreteCategory.hom g) (s • (y1 + y2)), map_add' := ⋯, map_smul' := ⋯ }))
      s =
    ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y1), map_add' := ⋯, map_smul' := ⋯ } +
          (CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y2), map_add' := ⋯, map_smul' := ⋯ }))
      s

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
x y : ↑((restrictScalars f).obj Y)
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (x + y))) 1 =
    ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) x)) 1 +
      ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
x1 x2 : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (x1 + x2)) 1 = ((CoextendScalars.equiv f X) x1) 1 + ((CoextendScalars.equiv f X) x2) 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x✝¹ x✝ : ↑X
⊢ (ConcreteCategory.hom g) (1 ⊗ₜ[R] (x✝¹ + x✝)) =
    (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝¹) + (ConcreteCategory.hom g) (1 ⊗ₜ[R] x✝)

Tactic:
rw [tmul_add, map_add]

Goal state after:
Module: Mathlib.Order.Category.Preord

Goal state before:
pp: X : Preord
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.Preord

Goal state before:
pp: X Y Z : Preord
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X : PartOrd
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.PartOrd

Goal state before:
pp: X Y Z : PartOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.Lat

Goal state before:
pp: X : Lat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.Lat

Goal state before:
pp: X Y Z : Lat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: X : BddOrd
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddOrd

Goal state before:
pp: X Y Z : BddOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toPartOrd
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.DistLat

Goal state before:
pp: X : DistLat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.DistLat

Goal state before:
pp: X Y Z : DistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X : Lat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X Y Z : Lat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddDistLat

Goal state before:
pp: X : BddDistLat
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BddDistLat

Goal state before:
pp: X Y Z : BddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: X : HeytAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.HeytAlg

Goal state before:
pp: X Y Z : HeytAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
⊢ (⇑f ∘ ⇑g) ⊥ = ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom β γ
g : HeytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⇨ b) = (⇑f ∘ ⇑g) a ⇨ (⇑f ∘ ⇑g) b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
⊢ (⇑f ∘ ⇑g) ⊤ = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom β γ
g : CoheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a \ b) = (⇑f ∘ ⇑g) a \ (⇑f ∘ ⇑g) b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a ⇨ b) = (⇑f ∘ ⇑g) a ⇨ (⇑f ∘ ⇑g) b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom β γ
g : BiheytingHom α β
a b : α
⊢ (⇑f ∘ ⇑g) (a \ b) = (⇑f ∘ ⇑g) a \ (⇑f ∘ ⇑g) b

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ₘ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X : BoolAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.BoolAlg

Goal state before:
pp: X Y Z : BoolAlg
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

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

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
inst✝² : MonoidalCategory C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv ≫ 𝟙 (𝟙_ C) ▷ 𝟙_ C = (λ_ (𝟙_ C)).inv

Tactic:
by simp

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 = 0 ∧ ¬a ^ n * c = 0
⊢ normalize a ::ₘ replicate n (normalize a) ≤ normalize a ::ₘ normalizedFactors (a ^ n * c)

Tactic:
cons_le_cons_iff,

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 (normalize a) ≤ normalizedFactors (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
n : ℕ
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
by simp

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
x : R
inst✝ : Away x S
⊢ (fun x_1 ↦ x ^ x_1) 1 = x

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x : R
hx : x ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x✝ : x - 0 ∈ span s
⊢ p (x - 0) x✝ → p x hx

Tactic:
by simp

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
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ ∃ a, (algebraMap R S) a = mk' S x ⟨(fun x ↦ e ^ x) n, ⋯⟩

Tactic:
suffices ∃ a k, e ^ k * (a * e ^ n) = e ^ k * x by
    simpa [IsLocalization.eq_mk'_iff_mul_eq, ← map_pow, ← map_mul,
      IsLocalization.eq_iff_exists (.powers e), Submonoid.mem_powers_iff]

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : R
n : ℕ
⊢ ∃ a k, e ^ k * (a * e ^ n) = e ^ k * x
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
e : R
he : IsIdempotentElem e
H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y
H' : Function.Surjective ⇑(algebraMap R S)
z : R
⊢ (algebraMap R S) z * (algebraMap R S) ↑(z, 1).2 = (algebraMap R S) (z, 1).1

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) (1 * x) 1 = x

Tactic:
by simp

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

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝² : CommRing S
inst✝¹ : CommRing T
inst✝ : Algebra S T
h₁ : Function.Surjective ⇑(algebraMap S T)
r : S
hr : IsUnit ((algebraMap S T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
s : S
⊢ ∃ a, (algebraMap S T) s * (algebraMap S T) r ^ 0 = (algebraMap S T) a

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J : Ideal R
x✝ : R
h : ∀ (I : TwoSidedIdeal R), ↑J ⊆ ↑I → x✝ ∈ I
x : R
⊢ x ∈ ↑J → x ∈ ↑(mk' ↑J ⋯ ⋯ ⋯ ⋯ ⋯)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x✝ : TwoSidedIdeal R
⊢ (fun I ↦
        have this := ⋯;
        (↑I).toTwoSided)
      ((fun I ↦ ⟨asIdeal I, ⋯⟩) x✝) =
    x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : { I // I.IsTwoSided }
⊢ (fun I ↦ ⟨asIdeal I, ⋯⟩)
      ((fun I ↦
          have this := ⋯;
          (↑I).toTwoSided)
        I) =
    I

Tactic:
by simp

Goal state after:
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 + 1) ∈ M

Tactic:
neg_mul,

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) + 1) ∈ M
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : IsLocalRing R
⊢ 0 ∈ nonunits R

Tactic:
by simp

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
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts✝ : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r ↦ ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
a : ↑s
hts : insert ↑a ↑t ⊆ s
⊢ ↑({↑a} ∪ t) = {↑a} ∪ ↑t

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
h : r - 1 ∈ ⊥.jacobson
s : R
hs : r * s = 1
⊢ IsUnit r

Tactic:
exact .of_mul_eq_one _ hs

Goal state after: