mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inl
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol k (Pi.single k x) j k = 0

pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
· rw [updateCol_self, Pi.single_eq_of_ne hjk]

Goal state after:
case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₙₐ[R] A₂
⊢ (fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f) =
    f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₙₐ[R] A₂'
⊢ (fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f) =
    f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₐ[R] A₂
⊢ (fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom)
      ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom) f) =
    f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₐ[R] A₂'
⊢ (fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom)
      ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom) f) =
    f

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
by
  simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]
  conv_rhs => rw [← span_singleton_generator I, Submodule.span_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
Q : Type uQ
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module A M
inst✝⁹ : Module B M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : IsScalarTower R B M
inst✝⁶ : SMulCommClass A B M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
⊢ (lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N) = ↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) =
    LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) =
    LinearMap.id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A id = id

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ baseChange A (g ∘ₗ f) = baseChange A g ∘ₗ baseChange A f

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_7
B : Type u_8
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : M →ₗ[R] N
⊢ baseChange B (baseChange A f) = ↑(cancelBaseChange R A B B N).symm ∘ₗ baseChange B f ∘ₗ ↑(cancelBaseChange R A B B M)

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
⊢ baseChange A (f * g) = baseChange A f * baseChange A g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u_1
x y : α
h : Function.Injective ![x, y]
⊢ x ≠ y

Tactic:
simpa using h.ne Fin.zero_ne_one

Goal state after:
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
n : ℕ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
let inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℕ) (R := R) (X := X) (S := S)

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
n : ℕ
x : OreLocalization S X
inst : Module ℕ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (∑ x, if ij.1 = x ∧ ij.2 = k then b₂ x else 0) = if ij.2 = k then b₂ ij.1 else 0

Tactic:
ite_and,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (∑ x, if ij.1 = x then if ij.2 = k then b₂ x else 0 else 0) = if ij.2 = k then b₂ ij.1 else 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun i j ↦ { toFun := fun x ↦ (f * g) (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) * fun i j ↦
      { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply,
      LinearMap.coe_sum, Finset.sum_apply]
    rw [← Fintype.sum_apply, ← map_sum]
    exact congr_arg₂ _ (by aesop) rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
⊢ (fun i j ↦ { toFun := fun x ↦ (f + g) (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) + fun i j ↦
      { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext; simp

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 y : ↥M
⊢ mk' S (↑x) y * mk' S (↑y) x = 1

Tactic:
rw [← mk'_mul, mul_comm]

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 y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1
Module: Mathlib.RingTheory.Localization.Basic

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
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'

Tactic:
simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
ext; simp

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
ext; simp

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

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ringEquivOfRingEquiv (RingEquiv.refl A) = RingEquiv.refl K

Tactic:
ext; simp

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

Goal state before:
pp: A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsFractionRing B L
C : Type u_12
M : Type u_13
inst✝³ : CommRing C
inst✝² : CommRing M
inst✝¹ : Algebra C M
inst✝ : IsFractionRing C M
f : A ≃+* B
g : B ≃+* C
⊢ ringEquivOfRingEquiv (f.trans g) = (ringEquivOfRingEquiv f).trans (ringEquivOfRingEquiv g)

Tactic:
by
  ext a
  simp [IsLocalization.map_map]

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

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
a b : (A ⧸ R') ⊗[R] (A ⧸ R')
e₁ : a = 0
e₂ : b = 0
⊢ a + b = 0

Tactic:
| add a b e₁ e₂ =>

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft

Tactic:
ext; simp

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l).range ≤ Submodule.span A ↑l.range

Tactic:
rintro _ ⟨x, rfl⟩
    induction x using TensorProduct.induction_on
    · simp
    · rw [LinearMap.liftBaseChange_tmul]
      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)
    · rw [map_add]
      exact add_mem ‹_› ‹_›

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x y : A ⊗[R] B
⊢ r • (x * y) = x * r • y

Tactic:
induction y with
    | zero => simp [smul_zero]
    | tmul a b => induction x with
      | zero => simp [smul_zero]
      | tmul a' b' =>
        dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
      | add x y hx hy => simp [smul_add, add_mul _, *]
    | add x y hx hy => simp [smul_add, mul_add _, *]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
⊢ mulLeft R (a ⊗ₜ[R] b) = map (mulLeft R a) (mulLeft R b)

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : SMulCommClass R A A
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R A A
inst✝ : IsScalarTower R B B
a : A
b : B
⊢ mulRight R (a ⊗ₜ[R] b) = map (mulRight R a) (mulRight R b)

Tactic:
ext; simp

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

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
      ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f) =
    f

Tactic:
ext; simp

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

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
⊢ (restrictScalars R
          ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯)
            ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight) f))).comp
      Algebra.TensorProduct.includeRight =
    (restrictScalars R f).comp Algebra.TensorProduct.includeRight

Tactic:
ext; simp

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

Goal state before:
pp: case e'_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ 1 = 1 + ↑0

Tactic:
· simp only [inr_zero, add_zero]

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

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv x * equiv y = 1

pp: case mpr.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv y * equiv x = 1

Tactic:
all_goals
      apply equiv.symm.injective
      assumption

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C✝ : Type uC
D : Type uD
E : Type uE
F : Type uF
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✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝ : B →ₐ[R] C
⊢ (fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) ((fun f ↦ lift (ofId S C) f ⋯) x✝) = x✝

Tactic:
ext; simp

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C✝ : Type uC
D : Type uD
E : Type uE
F : Type uF
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✝
inst✝⁷ : Semiring D
inst✝⁶ : Algebra R D
inst✝⁵ : Algebra R C✝
inst✝⁴ : IsScalarTower R S C✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝ : S ⊗[R] B →ₐ[S] C
⊢ (fun f ↦ lift (ofId S C) f ⋯) ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) x✝) = x✝

Tactic:
ext; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap =
    LinearMap.lTensor S (Algebra.linearMap R B)

Tactic:
ext; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
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
⊢ (↑(TensorProduct.rid R S A)).comp includeLeftRingHom = RingHom.id A

Tactic:
ext; simp

Goal state after: