mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

pp: case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : ¬g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Tactic:
<;>

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

case neg
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝⁴ : AddCommMonoid Γ
inst✝³ : PartialOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
h : ¬g = 0
⊢ ((C a).map f).coeff g = (C (f a)).coeff g
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case inl
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ (n + 1)).order = (n + 1) • order 0

pp: case inr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).order = (n + 1) • x.order

Tactic:
<;>

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
n : ℕ
⊢ (0 ^ (n + 1)).order = (n + 1) • order 0

case inr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
x : R⟦Γ⟧
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).order = (n + 1) • x.order
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: K : Type u
inst✝ : Field K
A : ValuationSubring K
a b : (PrimeSpectrum ↥A)ᵒᵈ
h : a ≤ b
⊢ (OrderDual.ofDual.trans A.primeSpectrumEquiv) a ≤ (OrderDual.ofDual.trans A.primeSpectrumEquiv) b

Tactic:
apply ofPrime_le_of_le; exact h

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : A = B
⊢ A = B

pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : B = ⊤
⊢ A = B

Tactic:
<;>

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : A = B
⊢ A = B

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hTop : B ≠ ⊤
h : B = ⊤
⊢ A = B
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : A = B
⊢ B = ⊤

pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : B = ⊤
⊢ B = ⊤

Tactic:
<;>

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : A = B
⊢ B = ⊤

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hle : A ≤ B
hne : A ≠ B
h : B = ⊤
⊢ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : A = B
⊢ B = ⊤

pp: case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : B = ⊤
⊢ B = ⊤

Tactic:
<;>

Goal state after:
case inl
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : A = B
⊢ B = ⊤

case inr
K : Type u
inst✝¹ : Field K
A : ValuationSubring K
inst✝ : Ring.KrullDimLE 1 ↥A
B : ValuationSubring K
hlt : A < B
h : B = ⊤
⊢ B = ⊤
Module: Mathlib.RingTheory.Valuation.ValuationSubring

Goal state before:
pp: case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) = 1

Tactic:
← π.map_one,

Goal state after:
case convert_3
K : Type u
inst✝ : Field K
A : ValuationSubring K
x : ↥A.unitGroup
π : ↥A →+* ↥A ⧸ IsLocalRing.maximalIdeal ↥A := Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥A)
⊢ ↑x ∈ A.principalUnitGroup ↔ π ↑(A.unitGroupMulEquiv x) = π 1
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ∈ Set.Ici 0

pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(y - x) ∈ Set.Ici 0

pp: K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ≤ ↑(y - x)

Tactic:
<;>

Goal state after:
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ∈ Set.Ici 0

K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(y - x) ∈ Set.Ici 0

K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
hy : 0 < mk ↑(y - x)
z : FiniteElement K
hxz : x ≤ z
hzy : z ≤ y
this : x ≤ y
⊢ ↑(z - x) ≤ ↑(y - x)
Module: Mathlib.Algebra.Order.WithTop.Untop0

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
a : WithTop α
ha : a ≠ ⊤
⊢ ↑a.untop₀ = a

Tactic:
obtain ⟨b, hb⟩ := WithTop.ne_top_iff_exists.1 ha

Goal state after:
α : Type u_1
inst✝ : Zero α
a : WithTop α
ha : a ≠ ⊤
b : α
hb : ↑b = a
⊢ ↑a.untop₀ = a
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 ?hc) = 0

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 0

Tactic:
<;>

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 0 ?hc) = 0

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 0
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 ?hc) = 1

pp: case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 1

Tactic:
<;>

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ (Classical.ofNonempty.comp FiniteResidueField.mk) (FiniteElement.mk 1 ?hc) = 1

case hc
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
⊢ 0 ≤ mk 1
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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc : c • x = b
hac : -c • x < a
⊢ f.eval (-c • x) < ↑↑f ⟨a, ha⟩

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -c • x < a
hc : c = 0
⊢ f.eval (-c • x) < ↑↑f ⟨a, ha⟩

case neg
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
hx' : ∀ {c : K}, c ≠ 0 → -c • x ∉ (↑f).domain
y z : ↥(f.extendFun hx).domain
hyzmem : ↑(z - y) ∈ (↑f).domain ⊔ K ∙ x
a : M
ha : a ∈ (↑f).domain
b : M
hb : b ∈ K ∙ x
hab : a + b = ↑(z - y)
hyz : 0 < ⟨a + b, ⋯⟩
this : z - y = ⟨a + b, ⋯⟩
c : K
habpos : 0 < a + c • x
hc✝ : c • x = b
hac : -c • x < a
hc : ¬c = 0
⊢ f.eval (-c • x) < ↑↑f ⟨a, ha⟩
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case hx
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ 0 ≤ mk (-x)

pp: case h
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ -r < stdPart (-x)

Tactic:
<;>

Goal state after:
case hx
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ 0 ≤ mk (-x)

case h
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : 0 ≤ mk x
h : stdPart x < r
⊢ -r < stdPart (-x)
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r - 1 < r

pp: K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r + 1 > r

Tactic:
<;>

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r - 1 < r

K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, f s ≤ x
hr : ∀ s > r, x ≤ f s
⊢ r + 1 > 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}
⊢ ∀ s < sInf {r | x < f r}, f s ≤ x

pp: case inl.hr
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}
⊢ ∀ s > sInf {r | x < f r}, x ≤ f s

Tactic:
<;>

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}
⊢ ∀ s < sInf {r | x < f r}, f s ≤ x

case inl.hr
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}
⊢ ∀ s > sInf {r | x < f r}, x ≤ f s
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 : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : x < 0
⊢ {r | x < f r} = Set.univ

Tactic:
Set.eq_univ_iff_forall

Goal state after:
K : Type u_1
inst✝² : LinearOrder K
inst✝¹ : Field K
inst✝ : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : mk x < 0
hr : ∀ {r : ℝ}, mk x < mk (f r)
h : x < 0
⊢ ∀ (x_1 : ℝ), x_1 ∈ {r | x < f r}
Module: Mathlib.Algebra.Polynomial.CoeffList

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : ¬P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
P : R[X]
h : ¬P = 0
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
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 : P.natDegree + 1 ≤ k + 1
⊢ none =
    (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))[k + 1]?

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 : P.natDegree + 1 ≤ k + 1
⊢ (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ k + 1

Tactic:
<;>

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 : P.natDegree + 1 ≤ k + 1
⊢ none =
    (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))[k + 1]?

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 : P.natDegree + 1 ≤ k + 1
⊢ (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ k + 1
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 : P.natDegree + 1 ≤ k + 1
⊢ n + P.eraseLead.degree.succ ≤ k

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 : P.natDegree + 1 ≤ k + 1
⊢ P.degree.succ ≤ k + 1

Tactic:
<;>

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 : P.natDegree + 1 ≤ k + 1
⊢ n + P.eraseLead.degree.succ ≤ k

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 : P.natDegree + 1 ≤ k + 1
⊢ P.degree.succ ≤ k + 1
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
x x✝¹ x✝ : R
⊢ (((evalEvalRingHom x x✝¹).comp C).comp C) x✝ = (((eval₂RingHom (evalRingHom x) x✝¹).comp C).comp C) x✝

pp: case h₂
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ ((evalEvalRingHom x x✝).comp C) X = ((eval₂RingHom (evalRingHom x) x✝).comp C) X

pp: case h₂
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ (evalEvalRingHom x x✝) Y = (eval₂RingHom (evalRingHom x) x✝) Y

Tactic:
<;>

Goal state after:
case h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
x x✝¹ x✝ : R
⊢ (((evalEvalRingHom x x✝¹).comp C).comp C) x✝ = (((eval₂RingHom (evalRingHom x) x✝¹).comp C).comp C) x✝

case h₂
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ ((evalEvalRingHom x x✝).comp C) X = ((eval₂RingHom (evalRingHom x) x✝).comp C) X

case h₂
R : Type u_1
inst✝ : CommSemiring R
x x✝ : R
⊢ (evalEvalRingHom x x✝) Y = (eval₂RingHom (evalRingHom x) x✝) Y
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x y : R
p : R[X][Y]
⊢ eval y (map (evalRingHom x) p) = evalEval x y p

Tactic:
by
  rw [eval_map, eval₂_evalRingHom]

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

Goal state before:
pp: case h₁.h₁
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
x✝ : R
⊢ (((eval₂RingHom (eval₂RingHom f x) y).comp C).comp C) x✝ =
    ((((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))).comp C).comp C) x✝

pp: case h₂
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ ((eval₂RingHom (eval₂RingHom f x) y).comp C) X = (((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))).comp C) X

pp: case h₂
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ (eval₂RingHom (eval₂RingHom f x) y) Y = ((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))) Y

Tactic:
<;>

Goal state after:
case h₁.h₁
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
x✝ : R
⊢ (((eval₂RingHom (eval₂RingHom f x) y).comp C).comp C) x✝ =
    ((((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))).comp C).comp C) x✝

case h₂
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ ((eval₂RingHom (eval₂RingHom f x) y).comp C) X = (((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))).comp C) X

case h₂
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ (eval₂RingHom (eval₂RingHom f x) y) Y = ((evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))) Y
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
x✝ : R
n✝¹ n✝ : ℕ
⊢ ((((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))).comp C).comp C) x✝).coeff
          n✝¹).coeff
      n✝ =
    (((((RingHom.id R[X][Y]).comp C).comp C) x✝).coeff n✝¹).coeff n✝

pp: case h₂
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ (((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))).comp C) X).coeff n✝¹).coeff
      n✝ =
    ((((RingHom.id R[X][Y]).comp C) X).coeff n✝¹).coeff n✝

pp: case h₂
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ ((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))) Y).coeff n✝¹).coeff n✝ =
    (((RingHom.id R[X][Y]) Y).coeff n✝¹).coeff n✝

Tactic:
<;>

Goal state after:
case h₁.h₁
R : Type u_1
inst✝ : CommSemiring R
x✝ : R
n✝¹ n✝ : ℕ
⊢ ((((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))).comp C).comp C) x✝).coeff
          n✝¹).coeff
      n✝ =
    (((((RingHom.id R[X][Y]).comp C).comp C) x✝).coeff n✝¹).coeff n✝

case h₂
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ (((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))).comp C) X).coeff n✝¹).coeff
      n✝ =
    ((((RingHom.id R[X][Y]).comp C) X).coeff n✝¹).coeff n✝

case h₂
R : Type u_1
inst✝ : CommSemiring R
n✝¹ n✝ : ℕ
⊢ ((((evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y))) Y).coeff n✝¹).coeff n✝ =
    (((RingHom.id R[X][Y]) Y).coeff n✝¹).coeff n✝
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₁
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

pp: case h₂
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

Tactic:
<;>

Goal state after:
case h₁
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]

case h₂
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ (aevalAeval Y (C X)).comp (aevalAeval Y (C X)) = AlgHom.id R R[X][Y]
Module: Mathlib.Algebra.Polynomial.Bivariate

Goal state before:
pp: case h₁.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

pp: case h₁.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m

Tactic:
<;>

Goal state after:
case h₁.hC
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ (((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))).comp CAlgHom) X).coeff n).coeff m =
    ((((AlgHom.id R R[X][Y]).comp CAlgHom) X).coeff n).coeff m

case h₁.hX
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
n m : ℕ
⊢ ((((aevalAeval Y (C X)).comp (aevalAeval Y (C X))) Y).coeff n).coeff m = (((AlgHom.id R R[X][Y]) Y).coeff n).coeff m