mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Mates

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

Tactic:
R₃.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      (R₃.map (β.app (G₁.obj (R₁.obj b))) ≫
          R₃.map
            ((L₂ ⋙ H₂).map (adj₂.unit.app (G₁.obj (R₁.obj b)) ≫ R₂.map (α.natTrans.app (R₁.obj b))) ≫
              (L₂ ⋙ H₂).map (R₂.map (H₁.map (adj₁.counit.app b))))) ≫
        R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ((lift R) f).range = Algebra.adjoin R (Set.range ⇑f)

Tactic:
by
  simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

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
⊢ (lTensor (A × B) counit ∘ₗ comul) ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
· rw [comp_assoc, comul_comp_inr, ← comp_assoc, lTensor_comp_map, counit_comp_inr,
        ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝² : Ring R
inst✝¹ : CommRing S
f : R →+* S
M : Type v
I : AddCommGroup M
inst✝ : Module S M
r : R
s : S
m : M
⊢ f r • s • m = s • f r • m

Tactic:
by simp [← mul_smul, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

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

Tactic:
abel

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ ε.op ▷ op A.X ≫ Δ.op = (λ_ (op A.X)).hom

Tactic:
← op_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (ε ▷ A.X).op ≫ Δ.op = (λ_ (op A.X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ Δ.op ▷ op A.X ≫ Δ.op = (α_ A.X A.X A.X).inv.op ≫ op A.X ◁ Δ.op ≫ Δ.op

Tactic:
← op_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (Δ ▷ A.X).op ≫ Δ.op = (α_ A.X A.X A.X).inv.op ≫ op A.X ◁ Δ.op ≫ Δ.op
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
hb : ¬b = 0
this : StrongNormalizationMonoid R := UniqueFactorizationMonoid.strongNormalizationMonoid
q : R
hq : q ∉ normalizedFactors a
⊢ Multiset.count q (normalizedFactors a) ≤ Multiset.count q (normalizedFactors b)

Tactic:
· simp [Multiset.count_eq_zero_of_notMem hq]

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
⊢ x ∈ I

Tactic:
rcases hM I hI with is_max | is_top

Goal state after:
case mpr.inl
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_max : I.IsMaximal
⊢ x ∈ I

case mpr.inr
R : Type u
inst✝ : Ring R
I✝ : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I✝ = sInf M
x : R
hx : x ∈ I✝.jacobson
I : Ideal R
hI : I ∈ M
is_top : I = ⊤
⊢ x ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ x ∉ I.jacobson

Tactic:
rw [Ideal.jacobson, mem_sInf]

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

Tactic:
isLocalizedModule_iff,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
⊢ ((∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R Aₛ)) ↑x)) ∧
      (∀ (y : Aₛ), ∃ x, x.2 • y = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x.1) ∧
        ∀ {x₁ x₂ : A},
          (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₁ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap x₂ →
            ∃ c, c • x₁ = c • x₂) ↔
    IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ η = η

Tactic:
trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ η = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ

C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η) ≫ μ = η
Module: Mathlib.RingTheory.Localization.Integer

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
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
i j : ↥s
h : integerMultiple M s f i = integerMultiple M s f j
⊢ ↑i = ↑j

Tactic:
← hf.eq_iff,

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
i j : ↥s
h : integerMultiple M s f i = integerMultiple M s f j
⊢ f ↑i = f ↑j
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case right
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)
s : PullbackCone f g
⊢ BinaryFan.IsLimit.lift H₂ s.fst s.snd ≫ (PullbackCone.mk h k ⋯).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
      m ≫ (PullbackCone.mk h k ⋯).fst = s.fst →
        m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd

Tactic:
use BinaryFan.IsLimit.lift_snd _ _ _

Goal state after:
case right
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)
s : PullbackCone f g
⊢ ∀ {m : s.pt ⟶ (PullbackCone.mk h k ⋯).pt},
    m ≫ (PullbackCone.mk h k ⋯).fst = s.fst →
      m ≫ (PullbackCone.mk h k ⋯).snd = s.snd → m = BinaryFan.IsLimit.lift H₂ s.fst s.snd
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R✝ : Type u_1
inst✝²³ : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝²² : CommSemiring A✝
inst✝²¹ : Algebra R✝ A✝
inst✝²⁰ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R✝ M✝
M' : Type u_4
inst✝¹⁷ : AddCommMonoid M'
inst✝¹⁶ : Module R✝ M'
inst✝¹⁵ : Module A✝ M'
inst✝¹⁴ : IsScalarTower R✝ A✝ M'
f : M✝ →ₗ[R✝] M'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x✝ : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (S ⊗[R] A)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ A]

Goal state after:
R✝ : Type u_1
inst✝²³ : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝²² : CommSemiring A✝
inst✝²¹ : Algebra R✝ A✝
inst✝²⁰ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R✝ M✝
M' : Type u_4
inst✝¹⁷ : AddCommMonoid M'
inst✝¹⁶ : Module R✝ M'
inst✝¹⁵ : Module A✝ M'
inst✝¹⁴ : IsScalarTower R✝ A✝ M'
f : M✝ →ₗ[R✝] M'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
x✝ : Algebra A (S ⊗[R] A) := Algebra.TensorProduct.rightAlgebra
⊢ Algebra.IsPushout R S A (S ⊗[R] A)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R✝ : Type u_1
inst✝²³ : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝²² : CommSemiring A✝
inst✝²¹ : Algebra R✝ A✝
inst✝²⁰ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R✝ M✝
M' : Type u_4
inst✝¹⁷ : AddCommMonoid M'
inst✝¹⁶ : Module R✝ M'
inst✝¹⁵ : Module A✝ M'
inst✝¹⁴ : IsScalarTower R✝ A✝ M'
f : M✝ →ₗ[R✝] M'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) (A ⊗[R] S)

Tactic:
rw [Algebra.isLocalization_iff_isPushout _ A]

Goal state after:
R✝ : Type u_1
inst✝²³ : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝²² : CommSemiring A✝
inst✝²¹ : Algebra R✝ A✝
inst✝²⁰ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : Module R✝ M✝
M' : Type u_4
inst✝¹⁷ : AddCommMonoid M'
inst✝¹⁶ : Module R✝ M'
inst✝¹⁵ : Module A✝ M'
inst✝¹⁴ : IsScalarTower R✝ A✝ M'
f : M✝ →ₗ[R✝] M'
T : Type u_5
B : Type u_6
inst✝¹³ : CommSemiring T
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R✝ T
inst✝¹⁰ : Algebra T B
inst✝⁹ : Algebra R✝ B
inst✝⁸ : Algebra A✝ B
inst✝⁷ : IsScalarTower R✝ T B
inst✝⁶ : IsScalarTower R✝ A✝ B
R : Type u_7
S : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
r : R
A : Type u_9
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
M : Submonoid R
inst✝ : IsLocalization M A
⊢ Algebra.IsPushout R S A (A ⊗[R] S)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
S✝ : Submonoid R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
T : Type u_1
inst✝⁷ : CommSemiring T
inst✝⁶ : Algebra R T
inst✝⁵ : IsLocalization S✝ T
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), 0 * a = 0

Tactic:
rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ pushout.inl f g ≫ pushout.inr f' (pushout.inl f g) ≫ (pushoutRightPushoutInlIso f g f').hom =
    f' ≫ pushout.inl (f ≫ f') g

Tactic:
by
  rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd ({a} + m)) = of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)

Tactic:
ofAdd_add,

Goal state after:
α : Type u
a : α
m : Multiset α
⊢ FreeAbelianGroup.of (Multiplicative.ofAdd {a} * Multiplicative.ofAdd m) =
    of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case mul
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝

Tactic:
rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

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

Goal state before:
pp: case h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
y : LocalizedModule S M
m : M
s : ↥S
⊢ r • mk m s = y ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • y

Tactic:
induction y using induction_on with

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
Algebra.algebraMap_eq_smul_one

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • 1 = mk ((algebraMap R A) a) s
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
⊢ IsSplitMono (T.η.app X) ↔ IsIso (T.η.app X)

Tactic:
by
  refine ⟨fun _ ↦ ⟨retraction (T.η.app X), by simp, ?_⟩, fun _ ↦ inferInstance⟩
  rw [← map_id, ← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _,
    map_comp, T.map_unit_app X, ← T.unit_naturality]

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

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ f (↑(a, b).2 • a') = f (↑(a', b').2 • a)

Tactic:
exact (IsLocalizedModule.eq_iff_exists S f).mpr ⟨c, eq1.symm⟩

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

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
r : R
x : LocalizedModule S M
a : M
b : ↥S
⊢ r • fromLocalizedModule' S f (LocalizedModule.mk a b) = fromLocalizedModule' S f (r • LocalizedModule.mk a b)

Tactic:
rw [fromLocalizedModule'_mk, LocalizedModule.smul'_mk, fromLocalizedModule'_mk,
        f.map_smul, map_smul]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
r : R
⊢ (↑↑(Hom.hom h)).toFun ((algebraMap R (A ⊗[R] B)) r) = (algebraMap R ↑s.pt) r

Tactic:
change h (algebraMap R A r ⊗ₜ[R] 1) = s.inl (algebraMap R A r)

Goal state after:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
r : R
⊢ (ConcreteCategory.hom h) ((algebraMap R A) r ⊗ₜ[R] 1) = (ConcreteCategory.hom s.inl) ((algebraMap R A) r)
Module: Mathlib.CategoryTheory.Comma.Over.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : HasPushoutsAlong f
x : Under X
y : Under Y
u : (pushout f).obj x ⟶ y
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u

Tactic:
rw [← assoc, ← assoc, pushout.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
simp [mapId']

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
simp [mapId']

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵖ C
b : B
⊢ F.mapId' (𝟙 b) ⋯ = F.mapId b

Tactic:
simp [mapId']

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : Algebra R X✝
inst✝³ : CommRing Y✝
inst✝² : Algebra R Y✝
inst✝¹ : CommRing Z
inst✝ : Algebra R Z
X Y : CommAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommAlgCat R)).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget (CommAlgCat.{u} R)).map f)
    let e : X ≃ₐ[R] Y := { f.hom, i.toEquiv with }
    exact (isoMk e).isIso_hom

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ Function.Surjective fun X ↦ ⟨↑(φ X), ⋯⟩

Tactic:
rintro ⟨_, Z, rfl⟩; exact ⟨Z, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
X : C
h : F.CorepresentableBy X
Y : F.Elements
m : initialOfCorepresentableBy h ⟶ Y
⊢ m = ⟨h.homEquiv.symm Y.snd, ⋯⟩

Tactic:
simp [← m.2, ← h.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : (coconeFiberwiseColimitOfCocone c).pt ⟶ s.pt
hm : ∀ (j : C), (coconeFiberwiseColimitOfCocone c).ι.app j ≫ m = s.ι.app j
X : Grothendieck F
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }

Tactic:
have := hm X.base

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : (coconeFiberwiseColimitOfCocone c).pt ⟶ s.pt
hm : ∀ (j : C), (coconeFiberwiseColimitOfCocone c).ι.app j ≫ m = s.ι.app j
X : Grothendieck F
this : (coconeFiberwiseColimitOfCocone c).ι.app X.base ≫ m = s.ι.app X.base
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ (𝟙 (F.obj X.base)).toFunctor.obj X.fiber = X.fiber

Tactic:
Cat.Hom.id_obj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
e₁ : X.base ≅ Y.base
e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber
⊢ X.fiber = X.fiber
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : Cat
f✝ : a✝ ⟶ b✝
X : ↑(Cat.of (WithTerminal ↑a✝))
⊢ (NatTrans.toCatHom₂ (map₂ (𝟙 f✝).toNatTrans)).toNatTrans.app X = (𝟙 (map f✝.toFunctor).toCatHom).toNatTrans.app X

Tactic:
cases X <;> rfl

Goal state after: