mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ (p * q).coeff (ap + aq) = p.coeff ap * q.coeff aq

Tactic:
simp_rw [coeff_mul, Finsupp.sum]
  rw [Finset.sum_eq_single ap, Finset.sum_eq_single aq, if_pos rfl]
  · refine fun a ha hne => if_neg (fun he => ?_)
    apply_fun D at he; simp_rw [hadd] at he
    exact (add_lt_add_right (((Finset.le_sup ha).trans hq).lt_of_ne <| hD.ne_iff.2 hne) _).ne he
  · intro h; rw [if_pos rfl, Finsupp.notMem_support_iff.1 h, mul_zero]
  · refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)
    apply_fun D at he
    simp_rw [hadd] at he
    have := addLeftMono_of_addLeftStrictMono B
    exact (add_lt_add_of_lt_of_le (((Finset.le_sup ha).trans hp).lt_of_ne <| hD.ne_iff.2 hne)
      <| (Finset.le_sup ha').trans hq).ne he
  · refine fun h => Finset.sum_eq_zero (fun a _ => ite_eq_right_iff.mpr <| fun _ => ?_)
    rw [Finsupp.notMem_support_iff.mp h, zero_mul]

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
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
by
  obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_ge)
  rw [leadingCoeff, supDegree_add_eq_left h, coeff_add, Finsupp.add_apply, ← leadingCoeff,
    coeff_eq_zero_of_not_le_supDegree (D := D), add_zero]
  rw [← he, Function.apply_invFun_apply (f := D), he]; exact h.not_ge

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

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

Tactic:
simp [(monic_X_pow n).degree_mul]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ eval₂ f 0 p = f (p.coeff 0)

Tactic:
by
  simp +contextual only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero,
    mul_one, sum, Classical.not_not, mem_support_iff, sum_ite_eq', ite_eq_left_iff, map_zero,
    imp_true_iff]

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

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

Tactic:
simp [← coeff_zero_eq_eval_zero]

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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : Monic D q
⊢ Monic D (p * q)

Tactic:
by
  rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]; exact hp

Goal state after:
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 : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p.degree = ⊥

Tactic:
← hpq,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ (map f p).degree = ⊥
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp.inl
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x a + y a = if a = a then n else 0
⊢ (if a = a then x a else 0) = x a ∧ (if a = a then y a else 0) = y a

Tactic:
exact ⟨if_pos rfl, if_pos rfl⟩

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
⊢ ↑(y + w).support ⊆ Set.range ⇑f

Tactic:
· simp [← hw]

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
f : F
x : A
p✝ p q : R[X]
hp : (aeval (f x)) p = f ((aeval x) p)
hq : (aeval (f x)) q = f ((aeval x) q)
⊢ (aeval (f x)) (p + q) = f ((aeval x) (p + q))

Tactic:
rw [map_add, hp, hq, ← map_add, ← map_add]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : 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)), a < b → b < c → a < c

Tactic:
rintro a b c ⟨N₁, lt_N₁, a_lt_b⟩ ⟨N₂, lt_N₂, b_lt_c⟩

Goal state after:
ι : 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₂
⊢ a < c
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
ext s
  simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Nat.succ_le_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 0 < m s then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 1 ≤ m s then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0

Tactic:
Nat.succ_le_iff,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if 0 < m s then 1 * coeff (m - Finsupp.single s 1) p else 0) =
    if m s ≠ 0 then coeff (m - Finsupp.single s 1) p else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∑ v ∈ p.support, (monomial v) (coeff v p)).coeff = p.coeff

Tactic:
AddMonoidAlgebra.coeff_sum

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ ∑ i ∈ p.support, ((monomial i) (coeff i p)).coeff = p.coeff
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1

Tactic:
let e := Fintype.equivFin { x // x ∈ s }

Goal state after:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ ∃ n f, ∃ (_ : Injective f), ∃ q_1, (rename Subtype.val) q = (rename f) q_1
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ p.vars = p.degrees.toFinset

Tactic:
by
  rw [vars]
  convert! rfl

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

Goal state before:
pp: case monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
inst✝ : DecidableEq S₁
a : σ →₀ ℕ
s : R
p : MvPolynomial σ R
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs
ih : ((map f) ((monomial a) s)).coeffs ⊆ Finset.image (⇑f) ((monomial a) s).coeffs
⊢ Disjoint ((map f) ((monomial a) s)).support ((map f) p).support

Tactic:
exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs

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

Tactic:
rw [nextCoeff, h₁, add_tsub_cancel_right, hdP, coeff_X_sub_C_mul]

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h : P.coeff (dP + 1) = 0
⊢ (if dP + 2 + 1 = 0 then 0 else P.coeff (dP + 1) - x * P.coeff (dP + 1 + 1)) ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)

Tactic:
rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    Polynomial.C (C r * m.some.prod fun n e ↦ X n ^ e) * Polynomial.X ^ m none
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = 1

Tactic:
Monic.def.1 hp,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this✝ : DecidableEq R := Classical.decEq R
h0 : ¬0 = 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ 1 * q.leadingCoeff = 1
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
⊢ (φ f).natDegree = fu f.natDegree → (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
fk

Goal state after:
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
⊢ (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ degree 1 = 0

pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Tactic:
degree_one

Goal state after:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 0 = 0

R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
(monic_X_add_C r).natDegree_pow,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ n * (X + C r).natDegree = 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.Monic

Tactic:
refine t.induction_on ?_ ?_

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.Monic

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) = -t.sum

Tactic:
convert! multiset_prod_X_sub_C_nextCoeff (by assumption)

Goal state after:
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) = (Multiset.map (fun x ↦ X - C x) t).prod.nextCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0

Tactic:
← smul_zero k

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = k • 0
⊢ p = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) = f

Tactic:
ext i; grind [finsetSum_coeff, Finset.sum_eq_single i, coeff_monomial]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : p ∈ degreeLT R p.natDegree
⊢ False

Tactic:
rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (X * p).degree
⊢ False

Tactic:
congr_arg degree hp,

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < degree 1
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
⊢ ∑ x ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P

Tactic:
apply P.sum_mem

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := ⋯
n : ℕ := ⋯
⊢ ∀ c ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
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
v : M
⊢ (LinearIndependent R fun n ↦ (f ^ n) v) ↔ ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0

Tactic:
by
  simp [linearIndependent_iff, Finsupp.linearCombination_apply, aeval_endomorphism, Finsupp.sum,
    forall_iff_forall_finsupp, AddMonoidAlgebra.coeffEquiv.forall_congr_left, Polynomial.sum]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ IsIdempotentElem (toSubmodule S)

Tactic:
by
  apply le_antisymm
  · refine (mul_toSubmodule_le _ _).trans_eq ?_
    rw [sup_idem]
  · intro x hx1
    rw [← mul_one x]
    exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := this✝¹.toSMul
this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
rank_mul_rank R A (Algebra.adjoin A (B : Set S))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
h✝ : Nontrivial R
a✝ : Nontrivial S
this✝¹ : Algebra ↥A ↥(Algebra.adjoin ↥A ↑B) := (Algebra.adjoin ↥A ↑B).algebra
this✝ : SMul ↥A ↥(Algebra.adjoin ↥A ↑B) := this✝¹.toSMul
this : IsScalarTower R ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥(Algebra.adjoin ↥A ↑B)
Module: Mathlib.Data.Int.ModEq

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

Tactic:
by
  rw [add_comm, modEq_add_modulus_mul_iff]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)

Tactic:
exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
refine ⟨fun h hf => ?_, hp.eq_two_or_odd.resolve_left⟩
  rw [hf] at h
  simp at h

Goal state after:
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
R : Type ?u.26
inst✝² : CommRing R
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
inst✝ : P.IsTwoSided
h : p ≤ comap (algebraMap R A) P
r₁ : R
a₁ : A
r₂ : R
a₂ : A
hr : r₁ ≈ r₂
ha : a₁ ≈ a₂
⊢ r₁ • a₁ ≈ r₂ • a₂

Tactic:
have := h (p.quotientRel_def.mp hr)
    rw [mem_comap, map_sub] at this
    simpa only [Algebra.smul_def] using P.quotientRel_def.mpr
      (P.mul_sub_mul_mem this <| P.quotientRel_def.mp ha)

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
z : A
⊢ z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
simp [← SetLike.mem_coe, centralizer_union, ← image_star, mem_centralizer_iff, forall_and]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
rw [nextOr_cons_of_ne _ _ _ _ hx] at h
      simpa [hx] using IH h

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
i : ℤ
g : G
a : α
⊢ g ^ (i + ↑(period g a)) • a = g ^ i • a

Tactic:
by
  rw [← zpow_mod_period_smul, Int.add_emod_right, zpow_mod_period_smul]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Card

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set α
⊢ Nat.card ↑(t * ↑s) = Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' t)

Tactic:
by
  rw [← Nat.card_prod, Nat.card_congr]
  apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)
  rw [QuotientGroup.preimage_image_mk]
  convert! Equiv.refl ↑(t * s)
  aesop (add simp [Set.mem_mul])

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

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)

Tactic:
· exact IH hx.right

Goal state after:
case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
h : l ~r l'
hn : l.Nodup
x : α
hx : x ∈ l
⊢ l.next x hx = l'.next x ⋯

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  obtain ⟨n, rfl⟩ := id h
  rw [next_getElem _ hn]
  simp_rw [getElem_eq_getElem_rotate _ n k]
  rw [next_getElem _ (h.nodup_iff.mp hn), getElem_eq_getElem_rotate _ n]
  simp [add_assoc]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
⊢ Chain r ↑(a :: l) → ∀ a_2 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_2 b

Tactic:
intro hs b hb c hc

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
hs : Chain r ↑(a :: l)
b : α
hb : b ∈ ↑(a :: l)
c : α
hc : c ∈ ↑(a :: l)
⊢ r b c
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
intro g hg

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (comap ((MulDistribMulAction.toMonoidEnd H G) h) (h • J)).relIndex K = J.relIndex K

Tactic:
pointwise_smul_def,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : Group G
inst✝ : MulDistribMulAction H G
J K : Subgroup G
⊢ (comap ((MulDistribMulAction.toMonoidEnd H G) h) (map ((MulDistribMulAction.toMonoidEnd H G) h) J)).relIndex K =
    J.relIndex K
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (comap ((DistribMulAction.toAddMonoidEnd H G) h) (h • J)).relIndex K = J.relIndex K

Tactic:
pointwise_smul_def,

Goal state after:
G : Type u_1
H : Type u_2
inst✝² : Group H
h : H
inst✝¹ : AddGroup G
inst✝ : DistribMulAction H G
J K : AddSubgroup G
⊢ (comap ((DistribMulAction.toAddMonoidEnd H G) h) (map ((DistribMulAction.toAddMonoidEnd H G) h) J)).relIndex K =
    J.relIndex K