mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 → ∃ v₀, s ≤ K ∙ v₀

Tactic:
rank_submodule_le_one_iff

Goal state after:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
this : Nontrivial K
⊢ (∃ v₀ ∈ s, s ≤ K ∙ v₀) → ∃ v₀, s ≤ K ∙ v₀
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (i : ℕ), f 0 * x ^ i = 0

Tactic:
simp [add_mul]

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

Goal state before:
pp: case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (a : ℕ) (b₁ b₂ : R), f (b₁ + b₂) * x ^ a = f b₁ * x ^ a + f b₂ * x ^ a

Tactic:
simp [add_mul]

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 g : E →ₛₗ.[σ] F
⊢ f - g = f + -g

Tactic:
by
    ext x _ h
    · rfl
    simp [sub_apply, add_apply, neg_apply, ← sub_eq_add_neg]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p r : R[X]
⊢ (C a * p).comp r = C a * p.comp r

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

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

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

Tactic:
mul_X_comp,

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
i : ℤ
⊢ (↑i).comp p = ↑i

Tactic:
cases i

Goal state after:
case ofNat
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).comp p = ↑(Int.ofNat a✝)

case negSucc
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).comp p = ↑(Int.negSucc a✝)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

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

Tactic:
mul_X_comp,

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

Goal state before:
pp: p : ℕ
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → m ∣ p → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ), m < p → n < p → m * n ≠ p

Tactic:
dvd_def,

Goal state after:
p : ℕ
⊢ (2 ≤ p ∧ ∀ (m : ℕ), m < p → (∃ c, p = m * c) → m = 1) ↔ 2 ≤ p ∧ ∀ (m n : ℕ), m < p → n < p → m * n ≠ p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
this : DecidableEq R := Classical.decEq R
H : ∀ (p : ℕ), ↑p = 0 → p = 0
x : ℕ
⊢ ↑x = 0 ↔ 0 ∣ x

Tactic:
rw [zero_dvd_iff]; exact ⟨H x, by rintro rfl; simp⟩

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ringChar R = 1 ↔ Subsingleton R

Tactic:
by
  rw [← Nat.dvd_one, ← spec, eq_comm, Nat.cast_one, subsingleton_iff_zero_eq_one]

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

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D 1 ≤ 0

Tactic:
one_def,

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (single 0 1) ≤ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
a : ℕ
⊢ ((X - C r) * p).coeff (a + 1) = p.coeff a - r * p.coeff (a + 1)

Tactic:
by simp [sub_mul]

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

Goal state before:
pp: i : ℤ
R : Type u_1
inst✝ : Ring R
⊢ (↑i).coeff 0 = ↑i

Tactic:
cases i

Goal state after:
case ofNat
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.ofNat a✝)).coeff 0 = ↑(Int.ofNat a✝)

case negSucc
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ (↑(Int.negSucc a✝)).coeff 0 = ↑(Int.negSucc a✝)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
· apply natDegree_eq_of_natDegree_add_lt_left; rwa [H, Nat.pos_iff_ne_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).degree = ↑n

Tactic:
rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]

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
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D 1 = 1

Tactic:
one_def,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
⊢ leadingCoeff D (single 0 1) = 1
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: S : Type v
inst✝ : Semiring S
r : S
⊢ (X + C r).leadingCoeff = 1

Tactic:
← pow_one (X : S[X]),

Goal state after:
S : Type v
inst✝ : Semiring S
r : S
⊢ (X ^ 1 + C r).leadingCoeff = 1
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case zero
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
⊢ supDegree D 1 = 0

Tactic:
one_def,

Goal state after:
case zero
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
⊢ supDegree D (single 0 1) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

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

Tactic:
rw [eval_eq_sum, p.sum_over_range' _ _ hn]; simp

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))

Tactic:
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) =
    ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
⊢ (map f p).natDegree < p.natDegree

Tactic:
by_cases H : map f p = 0

Goal state after:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ (map f p).natDegree < p.natDegree

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree
Module: Mathlib.Order.PiLex

Goal state before:
pp: case inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₁ < N₂
⊢ a < c

pp: case inr.inl
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → b j = c j
b_lt_c : b N₁ < c N₁
⊢ a < c

pp: case inr.inr
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝¹ : LinearOrder ι
inst✝ : (a : ι) → PartialOrder (β a)
a b c : Lex ((i : ι) → β i)
N₁ : ι
lt_N₁ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₁ → a j = b j
a_lt_b : a N₁ < b N₁
N₂ : ι
lt_N₂ : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j N₂ → b j = c j
b_lt_c : b N₂ < c N₂
H : N₂ < N₁
⊢ a < c

Tactic:
exacts [⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ <| hj.trans H), lt_N₂ _ H ▸ a_lt_b⟩,
      ⟨N₁, fun j hj => (lt_N₁ _ hj).trans (lt_N₂ _ hj), a_lt_b.trans b_lt_c⟩,
      ⟨N₂, fun j hj => (lt_N₁ _ (hj.trans H)).trans (lt_N₂ _ hj), (lt_N₁ _ H).symm ▸ b_lt_c⟩]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
r : R
⊢ (C r).coeffs = if r = 0 then ∅ else {r}

Tactic:
aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (p * X n).coeffs = p.coeffs

Tactic:
aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : σ
⊢ (X n * p).coeffs = p.coeffs

Tactic:
aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d ((rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a ∈ φ.degrees, f a = i

Tactic:
rintro ⟨d, hd, hi⟩

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d ((rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a ∈ φ.degrees, f a = i
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ ((rename f) ((killCompl hf) p)).support ⊆ p.support

Tactic:
by
  classical
  rw [MvPolynomial.support_rename_of_injective hf, support_killCompl, Finset.image_preimage]
  exact Finset.filter_subset ..

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

Goal state before:
pp: case mul_X
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
i : σ ⊕ τ
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X i) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X i))

Tactic:
cases i

Goal state after:
case mul_X.inl
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inl val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inl val✝)))

case mul_X.inr
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inr val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inr val✝)))
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
b : R
hnext : b = 0
⊢ (C a * X + C b).eraseLead = 0

Tactic:
subst b

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X + C 0).eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
p : R[X]
a : R
⊢ eval₂ Polynomial.C (fun x ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (Polynomial.C a)) = Polynomial.C a

Tactic:
by rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
this : #((X - C x) * P).support ≤ 2
⊢ ((X - C x) * P).eraseLead.eraseLead = 0

Tactic:
← card_support_eq_zero

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : P.eraseLead = 0
he₂ : ¬((X - C x) * P).eraseLead = 0
this : #((X - C x) * P).support ≤ 2
⊢ #((X - C x) * P).eraseLead.eraseLead.support = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
i : Option S₁
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X i)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X i))

Tactic:
cases i

Goal state after:
case none
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X none)) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X none))

case some
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
m✝ : Option S₁ →₀ ℕ
val✝ : S₁
⊢ coeff m✝
      (((Polynomial.aevalTower (rename Option.some) (X none)).comp
          (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)))
        (X (Option.some val✝))) =
    coeff m✝ ((AlgHom.id R (MvPolynomial (Option S₁) R)) (X (Option.some val✝)))
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
by
  have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
  rw [degree_mul_C h₁]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ x_1 ∈ range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)

Tactic:
rw [← Finset.sum_flip]

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ r ∈ range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
intro p hp
    replace hp := mem_degreeLT.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine Submodule.smul_mem _ _ (Submodule.subset_span <| by grind)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
⊢ Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)

Tactic:
intro r hr

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R (s ∪ t))
⊢ r ∈ span R (p * q)
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
⊢ (Finsupp.linearCombination (↥(adjoin R s)) _root_.id) l ∈ span R (p * q)

Tactic:
rw [this, Finsupp.sum]

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
⊢ ∑ a ∈ l.support, l a • _root_.id a ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
⊢ I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Tactic:
intro r hr

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
r : R
hr : r ∈ I.leadingCoeffNth m
⊢ r ∈ I.leadingCoeffNth n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}

Tactic:
by
  let p := Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }
  nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]
  refine Submodule.sum_mem _ fun n _hn => ?_
  dsimp
  have : C (coeff f n) ∈ p := by
    apply subset_span
    rw [mem_ofPred_eq]
    use n
  have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
  convert! this using 1
  simp only [monomial_mul_C, one_mul, smul_eq_mul]
  rw [← C_mul_X_pow_eq_monomial]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R {x | x ∈ s}) = Set.univ

Tactic:
Finset.setOfPred_mem,

Goal state after:
case mp
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Finset A
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R ↑s) = Set.univ
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R {x | x ∈ s}) = Set.univ

Tactic:
Finset.setOfPred_mem,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑(adjoin R ↑s) = Set.univ
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ≤ J
⊢ map (Quotient.mk J) I = ⊥

Tactic:
rw [map_eq_bot_iff_le_ker, mk_ker]
  exact h

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : SetLike S A
hSA : NonUnitalSubringClass S A
hSRA : SMulMemClass S R A
s : S
h : ∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s
inst✝¹ : FunLike F (Unitization R ↥s) A
inst✝ : AlgHomClass F R (Unitization R ↥s) A
f : F
hf : ∀ (x : ↥s), f ↑x = ↑x
⊢ Function.Injective ⇑f

Tactic:
by
  refine (injective_iff_map_eq_zero f).mpr fun x hx => ?_
  induction x with
  | inl_add_inr r a =>
    simp_rw [map_add, hf, ← Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx
    rw [add_eq_zero_iff_eq_neg] at hx ⊢
    by_cases hr : r = 0
    · ext
      · simp [hr]
      · simpa [hr] using hx
    · exact (h r hr <| hx ▸ (neg_mem a.property)).elim

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = A ∙ Submodule.Quotient.mk 1

Tactic:
Quotient.mk_eq_mk

Goal state after:
A : Type u_3
inst✝¹ : Ring A
I : Ideal A
inst✝ : I.IsTwoSided
⊢ A ∙ (mk I) 1 = A ∙ (mk I) 1
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p : ℕ
p_prime : Prime p
m n k l : ℕ
hpm : p ^ k ∣ m
hpn : p ^ l ∣ n
hpmn : p ^ (k + l + 1) ∣ m * n
hpd : p ^ (k + l) * p ∣ m * n
hpd2 : p ∣ m * n / p ^ (k + l)
hpd3 : p ∣ m * n / (p ^ k * p ^ l)
hpd4 : p ∣ m / p ^ k * (n / p ^ l)
hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l
⊢ p ^ k * p ∣ m ∨ p ^ l * p ∣ n

Tactic:
exact hpd5.elim (fun h : p ∣ m / p ^ k => Or.inl <| mul_dvd_of_dvd_div hpm h)
    fun h : p ∣ n / p ^ l => Or.inr <| mul_dvd_of_dvd_div hpn h

Goal state after: