mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case single_add
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
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : motive ((monomial p) a)
this : ∀ (e : ℕ), motive ((monomial p) a * X n ^ e)
⊢ motive ((monomial (Finsupp.single n e + p)) a)

Tactic:
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
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ Disjoint ((monomial a) s).support p.support

Tactic:
by
  classical
  simpa [support_monomial, hs] using notMem_support_iff.mp ha

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
g : τ → σ
hf : LeftInverse f g
⊢ LeftInverse ⇑(rename f) ⇑(rename g)

Tactic:
by
  intro x
  simp [hf.comp_eq_id]

Goal state after:
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
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ (rename Subtype.val) q = (rename (Subtype.val ∘ ⇑e.symm)) ((rename ⇑e) q)

Tactic:
← rename_rename,

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
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename ⇑e.symm) ((rename ⇑e) q))
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Tactic:
by
  simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]
  exact Multiset.subset_of_le degrees_mul_le

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

Goal state before:
pp: case refine_2.mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ S₁
n : σ
ih : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
hx : ↑p.coeffs ⊆ range ⇑f
⊢ p * X n ∈ range ⇑(map f)

Tactic:
obtain ⟨q, rfl⟩ := ih hx

Goal state after:
case refine_2.mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
n : σ
q : MvPolynomial σ R
ih : ↑((map f) q).coeffs ⊆ range ⇑f → (map f) q ∈ range ⇑(map f)
hx : ↑((map f) q).coeffs ⊆ range ⇑f
⊢ (map f) q * X n ∈ range ⇑(map f)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ eval₂ c (⇑f ∘ X) (p + q) = f (p + q)

Tactic:
rw [eval₂_add, hp, hq]
      exact (f.map_add _ _).symm

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

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom).comp C =
    (RingHom.id (MvPolynomial σ R)).comp C

pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

pp: case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
· ext1
        simp [algebraMap_eq]

Goal state after:
case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
i : τ
hip a✝ : f i ∈ p.vars
⊢ ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X (f i)) =
    (RingHom.id (MvPolynomial σ R)) (X (f i))

Tactic:
simp [partialInv_left hfi]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ erase i ((monomial i) r) = 0

Tactic:
erase_monomial

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

Tactic:
positivity

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

Tactic:
positivity

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

Goal state before:
pp: case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
positivity

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

Goal state before:
pp: case neg.Cf
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

Tactic:
exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + q).Monic

Tactic:
rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X ^ n).reverse = p.reverse

Tactic:
reverse_mul_X_pow

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.reverse = p.reverse
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
rintro h f g - hg rfl hdg
    exact h g hg hdg (dvd_mul_left g f)

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

Goal state before:
pp: case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩

Goal state after:
case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = p

case inr.mpr.refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₂).natDegree ∈ Ioc 0 (2 / 2)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsLeftRegular p

Tactic:
intro q r h

Goal state after:
case left
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x ↦ p * x) q = (fun x ↦ p * x) r
⊢ q = r
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ IsRightRegular p

Tactic:
intro q r h

Goal state after:
case right
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : p.Monic
q r : R[X]
h : (fun x ↦ x * p) q = (fun x ↦ x * p) r
⊢ q = r
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
⊢ (Multiset.map (⇑leadingCoeffHom) t).prod = (Multiset.map (fun f ↦ f.leadingCoeff) t).prod

Tactic:
simp only [leadingCoeffHom_apply]

Goal state after:
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
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree ≤ ↑n
⊢ ∑ n ∈ p.support, (monomial n) (p.coeff n) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))
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
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]

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

Goal state before:
pp: case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
    exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ⊥ < (P ^ n).degree

Tactic:
rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]
    exact (hP.pow _).ne_zero

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
hP₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * (of R M) (Multiplicative.ofAdd m₂) = (of R M) (Multiplicative.ofAdd (m₁ + m₂))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
hP₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * (of R M) (Multiplicative.ofAdd m₂) = (of R M) (Multiplicative.ofAdd (m₁ + m₂))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this✝¹ : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
this✝ : 0 ≠ 1
this : Nontrivial R
q : R[X]
hq : q ∈ I
hdq : q.degree ≤ ↑N
hlqp : q.leadingCoeff = p.leadingCoeff
H : p = 0
⊢ False

Tactic:
exact hp0 H

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) (m₁ * m₂)

Tactic:
hP₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * (of R M) m₂ = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) (m₁ * m₂)

Tactic:
hP₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) P₂ = (of R M) m₂
⊢ (of R M) m₁ * (of R M) m₂ = (of R M) (m₁ * m₂)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case right
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
a✝ : v ∈ ⊤
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ ((aeval f) (p * p')) v + ((aeval f) (q * q')) v = v

Tactic:
simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add] using!
    congr_arg (fun p : R[X] => aeval f p v) hpq'

Goal state after:
Module: Mathlib.Data.Int.ModEq

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

Tactic:
rw [mul_comm a, mul_comm b, mul_comm n]

Goal state after:
n a b c : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: m a b c : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]

Tactic:
by simpa [mul_comm] using h

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

Goal state before:
pp: R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = ↑(b - a) + ↑a

Tactic:
(cast_eq_zero_iff R p _).mpr h,

Goal state after:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : p ∣ b - a
hle : a ≤ b
⊢ ↑a = 0 + ↑a
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ 2 • x = 0

Tactic:
two_zsmul,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ x + x = 0
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f 1 x

Tactic:
rw [← h]

Goal state after:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsPeriodicPt f (minimalPeriod f x) x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))

Tactic:
intro a' b'

Goal state after:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (permutations'Aux b') (map (cons c) (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x : α
n : ℕ
hn✝ : n < (permutations'Aux x []).length
hn : n = 0
⊢ (permutations'Aux x [])[n] = [].insertIdx n x

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝² : Group G
inst✝¹ : Monoid X
inst✝ : MulAction X G
H : Subgroup G
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H

Tactic:
by
    rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G ⧸ H
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) g) = g

Tactic:
cases g using Quotient.inductionOn' with | _ g

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯)
      ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) (Quotient.mk'' g)) =
    Quotient.mk'' g
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b ∈ H

Tactic:
refine (hc _).or.resolve_left ?_

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
c : G
hc : ∀ (b : G), Xor (b * c ∈ H) (b ∈ H)
⊢ a * b * c ∉ H
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card G' ∣ Nat.card G

Tactic:
rw [← Nat.card_congr (QuotientGroup.quotientKerEquivOfSurjective f hf).toEquiv]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Surjective ⇑f
⊢ Nat.card (G ⧸ f.ker) ∣ Nat.card G
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = n
hn : n = 0
⊢ False

Tactic:
rw [hn] at h

Goal state after:
n : ℕ
R : Type u_1
inst✝² : Ring R
inst✝¹ : CharP R n
inst✝ : Fintype R
h : Fintype.card R = 0
hn : n = 0
⊢ False
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: a : ℕ
x : ZMod a
⊢ (ringEquivCongr ⋯) x = x

Tactic:
rw [ringEquivCongr_refl]

Goal state after:
a : ℕ
x : ZMod a
⊢ (RingEquiv.refl (ZMod a)) x = x
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n : ℕ
hn : ∀ (m : ℕ), 0 < m → m ≤ H.index → m ∣ n
⊢ a ^ n ∈ H

Tactic:
by
  rcases exists_pow_mem_of_index_ne_zero h a with ⟨m, hlt, hle, he⟩
  rcases hn m hlt hle with ⟨k, rfl⟩
  rw [pow_mul]
  exact pow_mem he _

Goal state after:
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ a.val * b.val < n

Tactic:
rw [← h]

Goal state after:
case mp
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : (a * b).val = a.val * b.val
⊢ (a * b).val < n
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
by
    apply card_le_card
    simp only [divisors, filter_subset]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n x y : ℕ
hn : n ≠ 0
⊢ (x, y) ∈ n.divisorsAntidiagonal ↔ x * y = n

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) ↔
    a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding n.divisorsAntidiagonal

Tactic:
map_swap_divisorsAntidiagonal,

Goal state after:
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ map (Equiv.prodComm ℕ ℕ).toEmbedding (map { toFun := fun d ↦ (n / d, d), inj' := ⋯ } n.divisors) ↔
    a✝ ∈ n.divisorsAntidiagonal
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case zero
s : Finset ℕ
hsub : s ⊆ properDivisors 0
⊢ ∑ x ∈ s, x = ∑ x ∈ properDivisors 0, x → s = properDivisors 0

pp: case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors

Tactic:
· rw [properDivisors_zero, subset_empty] at hsub
    simp [hsub]

Goal state after:
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ (n✝ + 1).properDivisors
⊢ ∑ x ∈ s, x = ∑ x ∈ (n✝ + 1).properDivisors, x → s = (n✝ + 1).properDivisors
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f i (n / i)

Tactic:
by
  rw [← map_div_right_divisors, Finset.prod_map]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.Divisors

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f

Tactic:
simp [hn]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Bounds

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
r n : ℕ
⊢ ↑(n.choose r) ≤ ↑n ^ r / ↑r !

Tactic:
by
  rw [le_div_iff₀']
  · norm_cast
    rw [← Nat.descFactorial_eq_factorial_mul_choose]
    exact n.descFactorial_le_pow r
  exact mod_cast r.factorial_pos

Goal state after: