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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
⊢ (p - ((monomial d) c - (monomial d') c)).support ⊆ p.support.erase d ∪ {d'}

Tactic:
intro x hx
  have hd_not := notMem_support_sub_monomial_sub_monomial p d d' c hdd' hc
  rcases Finset.mem_union.mp (support_sub σ p _ hx) with hp | hdelta
  · by_cases hxd : x = d
    · exact absurd (hxd ▸ hx) hd_not
    exact Finset.mem_union_left _ (Finset.mem_erase.mpr ⟨hxd, hp⟩)
  rcases Finset.mem_union.mp (support_sub σ _ _ hdelta) with h1 | h2
  · rw [support_monomial] at h1
    split_ifs at h1
    · exact absurd h1 (Finset.notMem_empty _)
    exact absurd ((Finset.mem_singleton.mp h1) ▸ hx) hd_not
  rw [support_monomial] at h2
  split_ifs at h2
  · exact absurd h2 (Finset.notMem_empty _)
  exact Finset.mem_union_right _ (by rwa [Finset.mem_singleton] at h2 ⊢)

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

Goal state before:
pp: case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i ↦ (φ i).vars
⊢ (φ a✝ + ∑ x ∈ s✝, φ x).vars = (φ a✝).vars ∪ s✝.biUnion fun i ↦ (φ i).vars

Tactic:
vars_add_of_disjoint,

Goal state after:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i ↦ (φ i).vars
⊢ (φ a✝).vars ∪ (∑ x ∈ s✝, φ x).vars = (φ a✝).vars ∪ s✝.biUnion fun i ↦ (φ i).vars

case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i ↦ (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i ↦ (φ i).vars
⊢ Disjoint (φ a✝).vars (∑ x ∈ s✝, φ x).vars
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Algebra.adjoin R (range f) ≤ (aeval f).range

Tactic:
rw [Algebra.adjoin_le_iff]

Goal state after:
case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ range f ⊆ ↑(aeval f).range
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
x✝ : σ → A
i✝ : σ
⊢ (aevalTower (Algebra.ofId S A) x✝) (X i✝) = (aeval x✝) (X i✝)

Tactic:
simp only [aeval_X, aevalTower_X]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree ≤ p.degrees.card

Tactic:
rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
this : f✝ (b + coeff a f) ∈ s
⊢ f✝ (coeff a f) ∈ s

Tactic:
rw [MvPolynomial.notMem_support_iff.1 ha, map_zero]

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
subS : Type u_3
inst✝² : CommSemiring S
inst✝¹ : SetLike subS S
inst✝ : SubsemiringClass subS S
f✝ : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : (∀ (i : σ →₀ ℕ), f✝ (coeff i f) ∈ s) → eval₂ f✝ v f ∈ s
hs : ∀ (i : σ →₀ ℕ), f✝ (coeff i ((monomial a) b + f)) ∈ s
this : f✝ (b + coeff a f) ∈ s
⊢ 0 ∈ s
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0

Tactic:
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : 1 < #f.support
⊢ f.eraseLead.natDegree < f.natDegree ∨ f.eraseLead = 0

Tactic:
left
    apply eraseLead_natDegree_lt h

Goal state after:
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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)

Tactic:
degree_eq_natDegree hb',

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)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ ↑(f b).natDegree ≤ s.sup' hs (WithBot.some ∘ fun i ↦ (f i).natDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
φ : R →+* S
a : σ → S
d : σ →₀ ℕ
r : R
⊢ a default ^ 0 = 1

Tactic:
· simp only [pow_zero]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
by_cases hp0 : p = 0

Goal state after:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

Tactic:
intro
      simp [eq_iff_true_of_subsingleton]

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
hq : q.Monic
h : q.natDegree ≠ 0
⊢ (p.comp q).Monic

Tactic:
by
  nontriviality R
  have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
    natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]
  rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a ∈ (((finSuccEquiv R n) f).coeff i).support, cons i a = m) ↔ coeff m f ≠ 0 ∧ m 0 = i

Tactic:
conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ m 0 = i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ Irreducible p ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

Tactic:
refine
    ⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
      ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
        (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
          (.of_mul_eq_one _)
          (.of_mul_eq_one _)⟩⟩

Goal state after:
case refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (g * C f.leadingCoeff).Monic

case refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ (f * C g.leadingCoeff).Monic

case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * C f.leadingCoeff * (f * C g.leadingCoeff) = p
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: 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

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons] at ht ⊢

Goal state after:
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 : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ (a * t.prod).natDegree = (a.natDegree ::ₘ Multiset.map (fun f ↦ f.natDegree) t).sum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
by
  simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ p * q = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0 <;> simp [h.mul_right_ne_zero, hq]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : X ^ (n + 1) ∈ degreeLE R ↑n
⊢ False

Tactic:
rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
this : 1 = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ i ∈ p.restriction.support ↔ i ∈ p.support

Tactic:
simp only [mem_support_iff, not_iff_not, Ne]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
i : ℕ
⊢ p.restriction.coeff i = 0 ↔ p.coeff i = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R[X]
hIJ : I ≤ J
⊢ I.leadingCoeff ≤ J.leadingCoeff

Tactic:
intro x hx
  rcases (I.mem_leadingCoeff x).1 hx with ⟨p, hpI, rfl⟩
  exact (J.mem_leadingCoeff p.leadingCoeff).2 ⟨p, hIJ hpI, rfl⟩

Goal state after:
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
i j : ℕ
hij : (i, j) ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij

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 : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι S)
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
⊢ FiniteType R (FreeAlgebra S ι)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_1
inst✝¹ : Finite ι
inst✝ : FiniteType R S
val✝ : Fintype ι
⊢ FiniteType R (FreeAlgebra S ι)
Module: Mathlib.Data.Int.ModEq

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

Tactic:
by
  rw [add_comm, add_modulus_modEq_iff]

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
hI : Pairwise (IsCoprime on I)
⊢ Surjective ⇑(quotientInfToPiQuotient I)

Tactic:
cases nonempty_fintype ι

Goal state after:
case intro
R : Type u_2
inst✝¹ : CommRing R
ι : Type u_3
inst✝ : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val✝ : Fintype ι
⊢ Surjective ⇑(quotientInfToPiQuotient I)
Module: Mathlib.Algebra.CharP.Two

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

Tactic:
← two_mul x,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharP R 2
x : R
⊢ 2 * x = 0
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:
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.Fintype.List

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : Fintype α
univSubsets : Multiset (Finset α) := ⋯
allPerms : Multiset (List α) := ⋯
m n : Finset α
this :
  (∀ ⦃x : Multiset (List α)⦄, x ≤ ↑m.toList.permutations → x ≤ ↑n.toList.permutations → x ≤ ⊥) ↔
    m.toList.permutations.Disjoint n.toList.permutations
⊢ ¬m = n → ∀ a ∈ m.toList.permutations, ∀ b ∈ n.toList.permutations, a ≠ b

Tactic:
intro h
        simp only [mem_permutations]
        intro a ha b hb
        by_contra hab
        absurd h
        rw [hab] at ha
        exact Finset.perm_toList.mp <| Perm.trans ha.symm hb

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

Goal state before:
pp: case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x

Tactic:
rw [tsub_eq_zero_iff_le.mpr h]
    apply isPeriodicPt_zero

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

Tactic:
exact hxs' _ (mem_cons_of_mem _ mem_cons_self)

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

Goal state before:
pp: α : Type u_1
f : α → α
inst✝ : Finite α
h : Injective f
x : α
⊢ x ∈ periodicPts f

Tactic:
obtain ⟨m, n, heq, hne⟩ : ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n := by
    simpa [Injective] using not_injective_infinite_finite (f^[·] x)
  rcases lt_or_gt_of_ne hne with hlt | hlt
  · exact mk_mem_periodicPts (by lia) (iterate_cancel h heq.symm)
  · exact mk_mem_periodicPts (by lia) (iterate_cancel h heq)

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

Goal state before:
pp: α : Type u_1
l : List α
hl : l.Nodup
⊢ (↑l).Nontrivial ↔ 2 ≤ l.length

Tactic:
rw [Nontrivial]

Goal state after:
α : Type u_1
l : List α
hl : l.Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ l.length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ next (Quot.mk (⇑(IsRotated.setoid α)) a✝) hs x hx ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝

Tactic:
apply next_mem

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
a✝ : List α
hs : Nodup (Quot.mk (⇑(IsRotated.setoid α)) a✝)
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) a✝
⊢ x ∈ a✝
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ ∈ s.reverse

Tactic:
apply next_mem

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m

Tactic:
by
  grind [isPrimePow_nat_iff, Nat.dvd_prime_pow, Nat.pow_eq_one]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
· rwa [ha, inv_mem_iff (x := b)]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ K ⊓ L).relIndex L ≠ 0

Tactic:
inf_assoc

Goal state after:
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hK : (K ⊓ L).relIndex L ≠ 0
hH : (H ⊓ (K ⊓ L)).relIndex (K ⊓ L) ≠ 0
⊢ (H ⊓ (K ⊓ L)).relIndex L ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑((↑u).val * (↑u⁻¹).val % (n + 1))

Tactic:
natCast_mod

Goal state after:
case succ
n : ℕ
u : (ZMod (n + 1))ˣ
⊢ ↑((↑u).val * (↑u⁻¹).val) = ↑((↑u).val * (↑u⁻¹).val)
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: m n : ℕ
H : IsUnit ↑m
H' : (m % n).Coprime n
⊢ m.Coprime n

Tactic:
Nat.coprime_iff_gcd_eq_one

Goal state after:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n
Module: Mathlib.Algebra.Order.Ring.GeomSum

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, (-1) ^ i ≠ 0

Tactic:
neg_one_geom_sum

Goal state after:
case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
have : NeZero b := ⟨hb⟩

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a - b).val = a.val - b.val
Module: Mathlib.Data.Nat.MaxPowDiv

Goal state before:
pp: p✝ n p : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hp : 1 < p ∧ n ≠ 0
hmod : n % p = 0
⊢ 1 < p * p ∧ n ≠ 0

Tactic:
simp [Nat.one_lt_mul_iff, hp, Nat.lt_trans Nat.one_pos]

Goal state after:
Module: Mathlib.RingTheory.Multiplicity

Goal state before:
pp: a b : ℕ
h : a = 1 ∨ b = 0
⊢ ∀ (n : ℕ), a ^ n ∣ b

Tactic:
cases h <;> simp [*]

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

Goal state before:
pp: d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ (∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p) ↔ d ∣ n

Tactic:
by
  rw [← factorization_le_iff_dvd hd hn]
  refine ⟨fun h p => (em p.Prime).elim (h p) fun hp => ?_, fun h p _ => h p⟩
  simp_rw [factorization_eq_zero_of_not_prime _ hp]
  rfl

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, a.factorization p < b.factorization p

Tactic:
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
  contrapose! hab
  rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
  exact le_of_dvd ha.bot_lt hab

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

Goal state before:
pp: case ha
p k : ℕ
hp : Prime p
⊢ p ^ k / p ^ (p ^ k).factorization p ≠ 0

Tactic:
exact pos_iff_ne_zero.mp (ordCompl_pos p (pow_ne_zero k hp.ne_zero))

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

Goal state before:
pp: n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k

Tactic:
conv_rhs => rw [← prod_factorization_pow_eq_self (choose_ne_zero hkn)]
  rw [eq_comm]
  apply Finset.prod_subset
  · intro p hp
    rw [Finset.mem_range]
    contrapose! hp
    rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
  · intro p _ h2
    simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)

Tactic:
simpa using h.add_pow_prime_pow_eq hp 1

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

Goal state before:
pp: p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
obtain hkp | hkp := hkp.symm.lt_or_gt
  · simp [choose_eq_zero_of_lt hkp]
  refine emultiplicity_ne_zero.1 fun h => hkp.not_ge <| Nat.le_of_dvd hk.bot_lt ?_
  have H := hp.emultiplicity_choose_prime_pow_add_emultiplicity hkp.le hk
  rw [h, zero_add, emultiplicity_eq_coe] at H
  exact H.1

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
⊢ (X ^ n).divX = if n = 0 then 0 else X ^ (n - 1)

Tactic:
by
  cases n
  · simp
  · ext n
    simp [coeff_X_pow]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
apply map_natDegree_eq_sub (φ := divX_hom)

Goal state after:
case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0

case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1
Module: Mathlib.Algebra.Polynomial.Inductions

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : C (p.coeff 0) ≠ 0
⊢ ¬C ((C (p.coeff 0)).coeff 0) = 0

Tactic:
simpa using h'

Goal state after: