mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
haV : a ∈ ↑V
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x

Tactic:
obtain ⟨f, g, e, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 _ ⟨haU, haV⟩

Goal state after:
X : Scheme
U V : (directedCover X).I₀
x : ↥(pullback ((directedCover X).f U) ((directedCover X).f V))
a : ↥X := (pullback.fst ((directedCover X).f U) ((directedCover X).f V) ≫ (↑U).ι) x
haU : a ∈ ↑U
haV : a ∈ ↑V
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
e : X.basicOpen f = X.basicOpen g
hxf : a ∈ X.basicOpen f
⊢ ∃ k hki hkj y, (pullback.lift (X.homOfLE ⋯) (X.homOfLE ⋯) ⋯) y = x
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ (q * p') = φ p' * φ q

pp: case inr.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

pp: case inr.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0

Tactic:
map_mul,

Goal state after:
case inr
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q * φ p' = φ p' * φ q

case inr.hb
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q ≠ 0

case inr.hd
K : Type u
inst✝⁵ : CommRing K
G₀ : Type u_1
L : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : Field L
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : FunLike F R[X] S[X]
φ : R[X] →*₀ G₀
hφ : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
f : R⟮X⟯
p q p' q' : R[X]
hq : q ∈ R[X]⁰
hq' : q' ∈ R[X]⁰
h : q' * p = q * p'
h✝ : Nontrivial R
⊢ φ q' ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) /
      (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)) =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
map_mul,

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) * (algebraMap K[X] K⟮X⟯) (p / gcd p q) /
      (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)) =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) * (algebraMap K[X] K⟮X⟯) (p / gcd p q) /
      (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)) =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q

Tactic:
map_mul,

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
q_div_ne_zero : q / gcd p q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) * (algebraMap K[X] K⟮X⟯) (p / gcd p q) /
      ((algebraMap K[X] K⟮X⟯) (C (q / gcd p q).leadingCoeff⁻¹) * (algebraMap K[X] K⟮X⟯) (q / gcd p q)) =
    (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) (x.num * q) = (algebraMap K[X] K⟮X⟯) (p * x.denom) ↔
    (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) (p * x.denom) ↔
    (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) (p * x.denom) ↔
    (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x : K⟮X⟯
p q : K[X]
hq : q ≠ 0
⊢ (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p * (algebraMap K[X] K⟮X⟯) x.denom ↔
    (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q = (algebraMap K[X] K⟮X⟯) p
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

pp: case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

pp: case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    ((algebraMap K[X] K⟮X⟯) (x.num * y.denom) + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

pp: case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

pp: case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom) =
    ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

case hb
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) x.denom ≠ 0

case hd
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ (algebraMap K[X] K⟮X⟯) y.denom ≠ 0
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom * y

Tactic:
← num_div_denom y,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
| (algebraMap K[X] K⟮X⟯) x.num / (algebraMap K[X] K⟮X⟯) x.denom *
    ((algebraMap K[X] K⟮X⟯) y.num / (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) (x.num * q) / (algebraMap K[X] K⟮X⟯) (x.denom * q)

Tactic:
map_mul,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q / (algebraMap K[X] K⟮X⟯) (x.denom * q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧ x = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q / (algebraMap K[X] K⟮X⟯) (x.denom * q)

Tactic:
map_mul,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
q : K[X]
hp : x.num * q ≠ 0
_hx : x.num ≠ 0
hq : q ≠ 0
⊢ x.denom * q ≠ 0 ∧
    x =
      (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) q /
        ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) q)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x = (algebraMap K[X] K⟮X⟯) (x.num * p) / (algebraMap K[X] K⟮X⟯) (x.denom * p)

Tactic:
map_mul,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) (x.denom * p)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) (x.denom * p)

Tactic:
map_mul,

Goal state after:
case h
K : Type u
inst✝ : Field K
x : K⟮X⟯
p : K[X]
hq : x.denom * p ≠ 0
_hx : x.denom ≠ 0
hp : p ≠ 0
⊢ x =
    (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) p /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) p)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = (algebraMap K[X] K⟮X⟯) (x.num * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
map_mul,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
map_mul,

Goal state after:
case neg
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ x * y =
    (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x * y = (algebraMap K[X] K⟮X⟯) (x.num * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x * y = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x * y = (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x * y =
    (algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.num /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y = (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) / (algebraMap K[X] K⟮X⟯) (x.denom * y.denom)

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    (algebraMap K[X] K⟮X⟯) (x.num * y.denom + x.denom * y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    ((algebraMap K[X] K⟮X⟯) (x.num * y.denom) + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom + (algebraMap K[X] K⟮X⟯) (x.denom * y.num)) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)

Tactic:
map_mul,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
⊢ x + y =
    ((algebraMap K[X] K⟮X⟯) x.num * (algebraMap K[X] K⟮X⟯) y.denom +
        (algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.num) /
      ((algebraMap K[X] K⟮X⟯) x.denom * (algebraMap K[X] K⟮X⟯) y.denom)
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
H'' : IsIntegral R[X] (derivative f * y %ₘ f)
⊢ φ (derivative f) * φ y = φ (derivative f * y) - φ (f * (derivative f * y /ₘ f))

Tactic:
map_mul,

Goal state after:
case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
H'' : IsIntegral R[X] (derivative f * y %ₘ f)
⊢ φ (derivative f) * φ y = φ (derivative f) * φ y - φ (f * (derivative f * y /ₘ f))
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
H'' : IsIntegral R[X] (derivative f * y %ₘ f)
⊢ φ (derivative f) * φ y = φ (derivative f) * φ y - φ (f * (derivative f * y /ₘ f))

Tactic:
map_mul,

Goal state after:
case inr
R : Type u_1
S : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing B
inst✝ : Algebra R B
φ : S[X] →ₐ[R] B
hφ : Function.Surjective ⇑φ
f : S[X]
hf : f.Monic
hf' : ∀ (i : ℕ), IsIntegral R (f.coeff i)
hfx : RingHom.ker φ.toRingHom = Ideal.span {f}
h✝ : Nontrivial B
hfd : f.natDegree ≠ 0
algInst✝¹ : Algebra S B := (φ.comp C).toAlgebra
this : Nontrivial S
y : S[X]
hy : IsIntegral R (φ y)
S' : Type u_2
w✝⁴ : CommRing S'
w✝³ : Algebra S S'
w✝² : Module.Finite S S'
w✝¹ : Module.Free S S'
w✝ : Nontrivial S'
hS' : (Polynomial.map (algebraMap S S') f).Splits
m : Multiset S'
hm : Polynomial.map (algebraMap S S') f = (Multiset.map (fun x ↦ X - C x) m).prod
algInst✝ : Algebra R S' := ((algebraMap S S').comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
hm' : ∀ a ∈ m, IsIntegral R a
hmc : m.card = f.natDegree
H :
  Polynomial.map (algebraMap S S') (derivative f * y %ₘ f) =
    (Multiset.map (fun x ↦ (Multiset.map (fun x ↦ X - C x) (m.erase x)).prod * C ((aeval x) y)) m).sum
H' : ∀ a ∈ m, IsIntegral R ((aeval a) y)
H'' : IsIntegral R[X] (derivative f * y %ₘ f)
⊢ φ (derivative f) * φ y = φ (derivative f) * φ y - φ f * φ (derivative f * y /ₘ f)
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
p : R[X]
hRS : integralClosure R S = ⊥
hφ : φ.Finite
hp : φ p * t ∈ conductor R (φ X)
algInst✝ : Algebra R[X] S := φ.toAlgebra
algebraizeInst✝ : Module.Finite R[X] S
this✝ : IsScalarTower R R[X] S
x : S
this : φ p * t * x ∈ φ.range
q : R[X]
n : ℕ
hn : IsIntegral R (p.leadingCoeff ^ n • (t * x) - φ q)
r : R
hr : (algebraMap R S) r = p.leadingCoeff ^ n • (t * x) - φ q
⊢ ∃ n, p.leadingCoeff ^ n • (t * x) ∈ φ.range

Tactic:
exact ⟨n, (C r + q), by simp [← Polynomial.algebraMap_eq, -Polynomial.algebraMap_apply, hr]⟩

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr.h.zero.inr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : R[X] →ₐ[R] S
t : S
hRS : integralClosure R S = ⊥
hφ : φ.Finite
i : ℕ
this : ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.leadingCoeff • t ∈ (conductor R (φ X)).radical
p : R[X]
hp : φ p * t ∈ (conductor R (φ X)).radical
IH :
  ∀ m < 0,
    ∀ (p : R[X]), φ p * t ∈ (conductor R (φ X)).radical → p.natDegree = m → p.coeff i • t ∈ (conductor R (φ X)).radical
hpn : p.natDegree = 0
hi' : i ≤ p.natDegree
⊢ p.coeff i • t ∈ (conductor R (φ X)).radical

Tactic:
simpa [← coeff_natDegree, hpn, show i = 0 by lia] using this _ hp

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : WeaklyQuasiFiniteAt R p
f : MvPolynomial (Fin 0) R →ₐ[R] S
hf : f.Finite
⊢ algebraMap R S = f.comp MvPolynomial.C

Tactic:
exact f.comp_algebraMap.symm

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ (C r).resultant g m n = (-1) ^ (m * n) * g.coeff n ^ m * r ^ n

Tactic:
rw [← zero_add m, resultant_add_left_deg _ _ _ _ _ (by simp), mul_comm n m]

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : R[X]
m n : ℕ
r : R
⊢ (-1) ^ (m * n) * g.coeff n ^ m * (C r).resultant g 0 n = (-1) ^ ((0 + m) * n) * g.coeff n ^ (0 + m) * r ^ n
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L) ((f %ₘ g).leadingCoeff⁻¹ ^ g.natDegree * g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

Tactic:
map_mul,

Goal state after:
case neg
n : ℕ
IH :
  ∀ m < n,
    ∀ {K : Type u_3} [inst : Field K] (f g : K[X]),
      f.Monic →
        g.Monic →
          f.Splits →
            g.Splits →
              g.natDegree ≤ f.natDegree →
                f.natDegree + g.natDegree = m →
                  f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
K : Type u_3
inst✝ : Field K
f g : K[X]
hf : f.Monic
hg : g.Monic
hf' : f.Splits
hg' : g.Splits
hfg : g.natDegree ≤ f.natDegree
hN : f.natDegree + g.natDegree = n
hr✝ : ¬g ∣ f
r : K[X] := C (f %ₘ g).leadingCoeff⁻¹ * (f %ₘ g)
hr₀ : f %ₘ g ≠ 0
hrd : r.natDegree < g.natDegree
hr : r.Monic
L : Type u_3 := r.SplittingField
this :
  (algebraMap K L) ((f %ₘ g).leadingCoeff⁻¹ ^ g.natDegree) *
      (algebraMap K L) (g.resultant (f %ₘ g) g.natDegree r.natDegree) =
    (Multiset.map (fun ij ↦ ij.1 - ij.2) ((map (algebraMap K L) g).roots ×ˢ (map (algebraMap K L) r).roots)).prod
⊢ f.resultant g = (Multiset.map (fun ij ↦ ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod