mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map f (r • g)))) x✝¹) x✝ = ((TensorProduct.curry (↑R (r • map f g))) x✝¹) x✝

Tactic:
TensorProduct.curry_apply,

Goal state after:
R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (↑R (map f (r • g))) (x✝¹ ⊗ₜ[R] x✝) = (↑R (r • map f g)) (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((TensorProduct.curry (↑R (map (b • f) g))) x✝¹) x✝ = ((TensorProduct.curry (↑R (b • map f g))) x✝¹) x✝

Tactic:
TensorProduct.curry_apply,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (↑R (map (b • f) g)) (x✝¹ ⊗ₜ[R] x✝) = (↑R (b • map f g)) (x✝¹ ⊗ₜ[R] x✝)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ Subsingleton (OreLocalization S R) ↔ 0 ∈ S

Tactic:
rw [← subsingleton_iff_zero_eq_one, OreLocalization.one_def,
    OreLocalization.zero_def, oreDiv_eq_iff]

Goal state after:
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ (∃ u v, u • 1 = v • 0 ∧ ↑u * ↑1 = v * ↑1) ↔ 0 ∈ S
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r : R
s : ↥S
⊢ (r /ₒ s) • (0 /ₒ 1) = 0 /ₒ 1

Tactic:
smul_div_one,

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r : R
s : ↥S
⊢ r • 0 /ₒ s = 0 /ₒ 1
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
⊢ ms.1 ≠ 0

Tactic:
refine fun h ↦ hn ?_

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h : ms.1 = 0
⊢ n = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ toMatrix' ((v₁.equivFun.arrowCongr v₃.equivFun) (f ∘ₗ g)) =
    toMatrix' ((v₂.equivFun.arrowCongr v₃.equivFun) f) * toMatrix' ((v₁.equivFun.arrowCongr v₂.equivFun) g)

Tactic:
LinearEquiv.arrowCongr_comp _ v₂.equivFun,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
f : M₂ →ₗ[R] M₃
g : M₁ →ₗ[R] M₂
⊢ toMatrix' ((v₂.equivFun.arrowCongr v₃.equivFun) f ∘ₗ (v₁.equivFun.arrowCongr v₂.equivFun) g) =
    toMatrix' ((v₂.equivFun.arrowCongr v₃.equivFun) f) * toMatrix' ((v₁.equivFun.arrowCongr v₂.equivFun) g)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₁ v₁) 1) x = x

Tactic:
Matrix.toLin_one,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ LinearMap.id x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ ((toLin v₂ v₂) 1) x = x

Tactic:
Matrix.toLin_one,

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝³ : Fintype m
M₃ : Type u_7
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
v₃ : Basis l R M₃
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₂
⊢ LinearMap.id x = x
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * x = x * (numeratorRingHom.comp (algebraMap R₀ R)) r

Tactic:
induction x using OreLocalization.ind with | _ r₁ s₁

Goal state after:
case c
R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (numeratorRingHom.comp (algebraMap R₀ R)) r * (r₁ /ₒ s₁) = r₁ /ₒ s₁ * (numeratorRingHom.comp (algebraMap R₀ R)) r
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = (algebraMap R₀ R) r /ₒ 1 * x

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
S : Submonoid R
inst✝⁴ : OreSet S
X : Type u_2
inst✝³ : AddCommMonoid X
inst✝² : Module R X
R₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
x : OreLocalization S R
⊢ r • x = r • 1 /ₒ 1 * x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
⊢ (toMatrix b b) ((lmul R S) 1) = 1

Tactic:
rw [map_one, LinearMap.toMatrix_one]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI₁ : Module.Finite R ↥I
hI₂ : IsTorsionFree R ↥I
this : Module.Finite R ↥(restrictScalars R I)
⊢ Free R ↥I

Tactic:
have : IsTorsionFree R (restrictScalars R I) := hI₂

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal S
hI₁ : Module.Finite R ↥I
hI₂ : IsTorsionFree R ↥I
this✝ : Module.Finite R ↥(restrictScalars R I)
this : IsTorsionFree R ↥(restrictScalars R I)
⊢ Free R ↥I
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
m : ↥N
i : Fin n
⊢ (⇑(snf.bM.repr ↑m) ∘ ⇑snf.f) i = (snf.a • ⇑(snf.bN.repr m)) i

Tactic:
simp [Pi.smul_apply (snf.a i)]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
m : ↥N
⊢ (snf.bM.coord (snf.f i) ∘ₗ N.subtype) m = (snf.a i • snf.bN.coord i) m

Tactic:
simp [Pi.smul_apply (snf.a i)]

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

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
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ x = 0

Tactic:
← mk'_sec (M := M) S x,

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
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ mk' S (sec M x).1 (sec M x).2 = 0
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w * ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

Tactic:
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.domRestrict M) h y),
    mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
    IsUnit.coe_liftRight]
  simp [RingHom.toMonoidHom_eq_coe, MonoidHom.domRestrict_apply]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
⊢ ∃ a, (Algebra.ofId R S) a = y

Tactic:
obtain ⟨⟨x, s⟩, eq⟩ := IsLocalization.surj M y

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ a, (Algebra.ofId R S) a = y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case map_units
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (y : ↥(Submonoid.map h M)), IsUnit ((algebraMap P S) ↑y)

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩⟩
    convert! IsLocalization.map_units S ⟨y, hy⟩
    dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]
    exact congr_arg _ (h.symm_apply_apply _)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
x✝ y✝ : R
eq : (algebraMap R K) x✝ = (algebraMap R K) y✝
⊢ ↑1 * x✝ = ↑1 * y✝

Tactic:
by simpa using inj eq

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsFractionRing R R ↔ R⁰ ≤ IsUnit.submonoid R

Tactic:
rw [self_iff_nonZeroDivisors_eq_isUnit, le_antisymm_iff,
    and_iff_left (isUnit_le_nonZeroDivisors R)]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : adjoin R (⇑(algebraMap A B) '' s) = (IsScalarTower.toAlgHom R A B).range
⊢ Subalgebra.restrictScalars R (adjoin A t) =
    Subalgebra.restrictScalars R (adjoin (↥(IsScalarTower.toAlgHom R A B).range) t)

Tactic:
← IsScalarTower.adjoin_range_toAlgHom

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
this : adjoin R (⇑(algebraMap A B) '' s) = (IsScalarTower.toAlgHom R A B).range
⊢ Subalgebra.restrictScalars R (adjoin (↥(IsScalarTower.toAlgHom R A B).range) t) =
    Subalgebra.restrictScalars R (adjoin (↥(IsScalarTower.toAlgHom R A B).range) t)
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s) ∪ f '' Fin.val ⁻¹' {sSup s}) =
    Submodule.span R (f '' {⟨sSup s, ⋯⟩} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s))

Tactic:
Set.union_comm

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
n : ℕ
f : Fin n → M
hf : Submodule.span R (Set.range f) = ⊤
s : Set ℕ := {m | Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m) ≠ ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s))) = ⊤
⊢ Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)) =
    Submodule.span R (f '' {⟨sSup s, ⋯⟩} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s))
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ 1 ⊗ₜ[R] (a • (1 / f b)) = f a ⊗ₜ[R] (1 / f b)

Tactic:
rw [← smul_tmul, algebraMap_eq_smul_one a]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (r • 1)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (↑ₐ ↑r - ↑a)
⊢ IsUnit (↑ₐ ↑r⁻¹ - ↑a⁻¹)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (↑r • 1 - ↑a)
⊢ IsUnit (↑r⁻¹ • 1 - ↑a⁻¹)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r s : R
⊢ r + s ∈ σ (↑ₐ s + a) ↔ r ∈ σ a

Tactic:
by
  rw [add_mem_iff, neg_add_cancel_left]

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (↑ₐ 1)

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (1 • 1)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra R B
z : ℤ
⊢ ↑z = 1 ⊗ₜ[R] ↑z

Tactic:
by
  rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)

Tactic:
by
    simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (algebraMap R S) x ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (x • 1) ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
s : S
r : R
⊢ s ⊗ₜ[R] (algebraMap R T) r ∈ ↑((mk R S T).flip 1).range

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
s : S
r : R
⊢ s ⊗ₜ[R] (r • 1) ∈ ↑((mk R S T).flip 1).range
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
x✝³ : A
x✝² : B
x✝¹ : A
x✝ : B
⊢ f ((x✝³ * x✝¹) ⊗ₜ[R] (x✝² * x✝)) = f (x✝³ ⊗ₜ[R] x✝²) * f (x✝¹ ⊗ₜ[R] x✝)

Tactic:
exact hf _ _ _ _

Goal state after:
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl ((algebraMap S R) s) * inl r✝ + inl ((algebraMap S R) s) * ↑a✝

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • 1) * inl r✝ + inl (s • 1) * ↑a✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (algebraMap R A) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (r • 1)