mathlib-initiative/mathlib-tactics huggingface dataset:
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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this✝ : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this : IsIso (LaxMonoidal.ε e.inverse)
X Y : D
⊢ IsIso (LaxMonoidal.μ e.inverse X Y)

Tactic:
simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]

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'
e : C ≌ D
inst✝ : e.functor.Monoidal
this✝ : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this : IsIso (LaxMonoidal.ε e.inverse)
X Y : D
⊢ IsIso
    (e.toAdjunction.unit.app (e.inverse.obj X ⊗ e.inverse.obj Y) ≫
      e.inverse.map
        (OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y) ≫
          (e.toAdjunction.counit.app X ⊗ₘ e.toAdjunction.counit.app Y)))
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
x✝ y✝ : M
⊢ (mapGen ⇑c.mk') (c.mk' x✝) (c.mk' y✝) ↔ ↑d x✝ y✝

Tactic:
mapGen_apply_apply_of_surjective c.mk' (c.ker_mk'_eq.trans_le d.2) c.mk'_surjective

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
x✝ y✝ : M
⊢ ↑d x✝ y✝ ↔ ↑d x✝ y✝
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
x y : M
⊢ ↑(FreeAlgebra.ι R (x + y)) = ↑(FreeAlgebra.ι R x) + ↑(FreeAlgebra.ι R y)

Tactic:
rw [← RingCon.coe_add]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ ↑(FreeAlgebra.ι R (x + y)) = ↑(FreeAlgebra.ι R x + FreeAlgebra.ι R y)
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
inst✝ : Nontrivial R
x : M
⊢ (ι R) x ≠ 1

Tactic:
by
  rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne, ι_eq_algebraMap_iff]
  exact one_ne_zero ∘ And.right

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : tsze R M
r : R
⊢ (x * inl r).snd = (x <• r).snd

Tactic:
by dsimp; rw [smul_zero, zero_add]

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
Y : ModuleCat S
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
s : S
r : R
y : ↑Y
⊢ s • r • y = (RingHom.id R) r • s • y

Tactic:
change s • f r • y = f r • s • y
            rw [← mul_smul, mul_comm, mul_smul]

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
Y : ModuleCat S
y : ↑Y
⊢ (ConcreteCategory.hom (map f)) (1 ⊗ₜ[R] y) = y

Tactic:
change (1 : S) • y = y
  simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
x : A
y : B
| (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) ((TensorProduct.comm S A A) (comul x) ⊗ₜ[R] comul y)

Tactic:
← comm_comul _ y

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Algebra R S
inst✝⁷ : Module R A
inst✝⁶ : Module S A
inst✝⁵ : Module R B
inst✝⁴ : IsScalarTower R S A
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
x : A
y : B
| (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
    ((TensorProduct.comm S A A) (comul x) ⊗ₜ[R] (TensorProduct.comm R B B) (comul y))
Module: Mathlib.CategoryTheory.Adjunction.Unique

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
⊢ adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G = adj2.unit

Tactic:
by
  ext x
  rw [NatTrans.comp_app, ← homEquiv_leftAdjointUniq_hom_app adj1 adj2]
  simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f

Tactic:
by
  rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
P : Type u_3
inst✝⁶ : CommSemiring P
Q : Type u_4
inst✝⁵ : CommSemiring Q
inst✝⁴ : Algebra P Q
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : R), f a = 0 → ∃ n, r ^ n * a = 0
a : R
n : ℕ
ha : f r ^ n * f a = 0
m : ℕ
hm : r ^ m * (r ^ n * a) = 0
⊢ ∃ m, r ^ m * a = 0

Tactic:
exact ⟨m + n, by simp [pow_add, mul_assoc, *]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span s ↔ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ) ↔
    z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)

Tactic:
· refine ⟨(span_mono (by simp only [Set.union_assoc, Set.subset_union_left]) ·), fun h ↦ ?_⟩
    refine mem_span_iff.mp h (span s) ?_
    simp only [union_subset_iff, union_assoc]
    exact ⟨subset_span, subset_mul_set subset_span _, set_mul_subset subset_span _,
      subset_mul_set (set_mul_subset subset_span _) _⟩

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z : R
⊢ z ∈ span (s ∪ s * univ ∪ univ * s ∪ univ * s * univ) ↔
    z ∈ AddSubgroup.closure (s ∪ s * univ ∪ univ * s ∪ univ * s * univ)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ (algebraMap R S) r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥

Tactic:
← (RingHom.ker (algebraMap S T)).map_comap_of_surjective _ h₂,

Goal state after:
case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ (algebraMap R S) r ^ n • Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) (RingHom.ker (algebraMap S T))) ≤ ⊥
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
h : ∃! P, P ≠ ⊥ ∧ P.IsPrime
⊢ ∃! I, I.IsMaximal

Tactic:
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
      refine ⟨P, ⟨⟨hPnot_top, ?_⟩⟩, fun M hM => hPunique _ ⟨?_, Ideal.IsMaximal.isPrime hM⟩⟩
      · refine Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_
        exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm
      · rintro rfl
        exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
I A : C
f : A ⟶ I
hI : IsInitial I
⊢ IsIso f

Tactic:
rw [isIso_iff_of_thin]
    exact ⟨hI.to _⟩

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

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H : b * (algebraMap R B) ↑(a₀, y).2 = (algebraMap R B) (a₀, y).1
⊢ ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b

Tactic:
obtain ⟨d, hy⟩ := (Submonoid.mem_powers_iff y.1 x).mp y.2

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
H : b * (algebraMap R B) ↑(a₀, y).2 = (algebraMap R B) (a₀, y).1
d : ℕ
hy : x ^ d = ↑y
⊢ ∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case commg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ g ≫ e₄.symm.hom = e₃.symm.hom ≫ g'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

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

Goal state before:
pp: case commg
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
⊢ g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'

Tactic:
simp only [Iso.symm_hom, Iso.comp_inv_eq, Category.assoc, ← commg, Iso.inv_hom_id_assoc]

Goal state after:
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
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
⊢ IsLocalization (algebraMapSubmonoid T S) B ↔ IsPushout R T A B

Tactic:
rw [Algebra.IsPushout.comm, Algebra.isPushout_iff, ← isLocalizedModule_iff_isLocalization]

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
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
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap
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
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)

Tactic:
have : IsScalarTower A Aₚ M' := (IsLocalizedModule.iso S g).symm.isScalarTower 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
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this : IsScalarTower A Aₚ M'
⊢ IsLocalizedModule S ((AlgebraTensorModule.rTensor R N) g)
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
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
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : ↑u₁ • ↑t₁ • a₁ = ↑u₁ • ↑s₁ • b₁
u₂ : ↥S
e₂ : ↑u₂ • ↑t₂ • a₂ = ↑u₂ • ↑s₂ • b₂
⊢ (↑u₁ * ↑u₂) • (↑t₁ * ↑t₂) • (a₁ * a₂) = (↑u₁ * ↑u₂) • (↑s₁ * ↑s₂) • (b₁ * b₂)

Tactic:
simp only [mul_smul_mul_comm, e₁, e₂]

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

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
⊢ IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) (S ⊗[R] B)

Tactic:
by
  change IsLocalization (Algebra.algebraMapSubmonoid _ M) (S ⊗[R] B)
  let : Algebra A (S ⊗[R] B) := .compHom _ (algebraMap A B)
  have : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B) := .of_algebraMap_eq' H.symm
  have : IsScalarTower R A (S ⊗[R] B) :=
    .of_algebraMap_eq' <| by
      rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]
  have : IsScalarTower R (S ⊗[R] A) (S ⊗[R] B) := .to₁₃₄ _ A _ _
  have : IsScalarTower A B (S ⊗[R] B) := .of_algebraMap_eq' rfl
  rw [Algebra.isLocalization_iff_isPushout _ B, Algebra.IsPushout.comm,
    ← Algebra.IsPushout.comp_iff R _ S]
  infer_instance

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:
dsimp [FreeCommRing]
  rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]

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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
p : M
s : ↥S
h : (p, s).2 • x = f (p, s).1
⊢ ∃ x_1, x_1.2 • x = (f ∘ₗ ↑e) x_1.1

Tactic:
exact ⟨⟨e.symm p, s⟩, by simpa using h⟩

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
m : M'
⊢ (iso S f) ((iso S f).symm m) = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)

Tactic:
rw [LinearEquiv.apply_symm_apply]

Goal state after:
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
m : M'
⊢ m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
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
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ (L.map (h₁.lift ((fst L R).mapCone s)) ≫ c.pt.hom) ≫ (R.mapCone ((snd L R).mapCone c)).π.app j =
    (s.pt.hom ≫ R.map (h₂.lift ((snd L R).mapCone s))) ≫ (R.mapCone ((snd L R).mapCone c)).π.app j

Tactic:
by
        simp [← Functor.map_comp, ← Functor.map_comp_assoc, ← CommaMorphism.w,
          dsimp% h₂.fac ((snd _ _).mapCone s) j,
          dsimp% h₁.fac ((fst _ _).mapCone s) j]

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
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s

Tactic:
rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]

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_6
M' : Type u_7
N : Type u_8
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : AddCommGroup N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ (m : M), g (f m) = 0 → f m = 0
⊢ Function.Injective ⇑g

Tactic:
refine IsLocalizedModule.injective_of_map_eq S f (fun hxy ↦ ?_)
  rw [← sub_eq_zero, ← map_sub]
  apply H
  simpa [sub_eq_zero]

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

Goal state before:
pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        ofHom
          ((RingHom.fst ↑A ↑B).comp
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
      s.fst

Tactic:
intro s
    ext x
    rfl

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

Goal state before:
pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g),
    ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
        ofHom
          ((RingHom.snd ↑A ↑B).comp
            (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
      s.snd

Tactic:
intro s
    ext x
    rfl

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

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
⊢ ∀ (s : PullbackCone f g)
    (m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))),
    m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
        s.fst →
      m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
          s.snd →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)

Tactic:
intro s m e₁ e₂

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
⊢ m =
    ofHom
      (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
        (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) ≫ F.mapComp g✝ h = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h

Tactic:
F.mapComp_naturality_left

Goal state after:
B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h