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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_11
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
h : Function.Surjective ⇑(algebraMap R A)
a : A
m : M
n : N
⊢ (a • m) ⊗ₜ[R] n = m ⊗ₜ[R] (a • n)

Tactic:
by
    obtain ⟨r, rfl⟩ := h a
    simp [smul_tmul]

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
x : M₁'
i : ι₂
y : M₂ i
⊢ (directSumRight R S M₁' M₂) (x ⊗ₜ[R] (lof R ι₂ M₂ i) y) = (lof S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)

Tactic:
simpa [directSumRight] using! lequivCongrLeft_lof S (by simp) _ _ rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ b'.repr ((b.prod b') (Sum.inl i)).2 = b'.repr 0

Tactic:
ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply,
      LinearEquiv.prodCongr_symm, LinearEquiv.prodCongr_apply, b'.repr.apply_symm_apply,
      LinearEquiv.symm_symm, Finsupp.snd_sumFinsuppLEquivProdFinsupp,
      map_zero, Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

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

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
⊢ vecCons x v ᵥ* of B = x • vecHead B + v ᵥ* of (vecTail B)

Tactic:
by
  ext i
  simp [vecMul]

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

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
⊢ v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B

Tactic:
by
  ext i
  simp [vecMul]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s

Tactic:
rw [← hm, Finset.sdiff_singleton_eq_erase, ← Finset.mul_prod_erase _ _ hrS]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ (AlgebraTensorModule.map LinearMap.id p.subtype).range ≤ baseChange A q

Tactic:
← subtype_comp_inclusion p q h,

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : p ≤ q
⊢ (AlgebraTensorModule.map LinearMap.id (q.subtype ∘ₗ inclusion h)).range ≤ baseChange A q
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
⊢ ϕ ⟨y', y'M⟩ ≠ 0

Tactic:
simpa only [ϕy'_eq] using one_ne_zero

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ⊆ ↑t ↔ s ≤ t
⊢ ↑(sInf S) = ⨅ x ∈ S, ↑x

Tactic:
exact coe_sInf _

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ -x + x = 0

Tactic:
induction x with | _ r s; simp

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

Goal state before:
pp: case neg.intro.refine_2.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i✝ : Fin (n' + 1)
i : Fin n'
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i.succ) =
    Fin.cons a as i.succ • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i).succ)

Tactic:
simp only [Fin.cons_succ, Function.comp_apply, coe_inclusion, h 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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ((toLocalizationMap M S).lift hg) z * w + w' = v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg,
    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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case surj
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)

Goal state after:
case surj
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e : h.symm y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
⊢ ∃ x, y * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
S : Type u_2
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
K : Type u_6
L : Type u_7
inst✝⁹ : Field K
inst✝⁸ : Semiring L
inst✝⁷ : Nontrivial L
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : Algebra S L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : IsScalarTower R K L
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
centralizer,

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, m * c = c * m} = {c | ∀ m ∈ star s, m * c = c * m}
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
⊢ f.toLinearMap = g.toLinearMap

Tactic:
ext a b

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Semiring C
inst✝⁶ : Algebra R C
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S A
inst✝³ : Algebra R S
inst✝² : Algebra S C
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S C
f g : A ⊗[R] B →ₐ[S] C
ha : f.comp includeLeft = g.comp includeLeft
hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight
a : A
b : B
⊢ ((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
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✝³ : AddCommGroupWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑↑n ⊗ₜ[R] 1 = ↑n

Tactic:
simp [natCast_def]

Goal state after:
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 b : A
⊢ {r | IsUnit r} ∩ σ (a * b) = {r | IsUnit r} ∩ σ (b * a)

Tactic:
ext r

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
⊢ r ∈ {r | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r | IsUnit r} ∩ σ (b * a)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
u : Aˣ
⊢ spectrum R (↑u⁻¹ * a * ↑u) = spectrum R a

Tactic:
by
  simpa using spectrum.units_conjugate (u := u⁻¹)

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ IsUnit (equiv x)

Tactic:
simp only [IsQuasiregular, IsUnit, Equiv.apply_symm_apply,
    ← PreQuasiregular.equiv (R := R).injective.eq_iff]

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
ext r

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ quasispectrum R a = spectrum R ↑a

Tactic:
ext r

Goal state after:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R a = spectrum R ↑a

Tactic:
ext r

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Tactic:
Unitization.quasispectrum_eq_spectrum_inr' _ S a,

Goal state after:
S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ spectrum S ↑a ↔ r ∈ spectrum R ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
⊢ quasispectrum R a = ⋃ i, quasispectrum R (a i)

Tactic:
ext r

Goal state after:
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ ⋃ i, quasispectrum R (a i)
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
⊢ (quasispectrum R (a, b))ᶜ = (quasispectrum R a ∪ quasispectrum R b)ᶜ

Tactic:
ext r

Goal state after:
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
r : R
⊢ r ∈ (quasispectrum R (a, b))ᶜ ↔ r ∈ (quasispectrum R a ∪ quasispectrum R b)ᶜ
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
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
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ ⇑includeLeft ∘ ⇑(TensorProduct.rid R S A) = ⇑(map (AlgHom.id R A) (ofId R B))

Tactic:
exact DFunLike.coe_fn_eq.mpr this

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R (id '' s)).mkQ ∘ id) t

Tactic:
by
    rw [image_id]
    exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))

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

Goal state before:
pp: R : Type u_1
A : Type u_2
a b : ℕ
this : AddSubmonoid.closure (range fun x ↦ x * x) = ⊤
⊢ a ≤ b ↔ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), b = a + p

Tactic:
simp [this, le_iff_exists_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : ⊤ ≤ span K t
⊢ range ⇑(extendLe hs hst ht) = hs.extend hst

Tactic:
rw [coe_extendLe, Subtype.range_coe_subtype, ofPred_mem_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R✝ : Type u
M✝ : Type v
ι : Type w
inst✝⁹ : Semiring R✝
inst✝⁸ : AddCommMonoid M✝
inst✝⁷ : Module R✝ M✝
R : Type u
M : Type v
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : Nonempty (Fintype { i // p i ≠ ⊥ })
⊢ Fintype { i // p i ≠ ⊥ }

Tactic:
exact this.some

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : B ⊆ ⇑f ⁻¹' this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : f ↑b = hC ⟨f ↑b, ⋯⟩
⊢ C.domRestrict (invFun ⇑f) ⟨f ↑b, ⋯⟩ = ↑b

Tactic:
exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S.toNonUnitalSubalgebra ↔ s ⊆ ↑S

Tactic:
coe_toNonUnitalSubalgebra

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ⊆ ↑S
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n
⊢ f (b i) = (b.coord ⟨w, ⋯⟩) (b i)

Tactic:
rw [Basis.coord_apply, Basis.repr_self]

Goal state after:
case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n
⊢ f (b i) = (Finsupp.single i 1) ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
⊢ S = ⊤

Tactic:
set bS := Basis.ofVectorSpace K S with bS_eq

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
⊢ S = ⊤
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (p.sum g) = p.sum fun n a ↦ eval₂ f x (g n a)

Tactic:
by
  let T : R[X] →+ S :=
    { toFun := eval₂ f x
      map_zero' := eval₂_zero _ _
      map_add' := fun p q => eval₂_add _ _ }
  have A : ∀ y, eval₂ f x y = T y := fun y => rfl
  simp only [A]
  rw [sum, map_sum, sum]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
⊢ Commute (f (X.coeff k)) x

Tactic:
rcases em (k = 1) with (rfl | hk)

Goal state after:
case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ Commute (f (X.coeff 1)) x

case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
k : ℕ
hk : ¬k = 1
⊢ Commute (f (X.coeff k)) x
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
⊢ Prime p

Tactic:
have h1 := Nat.one_lt_two.trans_le h.1

Goal state after:
p : ℕ
h : 2 ≤ p ∧ ∀ (m : ℕ), m ∣ p → m = 1 ∨ m = p
h1 : 1 < p
⊢ Prime p
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬n ∉ p.degree
⊢ p.degree = ↑p.natDegree

Tactic:
have hn : degree p = some n := Classical.not_not.1 hn

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬n ∉ p.degree
hn : p.degree = some n
⊢ p.degree = ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : p = 0
⊢ ⊥ ≤ q.degree

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
a : R
inst✝ : Semiring R
h : a = 0
⊢ degree 0 ≤ 0

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∑ i ∈ s, f i) ≤ s.sup fun i ↦ supDegree D (f i)

Tactic:
simp only [supDegree, coeff_sum]
  grw [Finsupp.support_finsetSum, Finset.sup_biUnion]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
this : DecidableEq R := Classical.decEq R
h : a = 0
⊢ ⊥ ≤ ↑n

Tactic:
exact bot_le

Goal state after: