mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y : FractionRing R[X]
y✝ : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := y }

Tactic:
cases y using Localization.induction_on with | _ a'

Goal state after:
case H.H
G₀ : Type u_1
R : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : CommRing R
inst✝ : Nontrivial R
φ : R[X] →*₀ G₀
hφ : Function.Injective ⇑φ
hφ' : R[X]⁰ ≤ Submonoid.comap φ G₀⁰
y✝ a' : R[X] × ↥R[X]⁰
⊢ (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk y✝.1 y✝.2 } =
      (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } →
    { toFractionRing := Localization.mk y✝.1 y✝.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite

Goal state before:
pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : Algebra (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) := ⋯
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    Algebra.QuasiFinite (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal)

pp: R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : Algebra (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) := ⋯
⊢ Algebra.QuasiFinite (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) ↔
    Algebra.QuasiFiniteAt (↑R) x.asIdeal

Tactic:
· rw [← RingHom.quasiFinite_algebraMap]
    exact RingHom.QuasiFinite.respectsIso.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso ..)

Goal state after:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst✝ : (CommRingCat.Hom.hom φ).FiniteType
algInst✝ : Algebra ↑R ↑S := ⋯
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
this : Algebra (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) := ⋯
⊢ Algebra.QuasiFinite (Localization.AtPrime (Ideal.under (↑R) x.asIdeal)) (Localization.AtPrime x.asIdeal) ↔
    Algebra.QuasiFiniteAt (↑R) x.asIdeal
Module: Mathlib.FieldTheory.RatFunc.Basic

Goal state before:
pp: case f.hd
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⟯) q ≠ 0

Tactic:
exact algebraMap_ne_zero hq

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

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

Tactic:
num_div,

Goal state after:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).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
⊢ (algebraMap K[X] K⟮X⟯) q ≠ 0

Tactic:
exact algebraMap_ne_zero hq

Goal state after:
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
s : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
⊢ Function.Bijective ⇑(toIntegralClosure R S B)

Tactic:
let φ (r : s) : integralClosure S (S ⊗[R] B) →ₐ[S] integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B) :=
    ((Algebra.TensorProduct.map (Algebra.ofId _ _) (.id _ _)).comp
      (integralClosure S (S ⊗[R] B)).val).codRestrict
        ((integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)).restrictScalars S) <| by
    simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply,
      Subalgebra.mem_restrictScalars, Subtype.forall, mem_integralClosure_iff]
    exact fun a ha ↦ (ha.map _).tower_top

Goal state after:
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 : Set S
hs : Ideal.span s = ⊤
Sᵣ : ↑s → Type u_4
inst✝⁴ : (r : ↑s) → CommRing (Sᵣ r)
inst✝³ : (r : ↑s) → Algebra S (Sᵣ r)
inst✝² : (r : ↑s) → Algebra R (Sᵣ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Sᵣ r)
H : ∀ (r : ↑s), Function.Bijective ⇑(toIntegralClosure R (Sᵣ r) B)
this :
  ∀ (r : ↑s),
    IsLocalizedModule.Away (↑r)
      (Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R ↥(integralClosure R B))).toLinearMap
φ : (r : ↑s) → ↥(integralClosure S (S ⊗[R] B)) →ₐ[S] ↥(integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B)) :=
  fun r ↦
    ((Algebra.TensorProduct.map (Algebra.ofId S (Sᵣ r)) (AlgHom.id R B)).comp
          (integralClosure S (S ⊗[R] B)).val).codRestrict
      (Subalgebra.restrictScalars S (integralClosure (Sᵣ r) (Sᵣ r ⊗[R] B))) ⋯
⊢ Function.Bijective ⇑(toIntegralClosure R S B)
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
φ : 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
⊢ ∀ a ∈ m,
    (Multiset.map (fun x ↦ X - C x) m).prod ∣
      (Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * (Polynomial.map (algebraMap S S') y - C ((aeval a) y))

Tactic:
intro a ham

Goal state after:
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
a : S'
ham : a ∈ m
⊢ (Multiset.map (fun x ↦ X - C x) m).prod ∣
    (Multiset.map (fun x ↦ X - C x) (m.erase a)).prod * (Polynomial.map (algebraMap S S') y - C ((aeval a) y))
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✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : ∀ (k : ℕ), IsIntegral (AdjoinRoot 𝓟.f) ((algebraMap (AdjoinRoot 𝓟.f) S) ((AdjoinRoot.mk 𝓟.f) 𝓟.g) ^ (m + k) • a)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)

Tactic:
have := 𝓟.monic_f.finite_adjoinRoot

Goal state after:
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✝ : Algebra.IsStandardEtale R S
a : S ⊗[R] B
hx : IsIntegral S a
𝓟 : StandardEtalePresentation R S
e : S ≃ₐ[R] Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g) := 𝓟.equivRing.trans 𝓟.equivAwayAdjoinRoot
algInst✝ : Algebra (AdjoinRoot 𝓟.f) S :=
  ((↑e.symm).comp (IsScalarTower.toAlgHom R (AdjoinRoot 𝓟.f) (Localization.Away ((AdjoinRoot.mk 𝓟.f) 𝓟.g)))).toAlgebra
this✝ : IsLocalization (Submonoid.powers ((AdjoinRoot.mk 𝓟.f) 𝓟.g)) S
m : ℕ
hm : ∀ (k : ℕ), IsIntegral (AdjoinRoot 𝓟.f) ((algebraMap (AdjoinRoot 𝓟.f) S) ((AdjoinRoot.mk 𝓟.f) 𝓟.g) ^ (m + k) • a)
this : Module.Finite R (AdjoinRoot 𝓟.f)
⊢ ∃ n, ∀ (m : ℕ), IsIntegral R ((aeval 𝓟.x) 𝓟.g ^ (n + m) • a)
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✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
⊢ IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)

Tactic:
have := 𝓟.monic_f.finite_adjoinRoot

Goal state after:
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✝ : Algebra.IsStandardEtale R S
𝓟 : StandardEtalePresentation R S
n : ℕ
𝓟' : StandardEtalePresentation B (B ⊗[R] S) := 𝓟.baseChange
e : B ⊗[R] S ≃ₐ[B] Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g) := 𝓟'.equivRing.trans 𝓟'.equivAwayAdjoinRoot
a : AdjoinRoot 𝓟'.f
m : ℕ
hx✝ :
  IsIntegral S
    ((Algebra.TensorProduct.comm R B S)
      (e.symm
        (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
          ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
hx :
  ∀ (m_1 : ℕ),
    IsIntegral R
      ((aeval 𝓟.x) 𝓟.g ^ (n + m_1) •
        (Algebra.TensorProduct.comm R B S)
          (e.symm
            (IsLocalization.mk' (Localization.Away ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)) a
              ⟨(fun x ↦ (AdjoinRoot.mk 𝓟'.f) 𝓟'.g ^ x) m, ⋯⟩)))
this : Module.Finite R (AdjoinRoot 𝓟.f)
⊢ IsIntegral R ((AdjoinRoot.mk 𝓟'.f) 𝓟'.g)
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
⊢ φ p * (t * x) ∈ φ.range

Tactic:
by convert! this using 1; ring

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
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝² : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝¹ : Algebra R[X] S := f.toAlgebra
this✝ : IsScalarTower R R[X] S
this : Module.Finite R[X] S
p : R[X]
hp : (algebraMap R[X] S) p = 0
⊢ p = 0

Tactic:
by_contra hp'

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : IsIntegrallyClosed R
inst✝² : IsDomain S
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : WeaklyQuasiFiniteAt R P
this✝² : IsDomain R
f : R[X] →ₐ[R] S
hx' : f.Finite
hf' : Function.Injective ⇑f
hx : IsStronglyTranscendental R (f X)
hf : aeval (f X) = f
this✝¹ : Algebra R[X] S := f.toAlgebra
this✝ : IsScalarTower R R[X] S
this : Module.Finite R[X] S
p : R[X]
hp : (algebraMap R[X] S) p = 0
hp' : ¬p = 0
⊢ False
Module: Mathlib.RingTheory.ZariskisMainTheorem

Goal state before:
pp: case pos.refine_1
R✝ S✝ : Type u
inst✝⁷ : CommRing R✝
inst✝⁶ : CommRing S✝
inst✝⁵ : Algebra R✝ S✝
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] = ⊤
H : integralClosure R S = ⊥
H₀ : Function.Surjective ⇑(aeval x)
f : R[X]
hf : (aeval x) f = 0
n : ℕ
hfn : (algebraMap R S) (f.coeff n) ∉ p
m : ℕ
IH :
  ∀ m_1 < m + 1,
    ∀ (f : R[X]),
      (aeval x) f = 0 → ∀ (n : ℕ), (algebraMap R S) (f.coeff n) ∉ p → f.natDegree = m_1 → ZariskisMainProperty R p
hm : f.natDegree = m + 1
Hfp : (algebraMap R S) f.leadingCoeff ∈ p
a : R
ha : (ofId R S).toRingHom a = f.leadingCoeff • x
⊢ (f.eraseLead + C a * X ^ m).natDegree < m + 1

Tactic:
suffices f.eraseLead.natDegree ≤ m by compute_degree!
      exact (eraseLead_natDegree_le ..).trans (by lia)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U)

Tactic:
let e := IsOpenImmersion.isoOfRangeEq (pullback.fst f.toNormalization
    (f.normalizationOpenCover.f U)) (f ⁻¹ᵁ U.1).ι (by simp [← Hom.coe_opensRange,
      Hom.opensRange_pullbackFst, ← f.fromNormalization_preimage, ← Scheme.Hom.comp_preimage])

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : IsIntegralHom f
U : (normalizationOpenCover f).toPreZeroHypercover.1
e : pullback (toNormalization f) ((normalizationOpenCover f).f U) ≅ ↑(f ⁻¹ᵁ ↑U) :=
  IsOpenImmersion.isoOfRangeEq (pullback.fst (toNormalization f) ((normalizationOpenCover f).f U)) (f ⁻¹ᵁ ↑U).ι ⋯
⊢ MorphismProperty.isomorphisms Scheme (Cover.pullbackHom (normalizationOpenCover f) (toNormalization f) U)
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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ¬g.natDegree = 0
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod

Tactic:
rw [hg'.natDegree_eq_card_roots, Multiset.card_eq_zero,
          Multiset.eq_zero_iff_forall_notMem, not_forall_not] at H

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
g : K[X]
hg : g.Monic
hg' : g.Splits
r : K[X]
hf : (g * r).Monic
hf' : (g * r).Splits
hfg : g.natDegree ≤ (g * r).natDegree
hN : (g * r).natDegree + g.natDegree = n
hr' : r ≠ 0
H : ∃ x, x ∈ g.roots
⊢ 0 * g.coeff 0 ^ (g * r).natDegree = (Multiset.map (fun ij ↦ ij.1 - ij.2) ((g * r).roots ×ˢ g.roots)).prod
Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
⊢ normalizationDesc f f₁ f₂ H ≫ f₂ = fromNormalization f

Tactic:
refine colimit.hom_ext fun U ↦ ?_

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst✝ : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U : (directedCover Y).I₀
⊢ colimit.ι (normalizationGlueData f).functor U ≫ normalizationDesc f f₁ f₂ H ≫ f₂ =
    colimit.ι (normalizationGlueData f).functor U ≫ fromNormalization f
Module: Mathlib.RingTheory.Polynomial.Resultant.Basic

Goal state before:
pp: case inr
K : Type u_2
inst✝ : Field K
f g : K[X]
hf : f ≠ 0
H : (C f.leadingCoeff⁻¹ * f).Monic
this : IsUnit (f.leadingCoeff⁻¹ ^ g.natDegree) ∧ IsUnit (f.resultant g) ↔ IsCoprime f g
⊢ f.resultant g = 0 ↔ (f ≠ 0 ∨ g ≠ 0) ∧ ¬IsCoprime f g

Tactic:
simp [← this, hf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.ZariskisMainTheorem

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ ∃ V, y ∈ V ∧ IsFinite (f ∣_ V)

Tactic:
refine ⟨V, ?_, ?_⟩

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ y ∈ V

case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : IsProper f
y : ↥Y
hx : (⇑f ⁻¹' {y}).Finite
V : Y.Opens := { carrier := (⇑f '' (↑(Scheme.Hom.quasiFiniteLocus f))ᶜ)ᶜ, is_open' := ⋯ }
⊢ IsFinite (f ∣_ V)
Module: Mathlib.RingTheory.Finiteness.Descent

Goal state before:
pp: R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : (algebraMap S (S ⊗[R] T)).FiniteType
⊢ (algebraMap R T).FiniteType

Tactic:
rw [finiteType_algebraMap] at h' ⊢

Goal state after:
R S T : Type u_4
x✝⁴ : CommRing R
x✝³ : CommRing S
x✝² : CommRing T
x✝¹ : Algebra R S
x✝ : Algebra R T
h : (algebraMap R S).FaithfullyFlat
h' : Algebra.FiniteType S (S ⊗[R] T)
⊢ Algebra.FiniteType R T
Module: Mathlib.RingTheory.Ideal.CotangentBaseChange

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
x : ↥I
⊢ (map a I).cotangentToQuotientSquare ((tensorCotangentHom R T I) (1 ⊗ₜ[R] I.toCotangent x)) =
    (Quotient.mk (map a I ^ 2)) (1 ⊗ₜ[R] ↑x)

Tactic:
rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
I : Ideal S
inst✝ : Module.Flat R T
a : S →+* T ⊗[R] S := Algebra.TensorProduct.includeRight.toRingHom
f : (map a I).Cotangent →ₗ[T] T ⊗[R] S ⧸ map a I ^ 2 := ↑T (map a I).cotangentToQuotientSquare
g : T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2) := (AlgebraTensorModule.lTensor T T) (↑R I.cotangentToQuotientSquare)
hₐ : T ⊗[R] (S ⧸ I ^ 2) ≃ₐ[T] T ⊗[R] S ⧸ map a I ^ 2 :=
  (Algebra.TensorProduct.tensorQuotientEquiv T S T (I ^ 2)).trans (quotientEquivAlgOfEq T ⋯)
x : ↥I
⊢ (Submodule.mkQ (map a I ^ 2)) ↑⟨1 ⊗ₜ[R] ↑x, ⋯⟩ = (Quotient.mk (map a I ^ 2)) (1 ⊗ₜ[R] ↑x)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent

Goal state before:
pp: X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ IsOpen (⋃ i ∈ irreducibleComponents ↥X \ {Z}, i)ᶜ

Tactic:
isOpen_compl_iff

Goal state after:
X : Scheme
Z : Set ↥X
hZ : Z ∈ irreducibleComponents ↥X
inst✝ : IsNoetherian X
⊢ IsClosed (⋃ i ∈ irreducibleComponents ↥X \ {Z}, i)
Module: Mathlib.AlgebraicGeometry.LimitsOver

Goal state before:
pp: X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
⊢ IsOpenImmersion (colimit.ι F j).left

Tactic:
← MorphismProperty.Over.forget_comp_forget_map

Goal state after:
X : Scheme
P : MorphismProperty Scheme
inst✝⁵ : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst✝⁴ : Category.{v_1, u_1} J
F : J ⥤ P.Over ⊤ S
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).left
inst✝² : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, u_1} J
j : J
⊢ IsOpenImmersion ((MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S).map (colimit.ι F j))
Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : Adj B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj) el.hom = er.hom
⊢ (conjugateEquiv α.adj β.adj) el.inv = er.inv

Tactic:
rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]

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

Goal state before:
pp: ⊢ @WeaklyEtale = @Flat ⊓ MorphismProperty.diagonal @Flat

Tactic:
by
  ext
  exact weaklyEtale_iff _

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]
  infer_instance

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

Goal state before:
pp: W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]
  infer_instance

Goal state after: