mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ (n • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] ↑n

Tactic:
smul_tmul,

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ 1 ⊗ₜ[R] (n • 1) = 1 ⊗ₜ[R] ↑n
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra R B
z : ℤ
⊢ (z • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] ↑z

Tactic:
smul_tmul,

Goal state after:
R : Type uR
A : Type uA
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_3
inst✝¹ : Ring B
inst✝ : Algebra R B
z : ℤ
⊢ 1 ⊗ₜ[R] (z • 1) = 1 ⊗ₜ[R] ↑z
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y : A ⊗[R] B), (0 * x) • m = 0 • x • m → (0 * y) • m = 0 • y • m → (0 * (x + y)) • m = 0 • (x + y) • m

Tactic:
intro z w _ _
      simp only [(· • ·), zero_mul, map_zero, LinearMap.zero_apply]

Goal state after:
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
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]

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
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case e'_4
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 b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
    all_goals exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

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✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ (y • x) ⊗ₜ[R] 1 = x ⊗ₜ[R] y

Tactic:
smul_tmul,

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✝⁵ : Semiring B
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
inst✝ : CompatibleSMul R S S S
x✝ : S ⊗[R] S
x y : S
⊢ x ⊗ₜ[R] (y • 1) = x ⊗ₜ[R] y
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card ≤ Fintype.card ι

Tactic:
convert! Fintype.card_range_le v

Goal state after:
case e'_3
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card = Fintype.card ↑(range v)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
h : IsAtom W
⊢ ∃ v, v ≠ 0 ∧ W = K ∙ v

Tactic:
obtain ⟨hbot, h⟩ := h

Goal state after:
case refine_1
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ b < W, b = ⊥
⊢ ∃ v, v ≠ 0 ∧ W = K ∙ v
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: case inl
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
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : x ∈ s
⊢ p x ⋯

Tactic:
exact mem x hx

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
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'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)
  obtain ⟨w, hw⟩ := exists_ne (0 : V')
  have : v ∉ (⊥ : Submodule K V) := by simp only [mem_bot, hv, not_false_eq_true]
  obtain ⟨g, _, hg⟩ := LinearMap.exists_extend_of_notMem (K := K) 0 this w
  exact ⟨g, 0, DFunLike.ne_iff.mpr ⟨v, by simp_all⟩⟩

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

Goal state before:
pp: case refine_2
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 + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ e ∈ t, f e = 0

pp: case refine_3
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 + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
· simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1

Goal state after:
case refine_3
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 + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x ∈ t, f x ≠ 0
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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W + Module.rank K ↥Q = Module.rank K ↥Q' + Module.rank K ↥W

pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
← rank_prod',

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K (↥W × ↥Q) = Module.rank K ↥Q' + Module.rank K ↥W

K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥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
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K V = Module.rank K ↥W' + Module.rank K ↥Q'

pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀

Tactic:
← rank_prod',

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K V = Module.rank K (↥W' × ↥Q')

K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ Module.rank K ↥W < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K✝ : Type u
V : Type v
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
hx : x ≠ 0
⊢ x * Classical.choose ⋯ = 1

Tactic:
exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : (X ^ k).comp p = p ^ k
⊢ (X ^ (k + 1)).comp p = p ^ (k + 1)

Tactic:
simp [pow_succ, mul_X_comp, ih]

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ (single a r).coeff.support * x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support

Tactic:
coeff_single,

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ (Finsupp.single a r).support * x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ {a} * x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support

Tactic:
change image₂ _ _ _ ⊆ _

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) {a} x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ x.coeff.support * (single a r).coeff.support ⊆ image (fun x ↦ x * a) x.coeff.support

Tactic:
coeff_single,

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ x.coeff.support * (Finsupp.single a r).support ⊆ image (fun x ↦ x * a) x.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ x.coeff.support * {a} ⊆ image (fun x ↦ x * a) x.coeff.support

Tactic:
change image₂ _ _ _ ⊆ _

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ image₂ (fun x1 x2 ↦ x1 * x2) x.coeff.support {a} ⊆ image (fun x ↦ x * a) x.coeff.support
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
⊢ eval₂ f x p = eval x (map f p)

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simp [hp, hq]
  | monomial n r => simp

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
⊢ g.toLinearPMap.graph = g

Tactic:
ext ⟨x_fst, x_snd⟩
  constructor <;> intro hx
  · rw [LinearPMap.mem_graph_iff] at hx
    rcases hx with ⟨y, hx1, hx2⟩
    convert! g.mem_graph_toLinearPMap hg y using 1
    exact Prod.ext hx1.symm hx2.symm
  rw [LinearPMap.mem_graph_iff]
  have hx_fst : x_fst ∈ g.map (LinearMap.fst R E F) := by
    simp only [mem_map, LinearMap.fst_apply, Prod.exists, exists_and_right, exists_eq_right]
    exact ⟨x_snd, hx⟩
  refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩
  rw [toLinearPMap_apply_aux hg]
  exact (existsUnique_from_graph @hg hx_fst).unique (valFromGraph_mem hg hx_fst) hx

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Monoid M
F : R[M] →ₐ[R] A
f : R[M]
⊢ F f = f.coeff.sum fun a b ↦ b • F (single a 1)

Tactic:
conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]

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

Goal state before:
pp: R : Type u_1
A : Type u_4
M : Type u_7
inst✝³ : CommSemiring R
inst✝² : AddMonoid M
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : R[M] →ₐ[R] A
f : R[M]
⊢ F f = f.coeff.sum fun m r ↦ r • F (single m 1)

Tactic:
conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
⊢ C r ∣ φ → ∀ (i : ℕ), r ∣ φ.coeff i

Tactic:
rintro ⟨φ, rfl⟩ c

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ
⊢ r ∣ (C r * φ).coeff c
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree

Tactic:
rcases le_max_iff.1 (degree_add_le p q) with h | h <;> simp [natDegree_le_natDegree h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).degree ≤ p.degree

Tactic:
apply sup_mono

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support ⊆ p.support
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : WithBot ℕ
⊢ f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Tactic:
by
  simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne, ← not_le,
    not_imp_comm, Nat.cast_withBot]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x

Tactic:
refine ⟨zero_lt_one.trans_le, fun h => ?_⟩

Goal state after:
x : WithBot ℕ
h : 0 < x
⊢ 1 ≤ x
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0

Tactic:
by simpa using one_le_iff_zero_lt

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✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ supDegree D p ≤ supDegree D (p + q)

Tactic:
rw [he] at h ⊢

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ D a ≤ supDegree D (p + q)
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✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
by_cases! h : ∀ k ∈ s, k = i

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
⊢ ∑ i ∈ s, f i ≠ 0

case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∃ k ∈ s, k ≠ i
⊢ ∑ i ∈ s, f i ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * (X ^ x).coeff n) = p.coeff n * r ^ n

Tactic:
coeff_X_pow

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Zero α
inst✝ : Preorder α
i : ι
a : α
⊢ 0 ≤ single i a ↔ 0 ≤ a

Tactic:
classical exact Pi.single_nonneg

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
x✝ : R[X]
⊢ ((aeval p).comp (aeval q)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
x✝ : R[X]
⊢ ((aeval q).comp (aeval p)) x✝ = (AlgHom.id R R[X]) x✝

Tactic:
by simp [← comp_eq_aeval, comp_assoc, hpq, hqp]

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g₁ g₂ : Π₀ (a : α), N a
⊢ (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂

Tactic:
by
  simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
⊢ ∀ (s : σ →₀ ℕ) (a : R), motive ((monomial s) a)

Tactic:
intro s a
  apply @Finsupp.induction σ ℕ _ _ s
  · change motive (monomial 0 a)
    exact C a
  · intro n e p _hpn _he ih
    have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
    simp [add_comm, monomial_add_single, this]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ coeff d (∏ y ∈ s, X y ^ x y) = if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0

Tactic:
prod_X_pow x s,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ coeff d ((monomial (Finsupp.indicator s fun i x_1 ↦ x i)) 1) =
    if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support ∆ q.support ⊆ (p + q).support

Tactic:
by
  rw [symmDiff_def, Finset.sup_eq_union]
  apply Finset.union_subset
  · exact support_sdiff_support_subset_support_add p q
  · rw [add_comm]
    exact support_sdiff_support_subset_support_add q p

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

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
rintro ⟨φ, rfl⟩ c

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
c : σ →₀ ℕ
⊢ r ∣ coeff c (C r * φ)
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ⇑toLex

Tactic:
by
  intro a b h
  refine le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)
  classical
  exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
    fun j hj ↦ notMem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_gt hj,
    (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g p) * k (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) (p * X s))

Tactic:
(map f).map_mul,

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g p) * k (eval₂ f g (X s)) = eval₂ k (⇑k ∘ g) ((map f) p * (map f) (X s))