mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent

Goal state before:
pp: case refine_2
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine (Spec T)
ψ : R ⟶ T
hfst : IsIso (pullback.fst (Spec.map φ) (Spec.map ψ))
⊢ ∀ {R S : CommRingCat} {f : R ⟶ S}, isomorphisms Scheme (Spec.map f) ↔ Function.Bijective ⇑(CommRingCat.Hom.hom f)

Tactic:
· simp_rw [← isIso_SpecMap_iff, implies_true]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Descent

Goal state before:
pp: case inr
P P' : MorphismProperty Scheme
inst✝³ : P'.IsStableUnderBaseChange
inst✝² : P'.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst✝ : IsZariskiLocalAtTarget P
H :
  ∀ {R S : CommRingCat} {Y : Scheme} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (pullback.fst (Spec.map φ) g) → P g
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (pullback.fst f g)
this : ∀ {X : Scheme} (f : X ⟶ Spec R), (P' ⊓ @QuasiCompact) f → P (pullback.fst f g) → (∃ T, X = Spec T) → P g
hX : ¬∃ T, X = Spec T
⊢ P g

Tactic:
have _ : CompactSpace X := by simpa [← quasiCompact_iff_compactSpace f] using hf.2
    obtain ⟨Y, p, hsurj, hP', hY⟩ := X.exists_hom_isAffine_of_isZariskiLocalAtSource @IsLocalIso
    refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩
    · rw [Category.assoc, (P' ⊓ @QuasiCompact).cancel_left_of_respectsIso]
      exact ⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩
    · rw [← pullbackRightPullbackFstIso_inv_fst f g _, P.cancel_left_of_respectsIso]
      exact P.pullback_fst _ _ h

Goal state after:
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
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ ∃ x_1 ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I),
    (algebraMap (↥R[x]) S) x_1 = (algebraMap R S) a * ((algebraMap R S) p * l a)

Tactic:
refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_

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
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥R[x]) I) ∧
    (algebraMap (↥R[x]) S) ((algebraMap R ↥R[x]) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a ↦ a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ l a * (algebraMap R S) p ∈ R[x]
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this✝ : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (algebraMap R SQ) P = p
⊢ p = Ideal.under R (Ideal.under S P)

Tactic:
rw [Ideal.under_under, ← e]

Goal state after:
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]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
⊢ X ^ m - p ∣ (Algebra.ofId R[X] S[X]) (eval (X ^ m) q)

Tactic:
rw [← coe_aeval_eq_eval, ← aeval_algHom_apply, ← neg_dvd, neg_sub]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : S[X]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
⊢ p - X ^ m ∣ (aeval ((Algebra.ofId R[X] S[X]) (X ^ m))) q
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]
hp : IsIntegral R[X] p
i : ℕ
a✝¹ : Nontrivial R
a✝ : Nontrivial S
hp0 : p ≠ 0
q : R[X][X] := minpoly R[X] p
m : ℕ := (q.support.sup fun i ↦ (q.coeff i).natDegree) + p.natDegree + 1
hm₁ : ∀ (i : ℕ), (q.coeff i).natDegree < m
hm₁' : (eval (X ^ m) q).Monic
hm₂ : p.natDegree < m
h₀ : (algebraMap R[X] S[X]) X = X
this : (Polynomial.map (algebraMap R[X] S[X]) ((taylor (X ^ m)) q)).IsRoot (p - X ^ m)
⊢ p - X ^ m ∣ (aeval ((Algebra.ofId R[X] S[X]) (X ^ m))) q

Tactic:
simpa [Polynomial.taylor_coeff_zero, -algebraMap_def, h₀] using this.dvd_coeff_zero

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

Goal state before:
pp: case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩

Tactic:
obtain ⟨f₃, hf₃⟩ := U.2.basicOpen_basicOpen_is_basicOpen f₂ f₁

Goal state after:
case mp
X : Scheme
U : X.AffineZariskiSite
s : Set ↑Γ(X, U.toOpens)
f₂ : ↑Γ(X, U.toOpens)
hf₂s : f₂ ∈ s
hW : IsAffineOpen (X.basicOpen f₂)
f₁ : ↑Γ(X, toOpens ⟨X.basicOpen f₂, hW⟩)
hV : IsAffineOpen (X.basicOpen f₁)
f₃ : ↑Γ(X, ↑U)
hf₃ : X.basicOpen f₃ = X.basicOpen f₁
⊢ ∃ f ∈ s, ∃ g, X.basicOpen (f * g) = toOpens ⟨X.basicOpen f₁, hV⟩
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      { toFractionRing := Localization.mk (p, q).1 (p, q).2 + Localization.mk (p', q').1 (p', q').2 } =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p, q).1 (p, q).2 } +
      (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p', q').1 (p', q').2 }

Tactic:
Localization.add_mk

Goal state after:
case inr.H.H
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)
      { toFractionRing := Localization.mk (↑(p, q).2 * (p', q').1 + ↑(p', q').2 * (p, q).1) ((p, q).2 * (p', q').2) } =
    (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p, q).1 (p, q).2 } +
      (liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ) { toFractionRing := Localization.mk (p', q').1 (p', q').2 }
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case inr.H.H
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (↑q * p' + ↑q' * p) / φ ↑(q * q') = φ p / φ ↑q + φ p' / φ ↑q'

Tactic:
rw [div_add_div, div_eq_div_iff]

Goal state after:
case inr.H.H
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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ (↑q * p' + ↑q' * p) * (φ ↑q * φ ↑q') = (φ p * φ ↑q' + φ ↑q * φ p') * φ ↑(q * q')

case inr.H.H.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑(q * q') ≠ 0

case inr.H.H.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q * φ ↑q' ≠ 0

case inr.H.H.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q ≠ 0

case inr.H.H.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] →+* L
hφ : R[X]⁰ ≤ Submonoid.comap φ L⁰
h✝ : Nontrivial R
p : R[X]
q : ↥R[X]⁰
p' : R[X]
q' : ↥R[X]⁰
⊢ φ ↑q' ≠ 0
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : (aeval (x + ε')) P.f = 0
hε'' : IsUnit ((aeval (x + ε')) P.g)
⊢ ε' = (aeval x) P.f * -b

Tactic:
Polynomial.aeval_add_of_sq_eq_zero _ _ _ (hI.le (Ideal.pow_mem_pow hε'I 2))

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : StandardEtalePair R
I : Ideal S
hI : I ^ 2 = ⊥
x : S
hx : P.HasMap ((Ideal.Quotient.mk I) x)
hf : (aeval x) P.f ∈ I
a : S
ha : (aeval x) P.g * a - 1 ∈ I
p₁ p₂ : R[X]
n : ℕ
e : (aeval x) (derivative P.f) * (aeval x) p₁ + (aeval x) P.f * (aeval x) p₂ = (aeval x) P.g ^ n
ε : S
hεI : ε ∈ I
b : S
hb : (aeval x) (derivative P.f) * b = 1 + ε
this✝ : (aeval x) P.f ^ 2 = 0
this : (aeval x) P.f * ε = 0
ε' : S
hε'I : ε' ∈ I
hε' : (aeval x) P.f + (aeval x) (derivative P.f) * ε' = 0
hε'' : IsUnit ((aeval (x + ε')) P.g)
⊢ ε' = (aeval x) P.f * -b
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ P.Ring ≃ₐ[R] Localization.Away ((AdjoinRoot.mk P.f) P.g)

Tactic:
refine .ofAlgHom (P.lift (algebraMap (AdjoinRoot P.f) _ (.root P.f)) ⟨?_, ?_⟩)
    (IsLocalization.Away.liftAlgHom (AdjoinRoot.mk P.f P.g)
      (f := AdjoinRoot.liftAlgHom _ _ P.X P.hasMap_X.1) P.hasMap_X.2) ?_ ?_

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.f = 0

case refine_2
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ IsUnit
    ((aeval ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f))) P.g)

case refine_3
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯).comp
      (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯) =
    AlgHom.id R (Localization.Away ((AdjoinRoot.mk P.f) P.g))

case refine_4
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
P : StandardEtalePair R
⊢ (IsLocalization.Away.liftAlgHom ((AdjoinRoot.mk P.f) P.g) ⋯).comp
      (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) =
    AlgHom.id R P.Ring
Module: Mathlib.RingTheory.Smooth.IntegralClosure

Goal state before:
pp: 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
inst✝ : Module.Flat R S
⊢ Function.Injective ⇑(toIntegralClosure R S B)

Tactic:
refine Function.Injective.of_comp (f := (integralClosure _ _).val) ?_
  rw [← AlgHom.coe_comp, toIntegralClosure, AlgHom.val_comp_codRestrict]
  exact Module.Flat.lTensor_preserves_injective_linearMap (M := S)
    (integralClosure R B).val.toLinearMap Subtype.val_injective

Goal state after:
Module: Mathlib.RingTheory.Etale.StandardEtale

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : IsStandardEtale R S
inst✝ : Etale R T
f : S →ₐ[R] T
hf : Function.Surjective ⇑f
⊢ IsStandardEtale R T

Tactic:
let := f.toAlgebra
  have : IsScalarTower R S T := .of_algebraMap_eq' f.comp_algebraMap.symm
  obtain ⟨e, he, hfe⟩ :=
    (Ideal.isIdempotentElem_iff_of_fg _ (Algebra.FinitePresentation.ker_fG_of_surjective f hf)).mp
      ((Algebra.FormallyEtale.iff_of_surjective hf).mp (.of_restrictScalars (R := R)))
  have := IsLocalization.away_of_isIdempotentElem he.one_sub (hfe.trans (by simp)) hf
  exact .of_isLocalizationAway (1 - e)

Goal state after:
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]
ht : φ.IsIntegralElem t
hp : φ p * t ∈ φ.range
a : R := p.leadingCoeff
R' : Type u_1 := Localization.Away a
S' : Type u_2 := Localization.Away ((algebraMap R S) a)
this✝ : Algebra R' S' := (Localization.awayMap (algebraMap R S) a).toAlgebra
this : IsScalarTower R R' S'
ha : IsUnit ((algebraMap R R') a)
⊢ (aeval ((algebraMap S S') (φ X))).comp (mapRingHom (algebraMap R R')) = (algebraMap S S').comp ↑φ

Tactic:
ext <;>
      simp [-Polynomial.algebraMap_apply, ← Polynomial.algebraMap_eq, ← algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case inr
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ ⊤ ≤ Subalgebra.restrictScalars R (↥(integralClosure R S))[x]

Tactic:
refine hx.ge.trans ?_

Goal state after:
case inr
R S : Type u
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : WeaklyQuasiFiniteAt R p
x : S
hx : R[x] = ⊤
this :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
    [WeaklyQuasiFiniteAt R p] (x : S), R[x] = ⊤ → integralClosure R S = ⊥ → ZariskisMainProperty R p
H : ¬integralClosure R S = ⊥
inst✝ : Algebra (↥(integralClosure R S)) (Localization.AtPrime p) := OreLocalization.instAlgebra
inst : WeaklyQuasiFiniteAt (↥(integralClosure R S)) p
⊢ R[x] ≤ Subalgebra.restrictScalars R (↥(integralClosure R S))[x]
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := ⋯
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := ⋯
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ Spec.map (appLE f₀ (g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) h₁) ≫ ⋯.fromSpec =
    Spec.map (CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom) ≫
      (normalizationOpenCover f).f U ≫ f₂

Tactic:
simp only [AlgHom.toRingHom_eq_coe, hf₀, comp_appLE, Spec.map_comp, Category.assoc,
        app_eq_appLE]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst✝ : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U : (normalizationOpenCover f).I₀
this✝¹ : Algebra ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U) := (CommRingCat.Hom.hom (app f ↑U)).toAlgebra
this✝ : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ ↑U ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₁' : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂ : fromNormalization f ⁻¹ᵁ ↑U = f₁ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₂' : fromNormalization f ⁻¹ᵁ ↑U = f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U
h₃ : f ⁻¹ᵁ ↑U = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ ↑U
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) (f ⁻¹ᵁ ↑U) ⋯) ≫
      Spec.map (appLE f₂ (g ⁻¹ᵁ ↑U) (f₂ ⁻¹ᵁ g ⁻¹ᵁ ↑U) ⋯) ≫ ⋯.fromSpec =
    Spec.map (CommRingCat.ofHom ↑(integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val) ≫ (normalizationOpenCover f).f U ≫ f₂
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
        (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) ≫
      normalizationDesc f
        ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
          coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ =
    𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
by
    ext
    · refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)
      have H : iU ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inl :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.left⟩
      simp [reassoc_of% H]
    · refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)
      have H : iV ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inr :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.right⟩
      simp [reassoc_of% H]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ ↑(factor₁ m k hn p) * ↑(factor₂ m k hn p) = ↑(p.map (algebraMap R 𝓡'))

Tactic:
simp [factor₁, factor₂, ← Polynomial.map_mul, UniversalFactorizationRing.factor₁_mul_factor₂,
    Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
⊢ IsCoprime ↑(factor₁ m k hn p) ↑(factor₂ m k hn p)

Tactic:
cases subsingleton_or_nontrivial 𝓡'

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Subsingleton 𝓡'
⊢ IsCoprime ↑(factor₁ m k hn p) ↑(factor₂ m k hn p)

case inr
R : Type u_1
inst✝ : CommRing R
n m k : ℕ
hn : n = m + k
p : MonicDegreeEq R n
h✝ : Nontrivial 𝓡'
⊢ IsCoprime ↑(factor₁ m k hn p) ↑(factor₂ m k hn p)
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0

Tactic:
rw [ite_and]

Goal state after:
case inl
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m
⊢ (if ↑j ≤ ↑i then g.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + n then g.coeff (↑i - ↑j) else 0 else 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i ∧ ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0

Tactic:
rw [ite_and]

Goal state after:
case inr
m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin n
⊢ (if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0) = if ↑j ≤ ↑i then if ↑i ≤ ↑j + m then f.coeff (↑i - ↑j) else 0 else 0
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hf : f.natDegree ≤ m
hg : g.natDegree ≤ n
i : Fin (m + n)
j : Fin m ⊕ Fin n
⊢ (LinearMap.toMatrix (((degreeLT.basis R m).prod (degreeLT.basis R n)).reindex finSumFinEquiv)
        (degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) i (finSumFinEquiv j) =
    f.sylvester g m n i (finSumFinEquiv j)

Tactic:
simpa [LinearMap.toMatrix_apply] using congr($(toMatrix_sylvesterMap f g hf hg) i j)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
⊢ (Matrix.reindex e e) f.sylvesterDeriv = !![1]

Tactic:
have : NeZero (f.natDegree - 1 + f.natDegree) := ⟨by lia⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.natDegree = 1
e : Fin (f.natDegree - 1 + f.natDegree) ≃ Fin 1 := finCongr ⋯
this : NeZero (f.natDegree - 1 + f.natDegree)
⊢ (Matrix.reindex e e) f.sylvesterDeriv = !![1]