mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ ¬IsAlgebraic A y⁻¹

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ ¬IsAlgebraic A y⁻¹
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ v y < 1

Tactic:
]

Goal state after:
case inr
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : y ≠ 0
hy : v y ≠ 1
this : ∀ (y : K), y ≠ 0 → v y ≠ 1 → 1 < v y → Transcendental A y
hlt : v y ≤ 1
⊢ v y < 1
Module: Mathlib.RingTheory.Valuation.IsTrivialOn

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ v ((aeval y) p) = 0

pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ p ≠ 0

Tactic:
]

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ v ((aeval y) p) = 0

Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝² : CommRing A
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra A K
v : Valuation K Γ
hv : IsTrivialOn A v
y : K
h0 : ¬y = 0
hy : ¬v y = 1
hlt : 1 < v y
this : IsAlgebraic A y
p : A[X]
hpnt : p ≠ 0
hp : (aeval ((algebraMap K K) y)) p = 0
⊢ p ≠ 0
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
u : ↥R[x]
hu : u ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
u : ↥R[x]
hu : u ∈ Ideal.map (algebraMap R ↥R[x]) I
⊢ u ∈ Ideal.map (algebraMap R ↥R[x]) I
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : 1 ∈ comap (algebraMap R S) (conductor R x) ⊔ I
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : 1 ∈ comap (algebraMap R S) (conductor R x) ⊔ I
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
hx : 1 ∈ Ideal.map (algebraMap R S) (comap (algebraMap R S) (conductor R x)) ⊔ Ideal.map (algebraMap R S) I
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
hx : 1 ∈ Ideal.map (algebraMap R S) (comap (algebraMap R S) (conductor R x)) ⊔ Ideal.map (algebraMap R S) I
⊢ 1 ∈ conductor R x ⊔ Ideal.map (algebraMap R S) I
Module: Mathlib.RingTheory.Conductor

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : ∃ x_1 ∈ conductor R x, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) x_1 = y
⊢ ∃ a, ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) a = y

pp: case refine_2.hf
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : y ∈ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (conductor R x)
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : ∃ x_1 ∈ conductor R x, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) x_1 = y
⊢ ∃ a, ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) a = y

case refine_2.hf
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)
f : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I →+* S ⧸ Ideal.map (algebraMap R S) I :=
  Ideal.Quotient.lift (Ideal.map (algebraMap R ↥R[x]) I)
    ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)).comp (algebraMap (↥R[x]) S)) ⋯
y : S ⧸ Ideal.map (algebraMap R S) I
z : S
hz : (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) z = y
this : y ∈ Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) (conductor R x)
⊢ Function.Surjective ⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
r : K
x : K⟮X⟯
⊢ C r * x = C r * x

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (⇑(algebraMap K[X] K⟮X⟯) ∘ ⇑Polynomial.C)

Tactic:
]

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Function.Injective (⇑(algebraMap K[X] K⟮X⟯) ∘ ⇑Polynomial.C)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ ((∃ x, Polynomial.C x = f.num) ∧ ∃ x, Polynomial.C x = f.denom) → ∃ c, f = C c

Tactic:
]

Goal state after:
K : Type u
inst✝ : Field K
f : K⟮X⟯
⊢ ((∃ x, Polynomial.C x = f.num) ∧ ∃ x, Polynomial.C x = f.denom) → ∃ c, f = C c
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
f : K⟮X⟯
a : K
ha : Polynomial.C a = f.num
b : K
hb : Polynomial.C b = f.denom
⊢ C a / C b = C a / C b

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x : K⟮X⟯
h : Polynomial.eval₂ f a x.denom = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom

Tactic:
]

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x + y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x + y).num / Polynomial.eval₂ f a (x + y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom +
      Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom +
        Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) *
      Polynomial.eval₂ f a (x + y).denom

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x + y).denom = 0
⊢ Polynomial.eval₂ f a (x + y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    (Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.denom +
        Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.num) *
      Polynomial.eval₂ f a (x + y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)

Tactic:
]

Goal state after:
case pos
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : Polynomial.eval₂ f a (x * y).denom = 0
this : Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom = 0
⊢ Polynomial.eval₂ f a (x * y).num / Polynomial.eval₂ f a (x * y).denom =
    Polynomial.eval₂ f a x.num / Polynomial.eval₂ f a x.denom *
      (Polynomial.eval₂ f a y.num / Polynomial.eval₂ f a y.denom)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * (Polynomial.eval₂ f a x.denom * Polynomial.eval₂ f a y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * Polynomial.eval₂ f a (x.denom * y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a (x * y).num * Polynomial.eval₂ f a (x.denom * y.denom) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a x.num * Polynomial.eval₂ f a y.num * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) =
    Polynomial.eval₂ f a (x.num * y.num) * Polynomial.eval₂ f a (x * y).denom
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)

Tactic:
]

Goal state after:
case neg
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
x y : K⟮X⟯
hx : Polynomial.eval₂ f a x.denom ≠ 0
hy : Polynomial.eval₂ f a y.denom ≠ 0
hxy : ¬Polynomial.eval₂ f a (x * y).denom = 0
⊢ Polynomial.eval₂ f a ((x * y).num * (x.denom * y.denom)) = Polynomial.eval₂ f a (x.num * y.num * (x * y).denom)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Transcendental K Polynomial.X

Tactic:
]

Goal state after:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ Transcendental K Polynomial.X
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ Prime X

pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0

Tactic:
]

Goal state after:
K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ Prime X

K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ ¬X = 0

Tactic:
]

Goal state after:
K✝ : Type u
K : Type u_1
inst✝ : Field K
⊢ ¬X = 0
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝ : Field K
⊢ exp (-1) = exp (-1)

Tactic:
]

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p✝ : K[X]
hp : p✝ ≠ 0
p : K[X]
⊢ ↑((aeval X) p) = (aeval ((algebraMap K[X] K⟮X⟯) X)) p

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hlt : 1 < v RatFunc.X
p✝ : K[X]
hp : p✝ ≠ 0
p : K[X]
⊢ ↑((aeval X) p) = (aeval ((algebraMap K[X] K⟮X⟯) X)) p
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: case insert
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : ι → S[X]
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) → ∀ (j : ℕ), IsIntegral R ((s.prod p).coeff j)
H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R (∑ x ∈ Finset.antidiagonal j, (p a).coeff x.1 * (∏ x ∈ s, p x).coeff x.2)

Tactic:
]

Goal state after:
case insert
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : ι → S[X]
a : ι
s : Finset ι
has : a ∉ s
IH : (∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) → ∀ (j : ℕ), IsIntegral R ((s.prod p).coeff j)
H : ∀ i ∈ insert a s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)
j : ℕ
⊢ IsIntegral R (∑ x ∈ Finset.antidiagonal j, (p a).coeff x.1 * (∏ x ∈ s, p x).coeff x.2)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
⊢ v (∑ x ∈ Finset.range (p.natDegree + 1), (algebraMap K[X] K⟮X⟯) ((monomial x) (p.coeff x))) ≤ 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
⊢ v (∑ x ∈ Finset.range (p.natDegree + 1), (algebraMap K[X] K⟮X⟯) ((monomial x) (p.coeff x))) ≤ 1
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R (p.coeff i)

Tactic:
hm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R ((C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod).coeff i)
Module: Mathlib.FieldTheory.RatFunc.AsPolynomial

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ↑((monomial i) (p.coeff i)) ≤ 1

Tactic:
]

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hv : IsTrivialOn K v
hle : v RatFunc.X ≤ 1
p : K[X]
i : ℕ
h0 : ¬p.coeff i = 0
⊢ i ∈ Finset.range (p.natDegree + 1) → v ↑((monomial i) (p.coeff i)) ≤ 1
Module: Mathlib.RingTheory.Polynomial.IsIntegral

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R (p.leadingCoeff * (∏ x, x.fst).coeff i)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hpmon : IsIntegral R p.leadingCoeff
hp : p.Splits
hpr : ∀ (x : S), p.IsRoot x → IsIntegral R x
i : ℕ
m : Multiset S
hm : p = C p.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
⊢ IsIntegral R (p.leadingCoeff * (∏ x, x.fst).coeff i)