mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ x * r • y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_smul_comm] using smul_mem _ _ hxy

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
by
  subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_mk

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ r • a * b = r • (b * a)

Tactic:
smul_mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ r • (a * b) = r • (b * a)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • a * (b * c) = r • a * b * c

Tactic:
smul_mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • a * b * c
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • a * b * c

Tactic:
smul_mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • (a * b) * c
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • (a * b) * c

Tactic:
smul_mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • (a * b * c)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
⊢ r • (x * a) = r • a * x

Tactic:
smul_mul_assoc,

Goal state after:
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
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
⊢ r • (x * a) = r • (a * x)
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
d : ℕ
⊢ M = (↑d).map star ↔ M = ↑d

Tactic:
by rw [map_natCast_star]

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

Goal state before:
pp: R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(b.mkFinSnoc y hli hsp) = Fin.snoc (Subtype.val ∘ ⇑b) y

Tactic:
unfold mkFinSnoc

Goal state after:
R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(have span_b := ⋯;
      Basis.mk ⋯ ⋯) =
    Fin.snoc (Subtype.val ∘ ⇑b) y
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ (fromBlocks A B C D).submatrix f Sum.swap i j = (fromBlocks B A D C).submatrix f id i j

Tactic:
cases j <;> dsimp <;> cases f i <;> rfl

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i ↦ d ⟨k, i⟩) i j

Tactic:
by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
    · rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]
      cases h
      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 : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

Tactic:
ext i k
  simp only [toBlock_apply, mul_apply]
  rw [Finset.sum_subtype]
  simp [Pi.top_apply, Prop.top_eq_true]

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

Goal state before:
pp: case neg.intro.refine_1.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'
z : O
zN : z ∈ N
⊢ ∃ c, z + c • y ∈ N'

Tactic:
obtain ⟨b, hb⟩ : _ ∣ ϕ ⟨z, N_le_M zN⟩ := generator_submoduleImage_dvd_of_mem N_le_M ϕ zN

Goal state after:
case neg.intro.refine_1.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'
z : O
zN : z ∈ N
b : R
hb : ϕ ⟨z, ⋯⟩ = generator (ϕ.submoduleImage N) * b
⊢ ∃ c, z + c • y ∈ N'
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✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
⊢ ∀ (a b : X × ↥S), a ≈ b → add'' a.fst a.snd r₂ s₂ = add'' b.fst b.snd r₂ s₂

Tactic:
by
    -- Porting note: `assoc_rw` & `noncomm_ring` were not ported yet
    rintro ⟨r₁', s₁'⟩ ⟨r₁, s₁⟩ ⟨sb, rb, hb, hb'⟩
    -- s*, r*
    rcases oreCondition (s₁' : R) s₂ with ⟨rc, sc, hc⟩
    --s~~, r~~
    rcases oreCondition rb sc with ⟨rd, sd, hd⟩
    -- s#, r#
    dsimp at *
    rw [add''_char _ _ _ _ rc sc hc (sc * s₁').2]
    have : sd * sb * s₁ = rd * rc * s₂ := by
      rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]
    rw [add''_char _ _ _ _ (rd * rc : R) (sd * sb) this (sd * sb * s₁).2]
    rw [mul_smul, ← Submonoid.smul_def sb, hb, smul_smul, hd, oreDiv_eq_iff]
    use 1
    use rd
    simp only [mul_smul, smul_add, one_smul, OneMemClass.coe_one, one_mul, true_and]
    rw [this, hc, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ (Function.Injective fun x ↦ M *ᵥ x) ↔ LinearIndependent R M.col

Tactic:
simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

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₁
⊢ (toLin v₁ v₁) 1 = LinearMap.id

Tactic:
by
  rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ star (star x) = x

Tactic:
simp_rw [star]
    rw [congr_congr]
    convert! congr($congr_refl_refl x) <;> 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 : R
y : ↥M
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

Tactic:
by
  rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

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₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (↑y₁ * ↑(y₁ * y₂) * x₂) y₂ + (algebraMap R S) (↑(y₁ * y₂) * x₁) =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁

Tactic:
mk'_add_eq_iff_add_mul_eq_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
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) ((algebraMap R S) z) * (map Q g hy) x = (algebraMap P Q) (g z) * (map Q g hy) x

Tactic:
map_eq

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
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (algebraMap P Q) (g z) * (map Q g hy) x = (algebraMap P Q) (g z) * (map Q g hy) x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
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
i : N
m : M
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, i ⊗ₜ[R] m = (rTensor M J.subtype) y

Tactic:
exact ⟨R ∙ i, fg_span_singleton i, ⟨i, mem_span_singleton_self _⟩ ⊗ₜ[R] m, rfl⟩

Goal state after:
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.restrictScalars R (algEquiv N Sₙ Sₙ')) ((algebraMap R Sₙ) x) = (algebraMap R Sₙ') x

Tactic:
AlgEquiv.commutes

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
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
⊢ (algebraMap R Sₙ') x = (algebraMap R Sₙ') x
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
Sₘ : Type u_5
inst✝³ : CommSemiring Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap R Sₘ) ↑y)

Tactic:
IsScalarTower.algebraMap_apply _ S

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
Sₘ : Type u_5
inst✝³ : CommSemiring Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap S Sₘ) ((algebraMap R S) ↑y))
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))) = ⊤
⊢ ⊤ = R ∙ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))).mkQ (f ⟨sSup s, ⋯⟩)

Tactic:
← Set.image_singleton,

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 (⇑(Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))).mkQ '' {f ⟨sSup s, ⋯⟩})
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • b • 1 ⊗ₜ[R] 1
⊢ a • b • 1 ⊗ₜ[R] 1 = b ⊗ₜ[R] a

Tactic:
this b a,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a b : A
this : ∀ (a b : A), a ⊗ₜ[R] b = a • b • 1 ⊗ₜ[R] 1
⊢ a • b • 1 ⊗ₜ[R] 1 = b • a • 1 ⊗ₜ[R] 1
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = 0
⊢ p * q + q * p = 0

Tactic:
by
    rw [hpq, zero_add]
    simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))

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✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul (1 ⊗ₜ[R] 1)) x = x

Tactic:
by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

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✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul x) (1 ⊗ₜ[R] 1) = x

Tactic:
by
  refine TensorProduct.induction_on x ?_ ?_ ?_ <;> simp +contextual

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✝⁸ : 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✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • 1 * x = r • (x * 1)

Tactic:
smul_mul_assoc,

Goal state after:
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✝⁸ : 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✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • (1 * x) = r • (x * 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ˣ
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:
smul_mul_assoc,

Goal state after:
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)
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✝⁸ : 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✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x = r • 1 ⊗ₜ[R] 1 * x

Tactic:
smul_mul_assoc,

Goal state after:
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✝⁸ : 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✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x = r • (1 ⊗ₜ[R] 1 * x)
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 • 1 - ↑a)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ r • ↑a⁻¹ * ↑a - 1 * ↑a = r • 1 - ↑a

Tactic:
smul_mul_assoc,

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)
h₁ : ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a
⊢ r • (↑a⁻¹ * ↑a) - 1 * ↑a = r • 1 - ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

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

Tactic:
refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩

Goal state after:
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

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
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → Ring (κ i)
inst✝ : (i : ι) → Algebra R (κ i)
a : (i : ι) → κ i
⊢ spectrum R a = ⋃ i, spectrum R (a i)

Tactic:
by
  apply compl_injective
  simp_rw [spectrum, Set.compl_iUnion, compl_compl, resolventSet, Set.iInter_ofPred,
    Pi.isUnit_iff, sub_apply, algebraMap_apply]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
x y : Unitization R A
⊢ (star (x * y)).toProd.1 = (star y * star x).toProd.1

Tactic:
by simp [-star_mul']

Goal state after: