mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 3
⊢ ∃ k m n,
    ∃ (_ : k < m) (_ : m < n),
      ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n

pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support = 3
⊢ ∃ k m n,
    ∃ (_ : k < m) (_ : m < n),
      ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False

pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ False

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : p = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ False

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z, ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0), f = C x * X ^ k + C y * X ^ m + C z * X ^ n) →
    #f.support = 3
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

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

Tactic:
·

Goal state after:
case inl
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
·

Goal state after:
case inr
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
Module: Mathlib.Algebra.Ring.GeomSum

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

Tactic:
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _

Goal state after:
case inr
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ 1 ≤ m

Tactic:
by lia

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

Tactic:
·

Goal state after:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → (if i = b then ↑(n.choose (b + 1)) else 0) = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0

Tactic:
·

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ∀ b ∈ range n, b ≠ i → (if i = b then ↑(n.choose (b + 1)) else 0) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ i ∉ range n → (if i = i then ↑(n.choose (i + 1)) else 0) = 0
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

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

Tactic:
·

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 ∈ range n, (P ^ b).degree < (P ^ n).degree
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
·

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
⊢ ⊥ < (P ^ n).degree
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
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ range n, P ^ i).Monic

Tactic:
by
  nontriviality R
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
  rw [geom_sum_succ']
  refine (hP.pow _).add_of_left ?_
  refine lt_of_le_of_lt (degree_sum_le _ _) ?_
  rw [Finset.sup_lt_iff]
  · simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
    simp only [Nat.cast_lt, hP.natDegree_pow]
    intro k
    exact nsmul_lt_nsmul_left hdeg
  · rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]
    exact (hP.pow _).ne_zero

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n

pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ ↑0 = p.coeff n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ ↑⟨p.coeff n, ⋯⟩ = p.coeff n
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inl.inl
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)
⊢ 1 * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inl.inr
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)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
·

Goal state after:
case inl.inl
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)
⊢ 1 * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inl.inr
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)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
·

Goal state after:
case inl.inr
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)
yj : C
hyj : yj ∈ ↑y
⊢ 1 * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Polynomial.Basic

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

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), f.coeff n ∈ I) → f ∈ map C I

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ f ∈ map C I → ∀ (n : ℕ), f.coeff n ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

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

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

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

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

Tactic:
·

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
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
·

Goal state after:
case inr.inl
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)
yi : C
hyi : yi ∈ ↑y
⊢ yi * 1 ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑∅)

pp: case refine_2
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ ∀ (a : A) (s : Finset A), a ∉ s → P (Algebra.adjoin R ↑s) → P (Algebra.adjoin R ↑(insert a s))

Tactic:
·

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : IsNoetherian R A
P : Subalgebra R A → Prop
base : P ⊥
ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))
t : Finset A
⊢ P (Algebra.adjoin R ↑∅)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

pp: case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
·

Goal state after:
case inr.inr
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)
yi : C
hyi : yi ∈ ↑y
yj : C
hyj : yj ∈ ↑y
⊢ yi * yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))
Module: Mathlib.RingTheory.Polynomial.Basic

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

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

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

Tactic:
·

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Basic

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

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

Tactic:
·

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Basic

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

Tactic:
·

Goal state after:
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.RingTheory.Polynomial.Basic

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

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
⊢ (∀ (n : ℕ), f.coeff n ∈ I) → f ∈ map C I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) → ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x) → ∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x
Module: Mathlib.RingTheory.Polynomial.Basic

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

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

Goal state after:
case mp.inl
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
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:
·

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x