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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∑ a ∈ x.support, (Finsupp.single (f a) (x a)) i = 0

Tactic:
Finset.sum_eq_zero

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ 0 = 0

R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
hi : ∀ a ∈ φ.degrees, f a ≠ i
⊢ ∀ x_1 ∈ x.support, (Finsupp.single (f x_1) (x x_1)) i = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = 0

Tactic:
Finset.sum_eq_zero

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ 0 = 0

case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
⊢ ∀ x ∈ p.support, (f (coeff x p) * x.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (C c * p) ≤ degreeOf i p

Tactic:
unfold degreeOf
  convert! Multiset.count_le_of_le i degrees_mul_le
  simp only [degrees_C, zero_add]

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
b : τ →₀ ℕ
h : b ∈ ((rename f) p).support
⊢ (b.sum fun x e ↦ e) ≤ p.totalDegree

Tactic:
by
    classical
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a

case neg
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : #((monomial n) a).support ≤ 1
ha : ¬a = 0
⊢ (monomial ((monomial n) a).natDegree) ((monomial n) a).leadingCoeff = (monomial n) a
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
| insert x s hx IH =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
⊢ reflect N (C r * f) = C r * reflect N f

Tactic:
ext
  simp only [coeff_reflect, coeff_C_mul]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (∃ x, C x = f) ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0

Tactic:
obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).eraseLead.coeff ((C a).natDegree - 1) = 0

case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : 0 < f.natDegree
h : f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ coeff d ((uniqueAlgEquiv R σ).symm P) = P.coeff (d default)

Tactic:
Finsupp.unique_single d,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ coeff (Finsupp.single default (d default)) ((uniqueAlgEquiv R σ).symm P) =
    P.coeff ((Finsupp.single default (d default)) default)
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
⊢ φ r * a default ^ d default = φ r * d.prod fun n e ↦ a n ^ e

Tactic:
Finsupp.unique_single d,

Goal state after:
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
⊢ φ r * a default ^ (Finsupp.single default (d default)) default =
    φ r * (Finsupp.single default (d default)).prod fun n e ↦ a n ^ e
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 1 ↔ ∃ a, a ≠ 0 ∧ ∃ b, C a * X + C b = p

Tactic:
refine ⟨fun hp ↦ ⟨p.coeff 1, fun h ↦ ?_, p.coeff 0, ?_⟩, ?_⟩
  · rw [← hp, coeff_natDegree, leadingCoeff_eq_zero] at h
    simp_all
  · ext n
    obtain _ | _ | n := n
    · simp
    · simp
    · simp only [coeff_add, coeff_mul_X, coeff_C_succ, add_zero]
      rw [coeff_eq_zero_of_natDegree_lt]
      simp [hp]
  · rintro ⟨a, ha, b, rfl⟩
    simp [ha]

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

pp: case neg.Nf
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.natDegree ≤ N

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

Goal state after:
case neg.Nf
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.natDegree ≤ N
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ (comp 0 q).degree = degree 0 * q.degree

Tactic:
rw [zero_comp, degree_zero, WithBot.bot_mul']

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = if q.degree = 0 then 0 else ⊥
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = f.support.sup fun m ↦ m none

Tactic:
support_optionEquivLeft,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ ((Finset.image (fun m ↦ m none) f.support).sup fun x ↦ x) = f.support.sup fun m ↦ 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
h : q.natDegree ≠ 0
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

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
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
⊢ (eval (Fin.cons y s)) f = Polynomial.eval y (Polynomial.map (eval s) ((finSuccEquiv R n) f))

Tactic:
let φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
    { Polynomial.mapRingHom (eval s) with
      commutes' := fun r => by
        convert! Polynomial.map_C (eval s)
        exact (eval_C _).symm }
  change
    aeval (Fin.cons y s : Fin (n + 1) → R) f =
      (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
  congr 2
  apply MvPolynomial.algHom_ext
  rw [Fin.forall_iff_succ]
  simp only [aeval_X, Fin.cons_zero, AlgHom.coe_comp, Polynomial.coe_aeval_eq_eval,
    AlgHom.coe_mk, Polynomial.coe_mapRingHom, AlgEquiv.coe_toAlgHom,
    comp_apply, finSuccEquiv_apply, eval₂Hom_X', Fin.cases_zero, Polynomial.map_X,
    Polynomial.eval_X, Fin.cons_succ, Fin.cases_succ, Polynomial.map_C, eval_X, Polynomial.eval_C,
    implies_true, and_self, φ]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
l : Multiset S[X]
⊢ ∀ (a : List S[X]), (Multiset.sum ⟦a⟧).natDegree ≤ foldr max 0 (Multiset.map natDegree ⟦a⟧)

Tactic:
simpa using natDegree_list_sum_le

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

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

Tactic:
intro a t ih ht

Goal state after:
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.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree * 2 ≤ p.natDegree)

Tactic:
mul_two

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Module: Mathlib.Algebra.Polynomial.BigOperators

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

Tactic:
nontriviality R
  convert! multiset_prod_X_sub_C_nextCoeff (by assumption)
  rw [nextCoeff, if_neg]
  swap
  · rw [natDegree_multiset_prod_of_monic]
    swap
    · simp only [Multiset.mem_map]
      rintro _ ⟨_, _, rfl⟩
      apply monic_X_sub_C
    simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]
    obtain ⟨x, hx⟩ := card_pos_iff_exists_mem.mp ht
    exact fun h => one_ne_zero <| h 1 ⟨_, ⟨x, hx, rfl⟩, natDegree_X_sub_C _⟩
  congr; rw [natDegree_multiset_prod_of_monic] <;> · simp [monic_X_sub_C]

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

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

pp: 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)

Tactic:
· rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
        ring

Goal state after:
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.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).degree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
apply Finset.sup_le
    intro i hi
    by_cases hf : f i = 0
    · simp [hf]
    rw [degree_eq_natDegree hf]
    apply le_degree_of_ne_zero
    rw [finsetSum_coeff]
    conv in (fun _ ↦ _) =>
      ext
      rw [coeff_smul, smul_eq_mul, coeff_map, mul_comm, ← Algebra.smul_def]
    intro H
    exact hf (leadingCoeff_eq_zero.mp (linearIndepOn_finset_iff.mp h _ H i hi))

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
  induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_ofPred_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H

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

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
this : ∀ (x : C), ∃ f, Function.support f ⊆ ↑y ∧ ∑ a ∈ y, f a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
choose f _ hf using this

Goal state after:
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG
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
⊢ ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree

Tactic:
simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ∀ b < n, ↑(P ^ b).natDegree < ↑(P ^ n).natDegree
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 : q.leadingCoeff = 0
⊢ False

Tactic:
hlqp,

Goal state after:
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.leadingCoeff = 0
⊢ False
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
⊢ AddMonoid.FG M

Tactic:
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : AddMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R R[M]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
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₂
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (m₁ * m₂)

Tactic:
exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
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
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
· rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
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₂
⊢ ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (m₁ * m₂)

Tactic:
exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
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
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) x) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) y) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ (of R M) ↑s) a = (of R M) (x * y)

Tactic:
· rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩

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

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

Tactic:
intro hx
    obtain ⟨y, hy⟩ := Quotient.mk_surjective x
    rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
    rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
    exact ⟨y, hx, rfl⟩

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

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ InjOn Int.cast {0, 1, -1}

Tactic:
by
  rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;>
  simp only
    [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
  · exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim
  · exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim

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

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ l ∈ s.lists ↔ s = ⟦l⟧

Tactic:
by
  induction s using Quotient.inductionOn
  simpa using perm_comm

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

Goal state before:
pp: case pos.refine_1
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)

pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
· rintro ⟨hr, H⟩ n hn
      rcases eq_or_lt_of_le (Nat.lt_succ_iff.1 hn) with hM' | hM'
      · rwa [hM', hM, iterate_minimalPeriod]
      · exact H _ hM'

Goal state after:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)