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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (p + q).eraseLead.coeff q.natDegree = (p + q.eraseLead).coeff q.natDegree

Tactic:
eraseLead_coeff,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : n = q.natDegree
⊢ (if q.natDegree = (p + q).natDegree then 0 else (p + q).coeff q.natDegree) = (p + q.eraseLead).coeff q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (p + q).eraseLead.coeff n = (p + q.eraseLead).coeff n

Tactic:
eraseLead_coeff,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else (p + q).coeff n) = (p + q.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.coeff n + q.eraseLead.coeff n

Tactic:
eraseLead_coeff,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ (if n = (p + q).natDegree then 0 else p.coeff n + q.coeff n) = p.coeff n + if n = q.natDegree then 0 else q.coeff n
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

Tactic:
mul_assoc,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (X ^ f.natDegree * (C g.leadingCoeff * X ^ g.natDegree))) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (C g.leadingCoeff * X ^ g.natDegree * X ^ f.natDegree)) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

Tactic:
mul_assoc,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * (C g.leadingCoeff * (X ^ g.natDegree * X ^ f.natDegree))) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * X ^ (revAt N) f.natDegree * (C g.leadingCoeff * X ^ (revAt O) g.natDegree)

Tactic:
mul_assoc,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * (X ^ (revAt N) f.natDegree * (C g.leadingCoeff * X ^ (revAt O) g.natDegree))
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * (C g.leadingCoeff * X ^ (revAt O) g.natDegree * X ^ (revAt N) f.natDegree)

Tactic:
mul_assoc,

Goal state after:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
⊢ C f.leadingCoeff * (C g.leadingCoeff * X ^ ((revAt N) f.natDegree + (revAt O) g.natDegree)) =
    C f.leadingCoeff * (C g.leadingCoeff * (X ^ (revAt O) g.natDegree * X ^ (revAt N) f.natDegree))
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
Finset.sum_eq_zero H,

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ natDegree 0 = s.sup fun i ↦ (f i).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.inr
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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
trans 0

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = 0

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
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ 0 = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
by_cases h₀ : a = 0 <;> simp [h₀, nextCoeff, natDegree_C_mul]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0

Tactic:
intro h
    rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.coeff ((revAt f.natDegree) f.reverse.natDegree) = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
revAt_le f.reverse_natDegree_le

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.coeff (f.natDegree - f.reverse.natDegree) = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
by_cases! FG : k ≤ f.natDegree

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree

case neg
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : f.natDegree < k
⊢ (φ f + φ g).natDegree = fu g.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ n * (X + C r).natDegree = n

Tactic:
natDegree_X_add_C,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ n * 1 = n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum

Tactic:
refine Multiset.induction_on t ?_ fun a t ih ht => ?_

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) 0).sum

case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) (a ::ₘ t)).sum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum

Tactic:
refine Multiset.induction_on t ?_ fun a t ih ht => ?_

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) 0).prod ≠ 0 → (prod 0).natDegree = (Multiset.map (fun f ↦ f.natDegree) 0).sum

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : (Multiset.map (fun f ↦ f.leadingCoeff) (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) (a ::ₘ t)).sum
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * y * y ^ (n - 1 - i)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
i : ℕ
hi : i ∈ range n
this : Commute y ((x + y) ^ i)
⊢ (x + y) ^ i * y ^ (n + 1 - 1 - i) = (x + y) ^ i * (y * y ^ (n - 1 - i))
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
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + ((y * ∑ i ∈ range n, f n i) * x + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n

Tactic:
mul_assoc,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (x + y) ^ n * x + (y * ((∑ i ∈ range n, f n i) * x) + y * y ^ n) = (x + y) ^ n * x + y * (x + y) ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
k : ℕ
hk : k ∈ p.support
this : k ≤ ↑n
⊢ C (p.coeff k) * X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * p * C ↑h.unit⁻¹ = 0
⊢ q = 0

Tactic:
mul_assoc,

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ q = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
k : ℕ
hk : k ∈ p.support
this : k < n
⊢ C (p.coeff k) * X ^ k ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - i) = ∑ x_1 ∈ range n, x ^ x_1 * (y * y ^ (n - 1 - x_1))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'

Tactic:
by rw [Algebra.adjoin_union, hs.2, hs'.2]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ↑(m + (n - m)) ≤ ↑n

Tactic:
add_tsub_cancel_of_le H

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
m n : ℕ
H : m ≤ n
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑m
⊢ ↑n ≤ ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)

Tactic:
exact Ideal.mul_mem_mul (by grind) (by grind)

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

Goal state before:
pp: case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * toSubmodule T * (toSubmodule S * toSubmodule T)
⊢ x * y ∈ toSubmodule S * toSubmodule T

Tactic:
mul_assoc,

Goal state after:
case refine_3
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝² : A
hx✝ : x✝² ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
x✝¹ : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
x✝ : y ∈ Algebra.adjoin R (↑S ∪ ↑T)
hx : x ∈ toSubmodule S * toSubmodule T
hy : y ∈ toSubmodule S * toSubmodule T
this : x * y ∈ toSubmodule S * (toSubmodule T * (toSubmodule S * toSubmodule T))
⊢ x * y ∈ toSubmodule S * toSubmodule T
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p * p' * q)) v = ((aeval f) (p' * (p * q))) v

Tactic:
mul_assoc,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p * (p' * q))) v = ((aeval f) (p' * (p * q))) v
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * q * p)) v = ((aeval f) (p' * (p * q))) v

Tactic:
mul_assoc,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) (p * q)).ker
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p' * (q * p))) v = ((aeval f) (p' * (p * q))) v
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD n * c]

Tactic:
mul_comm n

Goal state after:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
⊢ ker (Quotient.lift I f H) = map (Quotient.mk I) (ker f)

Tactic:
apply Ideal.ext

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
⊢ ∀ (x : R ⧸ I), x ∈ ker (Quotient.lift I f H) ↔ x ∈ map (Quotient.mk I) (ker f)
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : AddMonoidWithOne S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP S p
⊢ CharP (R × S) p

Tactic:
convert! Nat.lcm.charP R S p p; simp

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

Goal state before:
pp: case inl_add_inr
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
r : R
a : ↥s
hx : f (Unitization.inl r + ↑a) = 0
⊢ Unitization.inl r + ↑a = 0

Tactic:
| inl_add_inr r a =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x y : R
⊢ x - y = x + y

Tactic:
by rw [sub_eq_add_neg, neg_eq]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise (IsCoprime on I)
y : R ⧸ ⨅ i, I i
⊢ ∃ r, ∀ (i : ι), (Quotient.mk (I i)) r = (quotientInfToPiQuotient I) y i

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hf : Pairwise (IsCoprime on I)
r : R
⊢ ∃ r_1, ∀ (i : ι), (Quotient.mk (I i)) r_1 = (quotientInfToPiQuotient I) ((Quotient.mk (⨅ i, I i)) r) i
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
h : p * a * y = p * p
ha : x = p * a
⊢ p = a * y

Tactic:
mul_assoc,

Goal state after:
x✝ y✝ p : ℕ
hp : Prime p
hx✝ : x✝ ≠ 1
hy✝ : y✝ ≠ 1
h✝ : x✝ * y✝ = p ^ 2
pdvdxy : p ∣ x✝ * y✝
x y : ℕ
hx : x ≠ 1
hy : y ≠ 1
a : ℕ
h : p * (a * y) = p * p
ha : x = p * a
⊢ p = a * y
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
F : Type w
inst✝⁹ : Ring R
inst✝⁸ : Semiring S
R₁ : Type u_1
R₂ : Type u_2
A : Type u_3
B : Type u_4
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Algebra R₂ A
inst✝² : Semiring B
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : I.IsTwoSided
f : A →ₐ[R₁] B
hI : ∀ a ∈ I, f a = 0
r : R₁
⊢ (↑↑(lift I (↑f) hI)).toFun ((algebraMap R₁ (A ⧸ I)) r) = (algebraMap R₁ B) r

Tactic:
by
      have : algebraMap R₁ (A ⧸ I) r = Ideal.Quotient.mk I (algebraMap R₁ A r) := rfl
      rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk,
        AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one,
        map_smul, map_one]

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd

Tactic:
map_permutationsAux2' id,

Goal state after:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) (map id ts) (map f []) (map id ys) ?f').snd = (permutationsAux2 t ts [] ys f).snd

case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β

case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = ?f' (map id a)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
rw [map] at IH2

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n) * (minimalPeriod f x).gcd n

Tactic:
mul_assoc,

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x ∣ minimalPeriod f^[n] x * (n / (minimalPeriod f x).gcd n * (minimalPeriod f x).gcd n)