mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Rel R M ≤ ⇑(RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom)

Tactic:
intro x y h

Goal state after:
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
x y : FreeAlgebra R M
h : Rel R M x y
⊢ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) 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
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ Algebra.adjoin R (⇑((lift R) f) '' Set.range ⇑(ι R)) = Algebra.adjoin R (Set.range ⇑f)

Tactic:
← Set.range_comp,

Goal state after:
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
⊢ Algebra.adjoin R (Set.range (⇑((lift R) f) ∘ ⇑(ι R))) = Algebra.adjoin R (Set.range ⇑f)
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
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (x ^ n).snd = n •> x.fst ^ n.pred •> x.snd

Tactic:
snd_pow_eq_sum,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
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
inst✝ : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x ^ (n + 1)).snd = (x ^ n).fst •> x.snd + (x ^ n).snd <• x.fst

Tactic:
snd_pow_eq_sum,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
n : ℕ
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (List.map (fun i ↦ x.fst ^ ((n + 1).pred - i) •> x.snd <• x.fst ^ i) (List.range (n + 1))).sum =
    (x ^ n).fst •> x.snd + (List.map (fun i ↦ x.fst ^ (n.pred - i) •> x.snd <• x.fst ^ i) (List.range n)).sum <• x.fst
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ x * (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = 1

Tactic:
convert! mul_right_eq_one _ _ (mul_invOf_self x.fst)

Goal state after:
R : Type u
M : Type v
inst✝⁵ : AddCommGroup M
inst✝⁴ : Semiring R
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : Module R M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ f.range ⊔ Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)

Tactic:
← Set.range_comp,

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ f.range ⊔ Algebra.adjoin S (Set.range (⇑(lift f g hg hfg hgf) ∘ inr)) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)
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
s : S
g : X ⟶ (restrictScalars f).obj Y
⊢ ∀ (x y : ↑X), s • (ConcreteCategory.hom g) (x + y) = s • (ConcreteCategory.hom g) x + s • (ConcreteCategory.hom g) y

Tactic:
by
        intros
        dsimp only
        rw [map_add, smul_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
r : R
s : S
⊢ { toFun := fun y ↦ (r • s) • y, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) r • { toFun := fun y ↦ s • y, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
          ext y
          change (f r • s) • y = (f r) • s • y
          rw [smul_eq_mul, mul_smul]

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₂
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]
  ext
  rfl

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
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.inv ≫ ε = ε

Tactic:
by simp [Iso.inv_comp_eq]

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
f : M ≅ N
inst✝ : IsComonHom f.hom
⊢ f.inv ≫ Δ = Δ ≫ (f.inv ⊗ₘ f.inv)

Tactic:
by simp [Iso.inv_comp_eq]

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap R T) a = (algebraMap R T) b
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b

Tactic:
repeat rw [IsScalarTower.algebraMap_apply R S T] at h

Goal state after:
case refine_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
⊢ ∃ n, (y * x) ^ n * a = (y * x) ^ n * b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I : TwoSidedIdeal S
x : R
⊢ x ∈ (comap f) I ↔ f x ∈ I

Tactic:
by
  simp [comap, RingCon.comap, mem_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I) ↔ z ∈ I

Tactic:
refine ⟨fun h ↦ h I fun x hx ↦ ?mem_closure_of_forall, fun hz J hJ ↦ ?mem_ideal_of_subset⟩

Goal state after:
case mem_closure_of_forall
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
h : ∀ (I : TwoSidedIdeal R), s ⊆ ↑I → z ∈ I
x : R
hx : x ∈ s
⊢ x ∈ ↑I

case mem_ideal_of_subset
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
hz : z ∈ I
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
⊢ z ∈ J

Tactic:
simp only [I, SetLike.mem_coe, mem_mk'] at hz

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
hz : z ∈ closure s
⊢ z ∈ J
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
b : S
⊢ IsUnit b ∨ IsUnit (1 - b)

Tactic:
obtain ⟨a, rfl⟩ := hf b

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
a : R
⊢ IsUnit (f a) ∨ IsUnit (1 - f 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 : μ = μ
this : η = η
⊢ h₁ = h₂

Tactic:
by cases h₁; cases h₂; subst H this; rfl

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

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
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ ↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l) = (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)

Tactic:
← LinearEquiv.comp_toLinearMap_symm_eq

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_5
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
M' : Type u_3
N' : Type u_4
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
g₁ : M →ₗ[R] M'
g₂ : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S g₁
inst✝ : IsLocalizedModule S g₂
l : M →ₗ[R] N
⊢ (↑(IsLocalizedModule.iso S g₂) ∘ₗ ↑R ((map S) l)) ∘ₗ ↑(IsLocalizedModule.iso S g₁).symm =
    (IsLocalizedModule.map S g₁ g₂) l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: 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
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ fst = pullback.fst f g

Tactic:
by simp [Iso.inv_comp_eq]

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

Goal state before:
pp: 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
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ snd = pullback.snd f g

Tactic:
by simp [Iso.inv_comp_eq]

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

Goal state before:
pp: 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
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
⊢ IsLimit sq.cone

Tactic:
refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by cat_disch)

Goal state after:
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
inst✝¹ : IsIso fst
inst✝ : Mono g
sq : CommSq fst snd f g
s : PullbackCone f g
⊢ (s.fst ≫ inv fst) ≫ snd = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryProduct A X
inst✝ : HasBinaryProduct B X
s : PullbackCone f prod.fst
m : s.pt ⟶ A ⨯ X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m ≫ prod.snd = prod.lift s.fst (s.snd ≫ prod.snd) ≫ prod.snd

Tactic:
· simp [← h₂]

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
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'
h : IsBaseChange A f
this✝ : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x✝ : M
⊢ f x✝ = h.equiv (1 ⊗ₜ[R] x✝)

Tactic:
IsBaseChange.equiv_tmul,

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'
h : IsBaseChange A f
this✝ : Module A (LocalizedModule S M) := LocalizedModule.moduleOfIsLocalization
this : IsBaseChange A (LocalizedModule.mkLinearMap S M)
e : LocalizedModule S M ≃ₗ[R] M' := LinearEquiv.restrictScalars R (this.equiv.symm ≪≫ₗ h.equiv)
x✝ : M
⊢ f x✝ = 1 • f x✝
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
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
⊢ IsLocalizedModule S ↑(IsScalarTower.toAlgHom R T (A ⊗[R] T))

Tactic:
rw [isLocalizedModule_iff_isBaseChange (S := S) (A := A)]
  exact TensorProduct.isBaseChange _ _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
n : ℕ
a : A
s : ↥S
⊢ mk a s ^ n = mk (a ^ n) (s ^ n)

Tactic:
induction n with
  | zero =>
    rw [pow_zero, pow_zero, pow_zero, OreLocalization.one_def]
  | succ n ih =>
    simp only [pow_succ', ih, LocalizedModule.mk_mul_mk]

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

Goal state before:
pp: case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • r • t • m = a • t • r • m

Tactic:
smul_comm r t

Goal state after:
case h.h.mp
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
⊢ a • t • r • m = a • t • r • m
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₁✝ x₂✝ : M
h : (↑e ∘ₗ f) x₁✝ = (↑e ∘ₗ f) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      EmbeddingLike.apply_eq_iff_eq] at h
    exact hf.exists_of_eq h

Goal state after:
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.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X) ≫ T.map (retraction (T.η.app X))

Tactic:
T.map_unit_app X,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.η.app (T.obj X) ≫ T.map (retraction (T.η.app X))
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv

Tactic:
ext (x : S)

Goal state after:
case h₁
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
x : ↑S
⊢ (Hom.hom
        ((pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
            Under.Hom.right
              ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
          Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv))
      x =
    (Hom.hom
        ((pushout.inr A.hom (ofHom (algebraMap ↑R ↑S)) ≫
            Under.Hom.right
              ((tensorProdObjIsoPushoutObj S A).inv ≫
                (tensorProdObjIsoPushoutObj S A).hom ≫
                  Under.homMk
                    (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                      (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                    ⋯)) ≫
          Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv))
      x
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''
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
g : M' →ₗ[R] M''
inst✝ : IsLocalizedModule S (g ∘ₗ f)
⊢ ↑(linearEquiv S f (g ∘ₗ f)) = g

Tactic:
by
  refine ext S f (IsLocalizedModule.map_units (g ∘ₗ f)) ?_
  ext
  simp

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
s : ↥S
⊢ mk' f 0 s = 0

Tactic:
← zero_smul R (0 : M),

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
s : ↥S
⊢ mk' f (0 • 0) s = 0
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case zero
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
exact ⟨zero, 𝟙 _, 𝟙 _, inferInstance, by simp⟩

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

Goal state before:
pp: case exists_of_eq
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ {x₁ x₂ : S}, f.toLinearMap x₁ = f.toLinearMap x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
intro x y
    dsimp only [AlgHom.toLinearMap_apply]
    rw [← sub_eq_zero, ← map_sub, h₃]
    simp_rw [smul_sub, sub_eq_zero]
    exact id

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Finset R
inst✝ : (span ↑s).IsTwoSided
t : Finset M
⊢ (Submodule.span R ↑(s • t)).FG

Tactic:
exact ⟨_, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG) → FinitePresentation R A

Tactic:
rintro ⟨ι, hfintype, f, hf⟩

Goal state after:
case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ FinitePresentation R A