mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ≠ 0 ∧
    (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
    simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝ : Fintype m
⊢ P M

Tactic:
cases nonempty_fintype n

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P M
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val✝ : Fintype m
⊢ f = g

Tactic:
cases nonempty_fintype n

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ f = g
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ (n • s).toFinset ∪ (1 • s).toFinset = s.toFinset

Tactic:
one_nsmul,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ (n • s).toFinset ∪ s.toFinset = s.toFinset
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) 0) = 0

Tactic:
by rw [map_zero, map_zero]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
by
  have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
  rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h,
    Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]
  exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³ * x✝², ⋯⟩

Tactic:
by convert! congr_arg₂ (· * ·) h₁ h₂ <;> rw [← map_mul] <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι →₀ M
g : κ →₀ R
a : ι
b : κ
⊢ ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a

Tactic:
by
  simp [finsuppTensorFinsuppRid]

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : ι
b : κ
m : M
r : R
⊢ (finsuppTensorFinsuppRid R M ι κ) (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m)

Tactic:
by
  simp [finsuppTensorFinsuppRid]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ star (z * x) = star (x * y) ↔ x * y = z * x

Tactic:
star_inj,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ z * x = x * y ↔ x * y = z * x
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
⊢ Mᵀ.updateRow j c = (M.updateCol j c)ᵀ

Tactic:
by
  ext
  rw [transpose_apply, updateRow_apply, updateCol_apply]
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
⊢ Mᵀ.updateCol i b = (M.updateRow i b)ᵀ

Tactic:
by
  ext
  rw [transpose_apply, updateRow_apply, updateCol_apply]
  rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ ∑ j, A (↑i) j * B j ↑k = (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i ↦ ¬q i) * B.toBlock (fun i ↦ ¬q i) r) i k

Tactic:
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Goal state after:
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₁ v₃) (f ∘ₗ g) = (toMatrix v₂ v₃) f * (toMatrix v₁ v₂) g

Tactic:
simp_rw [LinearMap.toMatrix, LinearEquiv.trans_apply]
  rw [LinearEquiv.arrowCongr_comp _ v₂.equivFun, LinearMap.toMatrix'_comp]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ (toLinAlgEquiv v₁) ((toMatrixAlgEquiv v₁) f) = f

Tactic:
by
  rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ (toLinAlgEquiv v₁).symm ((toLinAlgEquiv v₁) M) = M

Tactic:
AlgEquiv.symm_apply_apply

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
⊢ M = M
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
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
let sI_basis : Basis I R N := Basis.span indepI

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
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
⊢ (n : ℕ) × Basis (Fin n) R M
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℤ
⊢ (algebraMap ℤ ℚ) x = (algebraMap ℤ ℚ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [eq_intCast, eq_intCast, Int.cast_inj]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℤ
⊢ x = y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₁ T) ((algebraMap R S₁) r) = (algebraMap S₁ T) (y * (algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
hs,

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₁ T) ((algebraMap R S₁) r) = (algebraMap S₁ T) ((algebraMap R S₁) s)
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * x * (algebraMap R S₁) ↑d = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * y * (algebraMap R S₁) ↑d

Tactic:
rw [mul_assoc, hr, mul_assoc, hs]

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) (c * r) = (algebraMap R S₂) (c * s)
a : ↥M₂
ha : ↑a * (c * r) = ↑a * (c * s)
⊢ ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) r = ↑⟨(algebraMap R S₁) ↑a, ⋯⟩ * (algebraMap R S₁) s
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x₁ x₂ : N ⊗[R] M
ihx₁ : ∃ J, ∃ (_ : J.FG), ∃ y, x₁ = (rTensor M J.subtype) y
ihx₂ : ∃ J, ∃ (_ : J.FG), ∃ y, x₂ = (rTensor M J.subtype) y
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, x₁ + x₂ = (rTensor M J.subtype) y

Tactic:
obtain ⟨J₁, fg₁, y₁, rfl⟩ := ihx₁

Goal state after:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x₂ : N ⊗[R] M
ihx₂ : ∃ J, ∃ (_ : J.FG), ∃ y, x₂ = (rTensor M J.subtype) y
J₁ : Submodule R N
fg₁ : J₁.FG
y₁ : ↥J₁ ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, (rTensor M J₁.subtype) y₁ + x₂ = (rTensor M J.subtype) y
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
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : Rₘ
⊢ ((↑(algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ)) x = ((algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')) x

Tactic:
by
  rw [algEquiv_comp_algebraMap M Rₘ Sₙ Rₘ']

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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * (↑⟨m, hm⟩ * n)) = (algebraMap R Rₘ) r

Tactic:
hn,

Goal state after:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ (algebraMap R Rₘ) (r * 1) = (algebraMap R Rₘ) r
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 1) (Submodule.span R ↑s))

Tactic:
hs,

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A ↑(Submodule.map ((TensorProduct.mk R A M) 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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) ↑y * mk' Rₘ x y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)

Tactic:
IsLocalization.mul_mk'_eq_mk'_of_mul

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = (algebraMap Rₘ Sₘ) ((algebraMap R Rₘ) x)
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
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm

Goal state after:
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'
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Semiring α

Tactic:
apply e.injective.semiring _

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n
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ˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [mul_smul_comm, ← smul_mul_assoc, smul_sub, smul_inv_smul, h.mul_val_inv]

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

Goal state before:
pp: case refine_2.refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ ∀ (x : A) (y : B), a₁ ⊗ₜ[R] b₁ * x ⊗ₜ[R] y = x ⊗ₜ[R] y * a₁ ⊗ₜ[R] b₁

Tactic:
intro a₂ b₂

Goal state after:
case refine_2.refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
a₂ : A
b₂ : B
⊢ a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] b₂ = a₂ ⊗ₜ[R] b₂ * a₁ ⊗ₜ[R] b₁
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

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

Tactic:
rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

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

Goal state before:
pp: R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Set.RightInvOn e (⇑(algebraMap R₁ R₃)) (quasispectrum R₃ a)

Tactic:
by
    convert! hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
    congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (x y : A), (x + y) • baseChangeHom R A M N = x • baseChangeHom R A M N + y • baseChangeHom R A M N

Tactic:
simp only [add_smul, forall_true_iff]

Goal state after: