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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ 1 = 1

pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ↑b ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ ↑b ≠ 0
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
⊢ b ≠ 0
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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ 1 ^ deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
]

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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ 1 ^ deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ f.natDegree| * |eval ((algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = |↑b ^ f.natDegree| * |eval ((algebraMap ℤ K) a * (1 / ↑b)) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ Submodule.span R[X] (Set.range v) = Submodule.span R[X] (Set.range v)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ ↑b ^ f.natDegree * |eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) ev =
    (algebraMap ℤ K) b ^ f.natDegree * eval ((algebraMap ℤ K) a * bi) (Polynomial.map (algebraMap ℤ K) f)
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
⊢ 1 ≤ |ev|
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : a = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
ha : ¬a = 0
⊢ C a * X ^ n = C a * X ^ n

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ natDegree 0 = natDegree 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) b ^ f.natDegree = 0 ∨
    eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
hF :
  (algebraMap ℤ K) b ^ f.natDegree = 0 ∨
    eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
⊢ eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) = 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.natDegree = p.natDegree

pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ ¬p = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ ¬p = 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ natTrailingDegree 0 = natTrailingDegree 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.natTrailingDegree = p.natTrailingDegree

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ p.natDegree < n

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ p.natDegree < n
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
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : p.natDegree < n
⊢ 0 = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
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
⊢ 0 = 0

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

Tactic:
]

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.natDegree + p.natTrailingDegree - n < p.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.DenomsClearable

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
f : ℤ[X]
a b : ℤ
b0 : 0 < b
fab : eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0
ev : ℤ
bi : K
bu : bi * (algebraMap ℤ K) b = 1
Fa : |↑ev| = ↑b ^ f.natDegree * |eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f)|
F0 : ev = 0
hF : eval ((algebraMap ℤ K) a * ((algebraMap ℤ K) b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
⊢ eval (↑a * (↑b)⁻¹) (Polynomial.map (algebraMap ℤ K) f) = 0
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
⊢ p.natTrailingDegree ≤ p.natTrailingDegree

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : p.natTrailingDegree ≤ n
⊢ p.coeff (p.natDegree - (n - p.natTrailingDegree)) = p.coeff (p.natDegree - (n - p.natTrailingDegree))

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = 0

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h2 : n ≤ p.natDegree
h3 : n < p.natTrailingDegree
⊢ p.mirror.coeff n = 0
Module: Mathlib.Algebra.Polynomial.Mirror

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

Tactic:
]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.mirror.coeff n ≠ 0
⊢ p.mirror.natTrailingDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n₁ : ℕ
x✝⁴ : n₁ ∈ Finset.range (p.natDegree + 1)
x✝³ : p.mirror.coeff n₁ ≠ 0
x✝² : ℕ
x✝¹ : x✝² ∈ Finset.range (p.natDegree + 1)
x✝ : p.mirror.coeff x✝² ≠ 0
h : (revAt (p.natDegree + p.natTrailingDegree)) n₁ = (revAt (p.natDegree + p.natTrailingDegree)) x✝²
⊢ x✝² = x✝²

Tactic:
]

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

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree

Tactic:
]

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ (revAt (p.natDegree + p.natTrailingDegree)) n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree

Tactic:
]

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natDegree + p.natTrailingDegree - n ≤ p.natDegree
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n

Tactic:
]

Goal state after:
case h.refine_1
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≤ p.natDegree
hp : p.coeff n ≠ 0
⊢ p.natTrailingDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.coeff n ≠ 0

Tactic:
]

Goal state after:
case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.coeff n ≠ 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.coeff n = p.coeff n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p.mirror = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natDegree = p.coeff p.natDegree

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.leadingCoeff = p.mirror.leadingCoeff

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 =
    p.sum fun x x_1 ↦ x_1 ^ 2

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 =
    p.sum fun x x_1 ↦ x_1 ^ 2
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 ^ 2 = p.coeff n ^ 2

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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.natDegree + p.natDegree = p.natDegree + p.natDegree

Tactic:
]

Goal state after:
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.natTrailingDegree + p.natTrailingDegree = p.natTrailingDegree + p.natTrailingDegree

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree))

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ C a * p.mirror = C a * p.mirror

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ -p.reverse * X ^ p.natTrailingDegree = -p.reverse * X ^ p.natTrailingDegree

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
⊢ g * h.mirror * (g.mirror * h) = k * (g.mirror * h)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ g * h
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → ((ofFn n) v).coeff N = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ∀ (N : ℕ), n - 1 < N → ((ofFn n) v).coeff N = 0