mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ r • a ∈ { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M

Tactic:
by
    rw [Algebra.smul_def]; exact Submodule.mul_mem_mul ⟨r, hr, rfl⟩ ha

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
rw [le_def, le_def]

Goal state after:
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : M}, c x y → d x y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔
    c ≤ d

Tactic:
rw [le_def, le_def]

Goal state after:
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : R}, c x y → d x y
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
x✝ : n
⊢ (replicateCol ι a * replicateRow ι b).diag x✝ = (a * b) x✝

Tactic:
simp [Matrix.mul_apply, replicateCol, replicateRow]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
⊢ blockDiagonal 0 = 0

Tactic:
by
  ext
  simp [blockDiagonal_apply]

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✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = (↑sd • ↑sb • r₁ + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑s₁, ⋯⟩

Tactic:
← Submonoid.smul_def sb,

Goal state after:
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
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = (↑sd • sb • r₁ + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑s₁, ⋯⟩
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:
← LinearMap.toMatrix_id v₁,

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

Tactic:
Matrix.toLin_toMatrix

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₁
⊢ LinearMap.id = LinearMap.id
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, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
i : ι
⊢ (∏ j ∈ {i}ᶜ, a j) • a i • s i = ((∏ i ∈ {i}ᶜ, a i) * a i) • s i

Tactic:
mul_smul

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
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
i : ι
⊢ (∏ j ∈ {i}ᶜ, a j) • a i • s i = (∏ i ∈ {i}ᶜ, a i) • a i • s i
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), ⋯⟩
⊢ (snf.bM.repr ↑⟨c.sum fun i x ↦ x • ↑(snf.bN i), hm✝⟩) (snf.f i) =
    (snf.bN.repr (snf.a i • ⟨c.sum fun i x ↦ x • ↑(snf.bN i), hm✝⟩)) i

Tactic:
simp_rw [hm, map_smul, map_finsuppSum, map_smul, Subtype.coe_eta, repr_self,
    Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_single, Finsupp.smul_apply, snf.snf,
    map_smul, repr_self, Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.sum_apply,
    Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Finsupp.sum_ite_eq',
    Finsupp.mem_support_iff, ite_not, mul_comm, ite_eq_right_iff]

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 i = 0 → 0 = snf.a i * c i
Module: Mathlib.Algebra.Algebra.RestrictScalars

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm (((algebraMap R S) r * s) • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
mul_smul

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)
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
⊢ IsLocalization M S ↔
    (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [isLocalization_iff_isLocalizationMap, Submonoid.isLocalizationMap_iff]

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

Goal state before:
pp: case exists_of_eq
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap R S) (h.symm.toRingHom x) = (algebraMap R S) (h.symm.toRingHom y) → ∃ c, ↑c * x = ↑c * y

Tactic:
IsLocalization.eq_iff_exists M S

Goal state after:
case exists_of_eq
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (∃ c, ↑c * h.symm.toRingHom x = ↑c * h.symm.toRingHom y) → ∃ c, ↑c * x = ↑c * 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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ (LinearMap.toSpanSingleton R (M ⧸ N) x).range = ⊤

Tactic:
← LinearMap.span_singleton_eq_range,

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 : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ R ∙ x = ⊤
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
⊢ Nontrivial (M ⊗[R] M)

Tactic:
obtain ⟨I, ϕ, hI, hϕ⟩ := Module.exists_surjective_quotient_of_finite R M

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
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
⊢ Nontrivial (M ⊗[R] M)
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
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

Tactic:
suffices ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m by
    let f : M →ₗ[R] A ⊗[R] M :=
      { toFun m := 1 ⊗ₜ m
        map_add' m n := tmul_add _ _ _
        map_smul' r m := tmul_smul _ _ _ }
    have aux : f ∘ₗ (lift <| LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = .id := by
      ext a m; simpa using! this a m
    exact HasLeftInverse.injective ⟨f, fun x ↦ congr($aux x)⟩

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
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mp
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
w : A ⊗[R] B
hw : ∀ g ∈ ⇑includeLeft '' S, g * w = w * g
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range

Tactic:
let ℬ := Module.Free.chooseBasis R B

Goal state after:
case mp
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
w : A ⊗[R] B
hw : ∀ g ∈ ⇑includeLeft '' S, g * w = w * g
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
⊢ w ∈ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).range
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ (x ≠ y ∧ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p) ↔
    ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p

Tactic:
← exists_and_left

Goal state after:
R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ (∃ x_1, x ≠ y ∧ x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + x_1) ↔
    ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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 : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : K i ≤ K k
hjk : K j ≤ K k
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
simp [hf i k hik, hf j k hjk]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
⊢ 0 ≤ star u * x * u ↔ 0 ≤ x

Tactic:
simpa using hu.star.star_right_conjugate_nonneg_iff

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

Goal state before:
pp: case e'_2
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
p : R
⊢ unop y = unop x + p ↔ y = x + op p

Tactic:
simp [← op_inj (α := R)]

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

Goal state before:
pp: 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
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ ∃ p_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s), f (x + p) = f x + p_1

Tactic:
refine ⟨f p, ?_, map_add f _ _⟩

Goal state after:
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
f : R →⋆ₙ+* S
x p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
⊢ f p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
⊢ star r = r

Tactic:
obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by grind

Goal state after:
case inl
R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
hr : 0 ≤ r
⊢ star r = r

case inr
R✝ : Type u_1
A : Type u_2
inst✝⁷ : NonUnitalRing R✝
inst✝⁶ : PartialOrder R✝
inst✝⁵ : StarRing R✝
inst✝⁴ : StarOrderedRing R✝
p q : R✝
R : Type u_3
inst✝³ : NonUnitalRing R
inst✝² : LinearOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
r : R
hr : 0 ≤ -r
⊢ star r = r
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1) * a) =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n) * a) + Quot.mk (Rel R X) a

Tactic:
mk_mul,

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) * Quot.mk (Rel R X) a =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n) * a) + Quot.mk (Rel R X) a
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) * Quot.mk (Rel R X) a =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n) * a) + Quot.mk (Rel R X) a

Tactic:
mk_mul,

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n + 1)) * Quot.mk (Rel R X) a =
    Quot.mk (Rel R X) (Pre.ofScalar ((algebraMap ℕ R) n)) * Quot.mk (Rel R X) a + Quot.mk (Rel R X) a
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ g.graph

Tactic:
refine h ?_

Goal state after:
case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph
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
⊢ p.degree ≤ q.degree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree

Tactic:
· rw [hp, degree_zero]
    exact bot_le

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.coeff p.natDegree ≠ 0
hp : ¬p = 0
⊢ p.degree ≤ q.degree
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl
    rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n

Tactic:
rintro rfl
    rfl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∑ i ∈ p.support, (monomial i) (p.coeff i) = ∑ i ∈ p.support, C (p.coeff i) * X ^ i

Tactic:
by simp only [C_mul_X_pow_eq_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : max p.degree q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0

Tactic:
HEq,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
HEq : p.degree = q.degree
hlt : max q.degree q.degree > (p + q).degree
⊢ p.leadingCoeff + q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Support

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ∑ i ∈ range n, (monomial i) (p.coeff i) = ∑ i ∈ range n, C (p.coeff i) * X ^ i

Tactic:
by simp only [C_mul_X_pow_eq_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = 1

Tactic:
rw [← coeff_one_zero, ← hgf]

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
x✝ : IsUnit X
g : R[X]
_hfg : (monomial 1) 1 * g = 1
hgf : g * (monomial 1) 1 = 1
⊢ 0 = (g * (monomial 1) 1).coeff 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.IsRoot 0 ↔ p.coeff 0 = 0

Tactic:
rw [coeff_zero_eq_eval_zero, IsRoot]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D (p * p ^ n) = (n + 1) • supDegree D p

Tactic:
(hp.pow hadd hD).supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero,

Goal state after:
case succ
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n✝ : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
n : ℕ
ih : supDegree D (p ^ n) = n • supDegree D p
⊢ supDegree D p + supDegree D (p ^ n) = (n + 1) • supDegree D p
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ ↑(s.coeff.support.inf' hs D) = ↑(s.coeff.support.inf D)

Tactic:
Finset.inf'_eq_inf

Goal state after:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.coeff.support.Nonempty
⊢ ↑(s.coeff.support.inf D) = ↑(s.coeff.support.inf D)
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
    rwa [Finset.mem_range_succ_iff, not_le] at h

Goal state after: