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

Goal state before:
pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (μ ⊗ₘ μ) ≫ (f ⊗ₘ g)

pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| tensorμ X Z X Z

Tactic:
rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]

Goal state after:
case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| ((f ⊗ₘ f) ⊗ₘ g ⊗ₘ g) ≫ (μ ⊗ₘ μ)

case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| tensorμ X Z X Z
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
M N O X✝ : C
inst✝¹⁰ : MonObj M
inst✝⁹ : MonObj N
inst✝⁸ : MonObj O
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
inst✝⁶ : MonoidalCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝³ : F.Monoidal
hF : F.FullyFaithful
X Y : C
inst✝² : AddMonObj X
inst✝¹ : AddMonObj Y
f : F.obj X ⟶ F.obj Y
inst✝ : IsAddMonHom f
⊢ F.map (AddMonObj.zero ≫ hF.preimage f) = F.map AddMonObj.zero

Tactic:
simp [← cancel_epi (ε F), ← obj.ζ_def_assoc, ← obj.ζ_def]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₂ ⟶ X₁
f₂ : X₃ ⟶ X₂
i₁ : Y₁ ⟶ X₁
t₁ : PullbackCone i₁ f₁
i₂ : t₁.pt ⟶ X₂
t₂ : PullbackCone i₂ f₂
hi₂ : i₂ = t₁.snd
⊢ (t₂.fst ≫ t₁.fst) ≫ i₁ = t₂.snd ≫ f₂ ≫ f₁

Tactic:
rw [← reassoc_of% t₂.condition, Category.assoc, t₁.condition, ← hi₂]

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

Goal state before:
pp: case refine_1
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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ f (x✝¹, x✝).1 =
    ↑eM.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).1

Tactic:
simp [LinearEquiv.eq_symm_apply, eM, eN]

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

Goal state before:
pp: case refine_2
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'
M₁ : Type ?u.45
M₂ : Type ?u.47
B : Type ?u.69
C : Type ?u.81
inst✝²¹ : AddCommMonoid M₁
inst✝²⁰ : AddCommMonoid M₂
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module A M₁
inst✝¹⁶ : Module A M₂
inst✝¹⁵ : IsScalarTower R A M₁
inst✝¹⁴ : IsScalarTower R A M₂
inst✝¹³ : Semiring B
inst✝¹² : Algebra R B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : IsScalarTower R A B
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
inst✝⁷ : Algebra A C
inst✝⁶ : IsScalarTower R A C
N : Type u_5
N' : Type u_6
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid N'
inst✝² : Module R N'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
eM : M' ≃ₗ[R] Localization S ⊗[R] M := IsLocalizedModule.linearEquiv S f ((mk R (Localization S) M) 1)
eN : N' ≃ₗ[R] Localization S ⊗[R] N := IsLocalizedModule.linearEquiv S g ((mk R (Localization S) N) 1)
x✝¹ : M
x✝ : N
⊢ g (x✝¹, x✝).2 =
    ↑eN.symm
      ((((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).1,
          (((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).1,
              ((mk R (Localization S) N)
                  ((((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1, 1).2)
                (↑(AlgebraTensorModule.rid (Localization S) (Localization S) (Localization S ⊗[R] M)).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).1,
                    ↑(LinearEquiv.refl R N).symm
                      (((mk R (Localization S) M) (1, ((mk R M N) x✝¹) x✝).1) (x✝¹, x✝).1, (x✝¹, x✝).2).2).2).2).2

Tactic:
simp [LinearEquiv.eq_symm_apply, eM, eN]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ IsPushout f' g' inl' inr'

Tactic:
apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commf, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← comminl, Iso.inv_hom_id_assoc]
  · simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← comminr, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ (IsLocalization.map (Localization (Algebra.algebraMapSubmonoid S M)) (RingHom.id S) ⋯)
      (IsLocalization.mk' (S ⊗[R] Rₘ) ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩) =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)

Tactic:
IsLocalization.map_mk',

Goal state after:
R : Type u_10
inst✝² : CommRing R
M : Submonoid R
S : Type u_12
inst✝¹ : CommRing S
inst✝ : Algebra R S
Rₘ : Type u_10 := Localization M
Sₘ : Type u_12 := Localization (Algebra.algebraMapSubmonoid S M)
x : R
y : ↥M
this : Algebra Rₘ (S ⊗[R] Rₘ) := Algebra.TensorProduct.rightAlgebra
h1 : 1 ⊗ₜ[R] IsLocalization.mk' Rₘ x y = (algebraMap Rₘ (S ⊗[R] Rₘ)) (IsLocalization.mk' Rₘ x y)
⊢ IsLocalization.mk' (Localization (Algebra.algebraMapSubmonoid S M)) ((RingHom.id S) ((algebraMap R S) x))
      ⟨(RingHom.id S) ↑⟨(algebraMap R S) ↑y, ⋯⟩, ⋯⟩ =
    (algebraMap (Localization M) (Localization (Algebra.algebraMapSubmonoid S M)))
      (IsLocalization.mk' (Localization M) x y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
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.π
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit <;> refine e.trans ?_ <;> symm <;>
      exact H.isColimit.fac _ _

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 ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) ≫ f' = pullback.fst (f' ≫ f) g ≫ f'

Tactic:
exact pullbackRightPullbackFstIso_inv_fst_assoc f g f' _

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs : x.IsSupported s
⊢ x.IsSupported ↑hfs.toFinset

Tactic:
Set.Finite.coe_toFinset

Goal state after:
α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs : x.IsSupported s
⊢ x.IsSupported s
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : G
⊢ (∃ y ∈ H, ↑y = x) ↔ toUnits x ∈ H

Tactic:
toUnits.surjective.exists,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup Gˣ
x : G
⊢ (∃ x_1, toUnits x_1 ∈ H ∧ ↑(toUnits x_1) = x) ↔ toUnits x ∈ H
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' := ⋯ }
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }

Tactic:
let g' : B →ₐ[R] s.pt :=
      { s.inr.hom with
        commutes' := DFunLike.congr_fun <| congrArg Hom.hom
          ((s.ι.naturality Limits.WalkingSpan.Hom.snd).trans
            (s.ι.naturality Limits.WalkingSpan.Hom.fst).symm) }

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' := ⋯ }
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }
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
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }

Tactic:
use ofHom (AlgHom.toRingHom (Algebra.TensorProduct.productMap f' g'))

Goal state after:
case property
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 := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ (pushoutCocone R A B).inl ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl ∧
    (pushoutCocone R A B).inr ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inr ∧
      ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
        (pushoutCocone R A B).inl ≫ m = s.inl →
          (pushoutCocone R A B).inr ≫ m = s.inr → m = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b' • a) = ↑⋯.unit⁻¹ (f (↑(b * b') • a))

pp: case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • f a')

Tactic:
all_goals rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff']

Goal state after:
case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (↑(b * b') • a) = ↑b • f (b' • a)

case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑(b * b') • f a' = ↑b' • f (b • a')
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: J : Type w
inst✝³ : Category.{w', w} J
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
G : A ⥤ T
X : T
F : J ⥤ CostructuredArrow G X
i₁ : HasColimit (F ⋙ proj G X)
i₂ : PreservesColimit (F ⋙ proj G X) G
⊢ HasColimit F

Tactic:
by
  have : HasColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) := i₁
  have : PreservesColimit (F ⋙ Comma.fst G (Functor.fromPUnit X)) _ := i₂
  apply Comma.hasColimit

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

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
j k : J
f : j ⟶ k
⊢ ((Functor.const J).obj (of (FreeCommRing PUnit.{u + 1}))).map f ≫
      ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv k) =
    ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j) ≫ F.map f

Tactic:
by
      ext1; change FreeCommRing.lift (fun _ => inv k) = _
      ext; simp [map_inv f]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk (⟨↑s, ⋯⟩ • m) s) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk (⟨↑s, ⋯⟩ • m) s)

Tactic:
mk_cancel

Goal state after:
case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) (LocalizedModule.mk m 1) =
    (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m 1)

Tactic:
simp [map, lift, iso_localizedModule_eq_refl, lift_mk]

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

Goal state before:
pp: R : Type u_6
M : Type u_8
M' : Type u_9
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
S : Submonoid R
g : M →ₗ[R] M'
inst✝ : IsLocalizedModule S g
⊢ Subsingleton M' ↔ g.ker = ⊤

Tactic:
rw [← top_le_iff]
  refine ⟨fun H m _ ↦ Subsingleton.elim _ _, fun H ↦ (subsingleton_iff_forall_eq 0).mpr fun x ↦ ?_⟩
  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S g x
  simpa using @H x Submodule.mem_top

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
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵒᵖᴸ C
G : C ⥤ᵒᵖᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.map₂ (F.map₂ (η ▷ g)) ≫ G.map₂ (F.mapComp f'✝ g) ≫ G.mapComp (F.map f'✝) (F.map g) =
    (G.map₂ (F.mapComp f✝ g) ≫ G.mapComp (F.map f✝) (F.map g)) ≫ G.map₂ (F.map₂ η) ▷ G.map (F.map g)

Tactic:
rw [← G.map₂_comp_assoc, mapComp_naturality_left, G.map₂_comp_assoc, mapComp_naturality_left,
      assoc]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing A
f : R →+* S
g : S →+* A
hf : (RingHom.ker f).FG
hg : (RingHom.ker g).FG
hsur : Function.Surjective ⇑f
this✝ : Algebra R S := f.toAlgebra
this : Algebra R A := (g.comp f).toAlgebra
⊢ (RingHom.ker (g.comp f)).FG

Tactic:
let : Algebra S A := RingHom.toAlgebra g

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing A
f : R →+* S
g : S →+* A
hf : (RingHom.ker f).FG
hg : (RingHom.ker g).FG
hsur : Function.Surjective ⇑f
this✝¹ : Algebra R S := f.toAlgebra
this✝ : Algebra R A := (g.comp f).toAlgebra
this : Algebra S A := g.toAlgebra
⊢ (RingHom.ker (g.comp f)).FG
Module: Mathlib.CategoryTheory.WithTerminal.Cone

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type w
inst✝ : Category.{w', w} J
X : C
K : J ⥤ Under X
F : C ⥤ D
t✝ : Cocone K
t : Cocone (liftFromUnder.obj K)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ K.map f ≫ Under.homMk (t.ι.app (of x✝)) ⋯ =
    Under.homMk (t.ι.app (of x✝¹)) ⋯ ≫ ((Functor.const J).obj (Under.mk (t.ι.app star))).map f

Tactic:
by ext; simpa using! t.ι.naturality (incl.map f)

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra R B
inst✝³ : IsScalarTower R A B
inst✝² : IsDomain A
inst✝¹ : Module.IsTorsionFree A B
inst✝ : Nontrivial B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
by
  rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ⇑f
hfk : (RingHom.ker f.toRingHom).FG
⊢ ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
set ulift_var := MvPolynomial.renameEquiv R Equiv.ulift

Goal state after:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ⇑f
hfk : (RingHom.ker f.toRingHom).FG
ulift_var : MvPolynomial (ULift.{?u.45, ?u.44} ?m.75) R ≃ₐ[R] MvPolynomial ?m.75 R :=
  MvPolynomial.renameEquiv R Equiv.ulift
⊢ ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
wlog hC : LocallySmall.{w} C; · simp [essentiallySmall_iff, hC]
  simp only [hC, ← exists_equivalence_iff_of_locallySmall, true_and]
  refine ⟨fun H ↦ H.1, fun H ↦ ⟨H⟩⟩

Goal state after: