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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q

Tactic:
apply MvPolynomial.induction_on q

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (a : R) {p : MvPolynomial σ R}, eval₂ f g (p * C a) = eval₂ f g p * eval₂ f g (C a)

case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      (∀ {p : MvPolynomial σ R}, eval₂ f g (p * q) = eval₂ f g p * eval₂ f g q) →
        ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p + q)) = eval₂ f g p_1 * eval₂ f g (p + q)

case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * p) = eval₂ f g p_1 * eval₂ f g p) →
      ∀ {p_1 : MvPolynomial σ R}, eval₂ f g (p_1 * (p * X n)) = eval₂ f g p_1 * eval₂ f g (p * X n)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mul_X
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
i : σ
hp : p ∈ S
⊢ p * X i ∈ S

Tactic:
exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
inst✝ : DecidableEq S₁
⊢ ((map f) p).coeffs ⊆ Finset.image (⇑f) p.coeffs

Tactic:
classical
  induction p using induction_on'' with
  | C a => aesop (add simp coeffs_C)
  | mul_X p n ih => simpa
  | monomial_add a s p ha hs hp ih =>
    rw [coeffs_add (disjoint_support_monomial ha hs), map_add, coeffs_add]
    · rw [Finset.image_union, Finset.union_subset_iff]
      exact ⟨ih.trans (by simp), hp.trans (by simp)⟩
    · exact Finset.disjoint_of_subset_left (support_map_subset _ _) <|
        Finset.disjoint_of_subset_right (support_map_subset _ _) <|
          disjoint_support_monomial ha hs

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

Goal state before:
pp: case inl
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
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hp : x ∈ p.support
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
by_cases hxd : x = d
    · exact absurd (hxd ▸ hx) hd_not
    exact Finset.mem_union_left _ (Finset.mem_erase.mpr ⟨hxd, hp⟩)

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

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : (p.support.sup fun s ↦ s i) = s i
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ b i

Tactic:
← degreeOf_eq_sup i p

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
this : p.support.Nonempty
s : σ →₀ ℕ
hs1 : s ∈ p.support
hs2 : degreeOf i p = s i
⊢ ∃ b ∈ (p + q).support, degreeOf i p ≤ b i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : (f.support.sup fun s ↦ s.sum fun x e ↦ e) < ∑ i ∈ d.support, d i
⊢ ⊥ < ∑ i ∈ d.support, d i

Tactic:
· exact lt_of_le_of_lt (Nat.zero_le _) h

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
exact le_antisymm natDegree_comp_le (by simp [hq])

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ ↑n < ⊤

Tactic:
exact WithTop.coe_lt_top n

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

Goal state before:
pp: case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * X ^ n).natTrailingDegree ≤ p.natTrailingDegree + n

Tactic:
refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_

Goal state after:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * X ^ n).coeff (p.natTrailingDegree + n) = 0
⊢ p.trailingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
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)
H : ∃ x ∈ s, f x ≠ 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
obtain ⟨x, hx, hx'⟩ := H

Goal state after:
case pos
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
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
⊢ motive f

Tactic:
convert! zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
⊢ f = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
key,

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : (C (p.coeff 0)).comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : p = C (p.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
key,

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp (C (q.coeff 0)) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
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
  by_cases hp0 : p = 0
  · simp [hp0]
  exact irreducible_mul_isUnit
    (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0

Tactic:
← mul_one (eval₂ i (⅟x) _),

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) * 1 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0

Tactic:
rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivRight R S₁) (X (Option.some x)) = X x

Tactic:
simp [optionEquivRight_apply, aeval_X]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivRight R S₁) (X none) = C Polynomial.X

Tactic:
simp [optionEquivRight_apply, aeval_X]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
⊢ f.natDegree < g.natDegree →
    g.natDegree ≤ p.natDegree →
      (φ f).natDegree = fu f.natDegree → (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
fg

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
⊢ g.natDegree ≤ p.natDegree →
    (φ f).natDegree = fu f.natDegree → (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
nontriviality R
  have hdeg : p.degree = 0 := by
    rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]
    · rw [hp.leadingCoeff, f.map_one]
      exact one_ne_zero
  have hndeg : p.natDegree = 0 :=
    WithBot.coe_eq_coe.mp ((degree_eq_natDegree hp.ne_zero).symm.trans hdeg)
  convert! eq_C_of_degree_eq_zero hdeg
  rw [← hndeg, ← Polynomial.leadingCoeff, hp.leadingCoeff, C.map_one]

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
k : ℕ
hk : k ∈ p.support
⊢ (monomial k) (p.coeff k) ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
by
  rw [sum_Ico_eq_sub _ hmn]
  have :
    ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
      ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
    refine sum_congr rfl fun j j_in => ?_
    rw [← pow_add]
    congr
    rw [mem_range] at j_in
    lia
  rw [this]
  simp_rw [pow_mul_comm y (n - m) _]
  simp_rw [← mul_assoc]
  rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), f.coeff n ∈ I

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf

Goal state after:
case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (n : ℕ), x.coeff n ∈ I

case mp.refine_2
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (n : ℕ), coeff 0 n ∈ I

case mp.refine_3
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (x y : R[X]),
    x ∈ Submodule.span R[X] (⇑C '' ↑I) →
      y ∈ Submodule.span R[X] (⇑C '' ↑I) →
        (∀ (n : ℕ), x.coeff n ∈ I) → (∀ (n : ℕ), y.coeff n ∈ I) → ∀ (n : ℕ), (x + y).coeff n ∈ I

case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I
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
H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'
⊢ x ∈ S'

Tactic:
suffices x ∈ Subalgebra.toSubmodule (Algebra.ofId S' S).range by
    obtain ⟨x, rfl⟩ := this
    exact x.2

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
H : ∀ (i : ι), ∃ n, s i ^ n • x ∈ S'
⊢ x ∈ toSubmodule (ofId (↥S') S).range
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case convert_3
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
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)) = restrictScalars A ⊤

Tactic:
rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]

Goal state after:
case convert_3
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
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
hyy :
  span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) * span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y) ≤
    span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
⊢ ↑(Submonoid.closure ↑x) ⊆ ↑(restrictScalars A (span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.inr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree = ↑n
⊢ ∃ p_1 ∈ I, p_1.degree ≤ ↑n ∧ p_1.leadingCoeff = p.coeff n

Tactic:
· refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
      rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
p : Ideal R
x : R
⊢ x ∈ (map C p).leadingCoeff → x ∈ p

pp: case mpr
R : Type u
inst✝ : CommSemiring R
p : Ideal R
x : R
⊢ x ∈ p → x ∈ (map C p).leadingCoeff

Tactic:
· intro hx
    rcases ((map C p).mem_leadingCoeff x).1 hx with ⟨f, hf, rfl⟩
    exact p.mem_map_C_iff.1 hf f.natDegree

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
p : Ideal R
x : R
⊢ x ∈ p → x ∈ (map C p).leadingCoeff
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 = 0
⊢ False

Tactic:
rw [← Polynomial.leadingCoeff_eq_zero] at H

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 : q.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]
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S

Tactic:
exact mem_closure_of_mem_span_closure hm

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule (S ⊔ T) ≤ toSubmodule S * toSubmodule T

Tactic:
rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
⊢ x ∈ toSubmodule S * toSubmodule T
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m f ∈ I

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hf

Goal state after:
case mp.refine_1
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ x ∈ ⇑C '' ↑I, ∀ (m : σ →₀ ℕ), coeff m x ∈ I

case mp.refine_2
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (m : σ →₀ ℕ), coeff m 0 ∈ I

case mp.refine_3
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (x y : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      y ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
        (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → (∀ (m : σ →₀ ℕ), coeff m y ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (x + y) ∈ I

case mp.refine_4
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal R
f : MvPolynomial σ R
hf : f ∈ Ideal.map C I
⊢ ∀ (a x : MvPolynomial σ R),
    x ∈ Submodule.span (MvPolynomial σ R) (⇑C '' ↑I) →
      (∀ (m : σ →₀ ℕ), coeff m x ∈ I) → ∀ (m : σ →₀ ℕ), coeff m (a • x) ∈ I
Module: Mathlib.Algebra.Algebra.Subalgebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : Module R A
inst✝³ : SMulCommClass R A A
inst✝² : IsScalarTower R A A
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₙₐ[R] C
c : Subalgebra R C
⊢ (lift f).range ≤ c ↔ Algebra.adjoin R ↑(NonUnitalAlgHom.range f) ≤ c

Tactic:
by rw [lift_range_le, Algebra.adjoin_le_iff]; rfl

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

Goal state before:
pp: case mp
m n : ℕ
h : ¬m.Coprime n
⊢ ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n

Tactic:
exact
      ⟨minFac (gcd m n), minFac_prime h, (minFac_dvd (gcd m n)).trans (gcd_dvd_left m n),
        (minFac_dvd (gcd m n)).trans (gcd_dvd_right m n)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
l : List α
f : Finset α
hf : f.val = ↑l
⊢ l.Nodup ↔ f.val.Nodup

Tactic:
rw [hf]

Goal state after:
α : Type u_1
inst✝ : Fintype α
l : List α
f : Finset α
hf : f.val = ↑l
⊢ l.Nodup ↔ (↑l).Nodup
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd

Tactic:
induction ys generalizing f <;> simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length

Tactic:
induction ys generalizing f <;> simp [*]

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

Goal state before:
pp: α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x

Tactic:
rw [IsPeriodicPt, iterate_add]
  exact hn.comp hm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
lpos : 0 < l.length
key : l.length - 1 - k < l.length
⊢ (pmap l.reverse.prev l.reverse ⋯)[l.length - 1 - k] = (l.rotate 1)[k]

Tactic:
simp_rw [pmap_prev_eq_rotate_length_sub_one _ (nodup_reverse.mpr h), rotate_reverse,
      length_reverse, Nat.mod_eq_of_lt (Nat.sub_lt lpos Nat.succ_pos'),
      Nat.sub_sub_self (Nat.succ_le_of_lt lpos)]
    rw [getElem_eq_getElem_reverse]
    · simp [Nat.sub_sub_self (Nat.le_sub_one_of_lt hk)]

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
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : g₁ * g₂⁻¹ ∈ H
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧

Tactic:
simp only [Quotient.eq, orbitRel_apply, mem_orbit_iff]

Goal state after:
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : g₁ * g₂⁻¹ ∈ H
⊢ ∃ x, x • g₂ • b = g₁ • b
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
⊢ ∀ (x : G ⧸ H), ((MulAction.toPermHom G (G ⧸ H)) g) x = 1 x

Tactic:
refine fun q ↦ QuotientGroup.induction_on q ?_

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
⊢ ∀ (z : G), ((MulAction.toPermHom G (G ⧸ H)) g) ↑z = 1 ↑z
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅

Tactic:
· rintro (rfl | rfl) <;> simp

Goal state after: