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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = (↑q.den)⁻¹ * unop ↑q.num

Tactic:
unop_intCast,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = (↑q.den)⁻¹ * ↑q.num
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = unop ↑q.num / ↑q.den

Tactic:
unop_intCast,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q.num / ↑q.den
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f ((↑c.num / ↑c.den) • x) = (↑c.num / ↑c.den) • f x

Tactic:
div_eq_mul_inv,

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num / ↑c.den) • f x
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num / ↑c.den) • f x

Tactic:
div_eq_mul_inv,

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ≥0
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num * (↑c.den)⁻¹) • f x
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ f ((↑c.num / ↑c.den) • x) = (↑c.num / ↑c.den) • f x

Tactic:
div_eq_mul_inv,

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num / ↑c.den) • f x
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num / ↑c.den) • f x

Tactic:
div_eq_mul_inv,

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
F : Type u_3
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_4
S : Type u_5
inst✝³ : DivisionRing R
inst✝² : DivisionRing S
inst✝¹ : Module R M
inst✝ : Module S M₂
c : ℚ
x : M
⊢ f ((↑c.num * (↑c.den)⁻¹) • x) = (↑c.num * (↑c.den)⁻¹) • f x
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ A.updateCol i b x y = (replicateCol (Fin 1) b).submatrix id (Function.const n 0) x y

Tactic:
simp [Subsingleton.elim i y]

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
⊢ baseChange A p ≤ baseChange A q

Tactic:
by
  rw [baseChange, LinearMap.baseChange, ← subtype_comp_inclusion p q h,
    ← LinearMap.id_comp LinearMap.id, AlgebraTensorModule.map_comp]
  apply LinearMap.range_comp_le_range

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

Tactic:
simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')

Tactic:
smulTower_leftMulMatrix,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) ((leftMulMatrix c) ((algebraMap S T) x) (i, k).2 (j, k').2) (i, k).1 (j, k').1 =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a₁ b ↦ (Finsupp.single (snf.f a₁) (b * snf.a a₁)) (snf.f i)) = snf.a i * c i

Tactic:
Finsupp.single_apply,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a₁ b ↦ if snf.f a₁ = snf.f i then b * snf.a a₁ else 0) = snf.a i * c i
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
m : ↥M
r : R
⊢ ↑m • mk' S r m = (algebraMap R S) r

Tactic:
by
  rw [smul_mk', mk'_mul_cancel_left]

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

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

Tactic:
obtain ⟨u, hu⟩ := H c.prop

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : (Algebra.ofId R S) x = (Algebra.ofId R S) y
c : ↥M
eq : ↑c * x = ↑c * y
u : Rˣ
hu : ↑u = ↑c
⊢ x = y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case e'_3
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ M = Submonoid.map (↑h.symm) (Submonoid.map (↑h) M)

Tactic:
RingEquiv.coe_toMulEquiv_symm,

Goal state after:
case e'_3
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ M = Submonoid.map (↑h).symm (Submonoid.map (↑h) M)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ u * (a * ↑d - ↑b * c) = 0

Tactic:
mul_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ u * (a * ↑d) - u * (↑b * c) = 0
Module: Mathlib.Algebra.Ring.TransferInstance

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

Tactic:
apply e.injective.commSemiring _ <;> intros

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

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

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
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
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb) - 1) = a - b

Tactic:
mul_sub,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit ha) * (↑(IsUnit.unit ha)⁻¹ * ↑(IsUnit.unit hb)) - ↑(IsUnit.unit ha) * 1 = a - b
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)
⊢ ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a

Tactic:
mul_sub,

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet R (φ a)

Tactic:
simpa only [map_sub, AlgHomClass.commutes] using! h.map φ

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

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
x : ↥(unitsFstOne R A)
⊢ ↑↑((fun x ↦
            ⟨{ val := 1 + ↑(PreQuasiregular.equiv.symm ↑x), inv := 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹), val_inv := ⋯,
                inv_val := ⋯ },
              ⋯⟩)
          ((fun x ↦
              { val := PreQuasiregular.equiv (↑↑x).toProd.2, inv := PreQuasiregular.equiv (↑↑x⁻¹).toProd.2,
                val_inv := ⋯, inv_val := ⋯ })
            x)) =
    ↑↑x

Tactic:
simpa using x.val.val.inl_fst_add_inr_snd_eq

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
⊢ (algebraMap R C) (x * y).toProd.1 + φ (x * y).toProd.2 =
    ((algebraMap R C) x.toProd.1 + φ x.toProd.2) * ((algebraMap R C) y.toProd.1 + φ y.toProd.2)

Tactic:
by
    induction x with
    | inl_add_inr x_r x_a =>
      induction y with
      | inl_add_inr =>
        simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero,
          map_mul, zero_add, map_add, map_smul φ]
        rw [add_mul, mul_add, mul_add]
        rw [← Algebra.commutes _ (φ x_a)]
        simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]

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

Goal state before:
pp: case mpr.tmul
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
b : ↥(centralizer R S)
c : B
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (b ⊗ₜ[R] c) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (b ⊗ₜ[R] c) * includeLeft x

Tactic:
simp [Subalgebra.mem_centralizer_iff _ |>.1 b.2 x hx]

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

Goal state before:
pp: case mpr.tmul
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
x : A
hx : x ∈ S
b : ↥(centralizer R S)
c : B
⊢ includeLeft x * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (b ⊗ₜ[R] c) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom (b ⊗ₜ[R] c) * includeLeft x

Tactic:
| tmul b c =>

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ f_inv (f x) ≤ f_inv (f y)

Tactic:
exact NonUnitalStarRingHom.map_le_map_of_map_star f_inv h

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

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
x✝ : ↑↑t
a✝ : x✝ ∈ Finset.univ
⊢ extend Subtype.val g 0 ↑x✝ = g x✝

Tactic:
apply Subtype.val_injective.extend_apply

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
⊢ GaloisConnection (adjoin R) SetLike.coe

Tactic:
intro s S

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
⊢ adjoin R s ≤ S ↔ s ⊆ ↑S
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
x : A
⊢ x ∈ ⊥.toNonUnitalSubalgebra ↔ x ∈ ⊥

Tactic:
simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
⊢ ↑(iSup K) ⊆ ⋃ i, ↑(K i)

Tactic:
coe_iSup_of_directed dir

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra 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)
⊢ ⋃ i, ↑(K i) ⊆ ⋃ i, ↑(K i)
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case pos
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
⊢ S = ⊥

Tactic:
refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_
    rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
    obtain ⟨h1⟩ := h1
    obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩
    exact ⟨y, congr(Subtype.val $(hy))⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
⊢ 0 + f = f

Tactic:
by
    ext x y hxy
    · simp [add_domain]
    · simp [add_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f : E →ₛₗ.[σ] F
⊢ f + 0 = f

Tactic:
by
    ext x y hxy
    · simp [add_domain]
    · simp [add_apply]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = f (∑ n ∈ p.support, p.coeff n * r ^ n)

Tactic:
map_sum f

Goal state after:
R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n ∈ p.support, f (p.coeff n) * f r ^ n = ∑ x ∈ p.support, f (p.coeff x * r ^ x)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
⊢ motive a

Tactic:
let of : X → s := Subtype.coind (ι R) grade1

Goal state after:
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) grade1
⊢ motive a
Module: Mathlib.Algebra.Polynomial.Eval.Algebra

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
  | monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p * (X - ↑n)).comp q = p.comp q * (q - ↑n)

Tactic:
mul_sub,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p * X - p * ↑n).comp q = p.comp q * (q - ↑n)
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
by
  rcases lt_trichotomy a 0 with (h | rfl | h)
  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
    lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
  · simp
  · lift a to ℕ using le_of_lt h with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: m n : ℕ
h : n = 1 ∨ m ≤ n.minFac
p : ℕ
pp : 1 < p
d : p ∣ n
⊢ n = 1 → m ≤ p

Tactic:
by rintro rfl; cases not_le_of_gt pp (le_of_dvd (by decide) d)

Goal state after: