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

Goal state before:
pp: case hX.refine_1
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X 0)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X 0)).coeff n✝

pp: case hX.refine_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ ∀ (i : Fin n),
    (↑(finSuccEquiv R n) (X i.succ)).coeff n✝ =
      ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i.succ)).coeff
        n✝

Tactic:
<;>

Goal state after:
case hX.refine_1
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X 0)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X 0)).coeff n✝

case hX.refine_2
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ ∀ (i : Fin n),
    (↑(finSuccEquiv R n) (X i.succ)).coeff n✝ =
      ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i.succ)).coeff
        n✝
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.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

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:
<;>

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial.e_a.inr
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0

Tactic:
· simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using!
        coeff_monomial m j.tail (1 : R)

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree

Tactic:
exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)

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

Goal state before:
pp: case pos
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : i = n
⊢ (↑p).coeff i = 1

pp: case neg
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : ¬i = n
⊢ (↑p).coeff i = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : i = n
⊢ (↑p).coeff i = 1

case neg
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
i : ℕ
hi : n ≤ i
h✝ : ¬i = n
⊢ (↑p).coeff i = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| coeff (cons i x✝) f ≠ 0 ∧ cons i x✝ = m

Tactic:
Ne

Goal state after:
case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| ¬coeff (cons i x✝) f = 0 ∧ cons i x✝ = m
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)

Tactic:
have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
⊢ ((finSuccEquiv R n) f).degree = ↑(degreeOf 0 f)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0

Tactic:
rw [ha.natDegree_eq_zero, hb.natDegree_eq_zero]

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

Goal state before:
pp: case hX.none
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X none) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X none)

pp: case hX.some
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
i : σ
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X (Option.some i)) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X (Option.some i))

Tactic:
<;>

Goal state after:
case hX.none
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X none) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X none)

case hX.some
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
i : σ
⊢ ((finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)).toRingHom)
      (X (Option.some i)) =
    ((Polynomial.mapRingHom (rename ⇑e).toRingHom).comp ↑(optionEquivLeft R σ)) (X (Option.some i))
Module: Mathlib.Algebra.Polynomial.Monic

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

pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case h₁
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
x✝ : R
⊢ (((eval f).comp ↑(toMvPolynomial i)).comp Polynomial.C) x✝ = ((evalRingHom (f i)).comp Polynomial.C) x✝

pp: case h₂
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ ((eval f).comp ↑(toMvPolynomial i)) Polynomial.X = (evalRingHom (f i)) Polynomial.X

Tactic:
<;>

Goal state after:
case h₁
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
x✝ : R
⊢ (((eval f).comp ↑(toMvPolynomial i)).comp Polynomial.C) x✝ = ((evalRingHom (f i)).comp Polynomial.C) x✝

case h₂
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ ((eval f).comp ↑(toMvPolynomial i)) Polynomial.X = (evalRingHom (f i)) Polynomial.X
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
f g : R[X]
hf : f.Monic
hg : g.Monic
he : f * g = p
⊢ f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

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

pp: case e_a.e_a.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

Tactic:
<;>

Goal state after:
case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum

case e_a.e_a.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
rw [pow_mul]; exact sub_one_dvd_pow_sub_one (x ^ m) n

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

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

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ p * q = 0 ↔ q = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ p * q = 0 ↔ q = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ p * q = 0 ↔ q = 0
Module: Mathlib.Algebra.Polynomial.Monic

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

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : q = 0
⊢ q * p = 0 ↔ q = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
hq : ¬q = 0
⊢ q * p = 0 ↔ q = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n + ↑p).natDegree = n

Tactic:
by
        rw [natDegree_add_eq_left_of_degree_lt]
        · simp
        · simp [mem_degreeLT.1 p.2]

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

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ Function.LeftInverse (fun p ↦ ⟨X ^ n + ↑p, ⋯⟩) fun p ↦ ⟨(↑p).eraseLead, ⋯⟩

Tactic:
by
    rintro ⟨p, hp, rfl⟩
    ext1
    simp only
    conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]
    simp [Monic.def.1 hp, add_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Tactic:
by
  refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm
  simpa only [tsub_add_cancel_of_le (by lia : 1 ≤ m), eq_comm] using geom_sum_mul_add (m - 1) n

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : i = 0
⊢ 1 = ↑1

pp: case neg
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : ¬i = 0
⊢ 0 = ↑0

Tactic:
<;>

Goal state after:
case pos
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : i = 0
⊢ 1 = ↑1

case neg
R : Type u
inst✝ : Ring R
i : ℕ
h✝ : ¬i = 0
⊢ 0 = ↑0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (mapRingHom f) ↔ x✝ ∈ map C (RingHom.ker f)

Tactic:
simp only [RingHom.mem_ker, coe_mapRingHom]

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Semiring S
f : R →+* S
x✝ : R[X]
⊢ Polynomial.map f x✝ = 0 ↔ x✝ ∈ map C (RingHom.ker f)
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
⊢ x ∈ toSubmodule (ofId (↥S') S).range

Tactic:
have hN := Ideal.span_pow_eq_top _ this N

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
this : Ideal.span (s' '' ↑ι') = ⊤
N : ℕ := ι'.sup n
hN : Ideal.span ((fun x ↦ x ^ N) '' s' '' ↑ι') = ⊤
⊢ x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ s f, Surjective ⇑f

pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S

Tactic:
· rintro ⟨s, hs⟩
    use s, MvPolynomial.aeval (↑)
    intro x
    rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, SetLike.mem_coe, hs]
    apply mem_top

Goal state after:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B

Tactic:
by
  rw [FiniteType, toAlgebra_algebraMap]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
suffices of R M '' ⋃ f ∈ S, f.coeff.support = ⋃ f ∈ S, of R M '' f.coeff.support by
    rw [this]
    exact support_gen_of_gen hS

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ i (nj j) ∈ M'

Tactic:
rw [← hc, piEquiv_apply_apply]

Goal state after:
case refine_1.mem.inr
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝² : AddCommMonoid M
x✝¹ : Module R M
x✝ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x : ↥N
j : Fin k
⊢ ∑ i, c j i • mj i ∈ M'
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case e'_1
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.24 * (m / c)

pp: case e'_2
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = ?m.24 * (a / c)

pp: case e'_3
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = ?m.24 * (b / c)

pp: m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ ℤ

Tactic:
<;>

Goal state after:
case e'_1
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.24 * (m / c)

case e'_2
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = ?m.24 * (a / c)

case e'_3
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = ?m.24 * (b / c)

m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ ℤ
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ (Ideal.Quotient.mk I) v = 0

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ v ∈ I
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b

pp: case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
<;>

Goal state after:
case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b

case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs ≡ a [ZMOD b]
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b

pp: case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]

Tactic:
<;>

Goal state after:
case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b

case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inl.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑0
⊢ 0 = 0

pp: case inl.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑1
⊢ 0 = 1

pp: case inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑(-1)
⊢ 0 = -1

pp: case inr.inl.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑0
⊢ 1 = 0

pp: case inr.inl.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑1
⊢ 1 = 1

pp: case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑(-1)
⊢ 1 = -1

pp: case inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑0
⊢ -1 = 0

pp: case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑1
⊢ -1 = 1

pp: case inr.inr.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑(-1)
⊢ -1 = -1

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑0
⊢ 0 = 0

case inl.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑1
⊢ 0 = 1

case inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑0 = ↑(-1)
⊢ 0 = -1

case inr.inl.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑0
⊢ 1 = 0

case inr.inl.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑1
⊢ 1 = 1

case inr.inl.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑1 = ↑(-1)
⊢ 1 = -1

case inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑0
⊢ -1 = 0

case inr.inr.inr.inl
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑1
⊢ -1 = 1

case inr.inr.inr.inr
R : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
h : ↑(-1) = ↑(-1)
⊢ -1 = -1
Module: Mathlib.Algebra.GroupWithZero.Units.Fintype

Goal state before:
pp: case inl
α : Type u_1
x : ℤˣ
h✝ : x = 1
⊢ x ∈ {1, -1}

pp: case inr
α : Type u_1
x : ℤˣ
h✝ : x = -1
⊢ x ∈ {1, -1}

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
x : ℤˣ
h✝ : x = 1
⊢ x ∈ {1, -1}

case inr
α : Type u_1
x : ℤˣ
h✝ : x = -1
⊢ x ∈ {1, -1}
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ↑0 = if Even 0 then 0 else 1

pp: case succ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n✝ : ℕ
a✝ : ↑n✝ = if Even n✝ then 0 else 1
⊢ ↑(n✝ + 1) = if Even (n✝ + 1) then 0 else 1

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ ↑0 = if Even 0 then 0 else 1

case succ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
n✝ : ℕ
a✝ : ↑n✝ = if Even n✝ then 0 else 1
⊢ ↑(n✝ + 1) = if Even (n✝ + 1) then 0 else 1
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑↑n = if Even ↑n then 0 else 1

pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑(-↑n) = if Even (-↑n) then 0 else 1

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑↑n = if Even ↑n then 0 else 1

case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
n : ℕ
⊢ ↑(-↑n) = if Even (-↑n) then 0 else 1