mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : (↑f).toFun z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ ↑z ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : (↑f).toFun z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
⊢ ↑z ∈ (↑f).domain ⊔ K ∙ x
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
⊢ ↑b ∈ {r | x < f r}

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
⊢ x < ↑b
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
r : ℝ
hr : r ∈ {r | x < f r}
hra : r < ↑a
⊢ (↑↑f.toRingHom).toFun ↑a < (↑↑f.toRingHom).toFun r

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb : x < ↑b
hn : {r | x < f r}.Nonempty
r : ℝ
hr : r ∈ {r | x < f r}
hra : r < ↑a
⊢ ↑a < f r
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case inl.hl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
hr : r < sInf {r | x < f r}
⊢ f r ≤ x

Tactic:
simpa using

Goal state after:
case inl.hl
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : 0 ≤ mk x
a : ℤ
ha : ↑a < x
b : ℤ
hb✝ : x < ↑b
hn : {r | x < f r}.Nonempty
hb : BddBelow {r | x < f r}
r : ℝ
hr : r < sInf {r | x < f r}
⊢ f r ≤ x
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case pos.inl
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ ↑(ball K c) ⊆ ↑(ball K d)

Tactic:
simpa using

Goal state after:
case pos.inl
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K c
z : ↥(↑f).domain
hz : ↑↑f z = toLex ((truncLTLinearMap K c) (ofLex (↑↑f y)))
d : FiniteArchimedeanClass M
hdc : d < c
⊢ ball K c ≤ ball K d
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ x ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
h : ¬∃ y, ↑y - x ∈ ball K c
⊢ x ∈ (↑f).domain ⊔ K ∙ x
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ↑(ball K d) ⊆ ↑(ball K c)

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c d : FiniteArchimedeanClass M
hdc : c ≤ d
y : ↥(↑f).domain
hy : ↑y - x ∈ ball K d
⊢ ball K d ≤ ball K c
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
h₃ : ¬P.eraseLead = 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
h₃ : ¬P.eraseLead = 0
⊢ ∀ a < P.natDegree, P.eraseLead.coeff a = P.coeff a
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
this : ((monomial n) x).natDegree.succ = n + 1
⊢ ((monomial n) x).coeffList.get ⟨k + 1, h₁✝¹⟩ = (x :: List.replicate n 0).get ⟨k + 1, h₁✝⟩

Tactic:
simpa using

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬(monomial n) x = 0
k : ℕ
h₁✝¹ : k + 1 < ((monomial n) x).coeffList.length
h₁✝ : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
this : ((monomial n) x).natDegree.succ = n + 1
⊢ ((monomial n) x).coeff (((monomial n) x).natDegree - (k + 1)) = 0
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ (monomial P.natDegree) P.leadingCoeff = P

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ (monomial P.natDegree) P.leadingCoeff = P
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ k + 1 < (List.map P.coeff (List.range P.degree.succ)).length

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ k < P.natDegree
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : k < n
⊢ some (P.eraseLead.coeff dk) =
    (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse)[k]?

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : k < n
⊢ P.eraseLead.coeff dk = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ a' ∈ ((↑f).supSpanSingleton x (f.eval x) hx).domain

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
seed : Seed K M R
f : Partial seed
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
x : M
hx : x ∉ (↑f).domain
c : FiniteArchimedeanClass M
y' : M
hy'✝ : y' ∈ (f.extendFun hx).domain
hy' : y' ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = y'
k : K
hk : k • x = b
a' : M
ha'mem : a' ∈ (↑f).domain
ha' : (↑f).toFun ⟨a', ha'mem⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑↑f ⟨a, ha⟩)))
⊢ a' ∈ (↑f).domain ⊔ K ∙ x
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
simpa using

Goal state after:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
by_cases hr' : r = 0

Goal state after:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ swap (C f) = map C f

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ (aeval Y) f = map (algebraMap R R[X]) f
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Subsingleton R
⊢ (p + q).IsMonicOfDegree n

Tactic:
simpa using

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
hq : q.natDegree < n
H : Subsingleton R
⊢ n = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem'✝ : f' ∈ c✝
hf' : ↑f' = f
x' : ↥f.domain
hx' : ↑f x' = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
hmem' : ↑x' ∈ (sSupFun hc).domain
hleft : ↑(sSupFun hc) ⟨↑x', hmem'⟩ = ↑f x'
hright : ↑(sSupFun hc) x = ↑f ⟨↑x, hf⟩
⊢ ↑(sSupFun hc) ⟨↑x', hmem'⟩ = toLex ((truncLTLinearMap K c) (ofLex (↑(sSupFun hc) x)))

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹¹ : DivisionRing K
inst✝¹⁰ : LinearOrder K
inst✝⁹ : IsOrderedRing K
inst✝⁸ : Archimedean K
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : LinearOrder M
inst✝⁵ : IsOrderedAddMonoid M
inst✝⁴ : Module K M
inst✝³ : IsOrderedModule K M
R : Type u_3
inst✝² : AddCommGroup R
inst✝¹ : LinearOrder R
inst✝ : Module K R
seed : Seed K M R
c✝ : Set (Partial seed)
hnonempty : c✝.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c✝
x : ↥(sSupFun hc).domain
c : FiniteArchimedeanClass M
hx : ↑x ∈ sSup (LinearPMap.domain '' (fun x ↦ ↑x) '' c✝)
f : M →ₗ.[K] Lex R⟦FiniteArchimedeanClass M⟧
hmem : f ∈ (fun x ↦ ↑x) '' c✝
hf : ↑x ∈ f.domain
f' : Partial seed
hmem'✝ : f' ∈ c✝
hf' : ↑f' = f
x' : ↥f.domain
hx' : ↑f x' = toLex ((truncLTLinearMap K c) (ofLex (↑f ⟨↑x, hf⟩)))
hmem' : ↑x' ∈ (sSupFun hc).domain
hleft : ↑(sSupFun hc) ⟨↑x', hmem'⟩ = ↑f x'
hright : ↑(sSupFun hc) x = ↑f ⟨↑x, hf⟩
⊢ ↑f x' = toLex ((truncLT c) (ofLex (↑f ⟨↑x, hf⟩)))
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ ((monomial n) 1).IsMonicOfDegree n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).IsMonicOfDegree n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Subsingleton R
⊢ ((aeval (X + C r)) p).IsMonicOfDegree n

Tactic:
simpa using

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
n : ℕ
hp : p.IsMonicOfDegree n
r : R
H : Subsingleton R
⊢ n = 0
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h✝ : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h✝.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
a✝ b✝ : M
h : a✝ < b✝
⊢ (LinearMap.codRestrict ⊤ LinearMap.id ⋯) a✝ < (LinearMap.codRestrict ⊤ LinearMap.id ⋯) b✝

Tactic:
simpa using

Goal state after:
case refine_1
K : Type u_1
inst✝¹³ : DivisionRing K
inst✝¹² : LinearOrder K
inst✝¹¹ : IsOrderedRing K
inst✝¹⁰ : Archimedean K
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : LinearOrder M
inst✝⁷ : IsOrderedAddMonoid M
inst✝⁶ : Module K M
inst✝⁵ : IsOrderedModule K M
R : Type u_3
inst✝⁴ : AddCommGroup R
inst✝³ : LinearOrder R
inst✝² : Module K R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
h✝ : Nonempty (HahnEmbedding.Seed K M R)
f : ↥⊤ →ₗ[K] Lex R⟦FiniteArchimedeanClass M⟧
hpartial : HahnEmbedding.IsPartial h✝.some { domain := ⊤, toFun := f }
harch :
  ∀ (x : ↥(↑⟨{ domain := ⊤, toFun := f }, hpartial⟩).domain),
    (withTopOrderIso M) (ofLex (↑↑⟨{ domain := ⊤, toFun := f }, hpartial⟩ x)).orderTop = ArchimedeanClass.mk ↑x
a✝ b✝ : M
h : a✝ < b✝
⊢ a✝ < b✝
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ n + p.natTrailingDegree - n ≤ p.natTrailingDegree

Tactic:
add_tsub_cancel_left

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
h1 : n ≤ p.natDegree + p.natTrailingDegree
⊢ p.natTrailingDegree ≤ p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
⊢ p.coeff (n, (revAt (p.natDegree + p.natTrailingDegree)) n).1 *
      p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) (n, (revAt (p.natDegree + p.natTrailingDegree)) n).2) =
    p.coeff n ^ 2

Tactic:
revAt_invol,

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ
⊢ p.coeff (n, (revAt (p.natDegree + p.natTrailingDegree)) n).1 * p.coeff n = p.coeff n ^ 2
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
natDegree_mul hp (mt mirror_eq_zero.mp hp),

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ p.natDegree + p.mirror.natDegree = 2 * p.natDegree
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
c : R
n : ℕ
⊢ (C c).homogenize n = MvPolynomial.C c * MvPolynomial.X 1 ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
c : R
n : ℕ
⊢ (C c).homogenize n = (MvPolynomial.monomial fun₀ | 1 => n) c
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ homogenize 1 n = MvPolynomial.X 1 ^ n

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ homogenize 1 n = MvPolynomial.X 1 ^ n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ MvPolynomial.coeff m q ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ ¬MvPolynomial.coeff m q = 0
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)

Tactic:
simpa using

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_1.cast
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
i : Fin n
⊢ (Fin.snoc r (q %ₘ g) i.castSucc).degree < g.degree

Tactic:
simpa using

Goal state after:
case succ.refine_1.cast
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
i : Fin n
⊢ (r i).degree < g.degree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_1.last
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ (Fin.snoc r (q %ₘ g) (Fin.last n)).degree < g.degree

Tactic:
simpa using

Goal state after:
case succ.refine_1.last
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ (q %ₘ g).degree < g.degree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
q₁ q₂ : R[X]
r₁ r₂ : Fin 0 → R[X]
hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree
hf : q₁ * g ^ 0 + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ 0 + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
q₁ q₂ : R[X]
r₁ r₂ : Fin 0 → R[X]
hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree
hf : q₁ * g ^ 0 + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ 0 + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂