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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
⊢ IsOpenImmersion (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
⊢ IsOpenImmersion (pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑S))))
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ ∀ b ∈ F''.support, (p * b.sum fun x e ↦ e) ≤ F.totalDegree

Tactic:
]

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
p : ℕ
hp : Nat.Prime p
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
hF''0 : F'' ≠ 0
hF'' : (aeval a) F'' = 0
⊢ ∀ b ∈ F''.support, (p * b.sum fun x e ↦ e) ≤ F.totalDegree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
]

Goal state after:
case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * (e * x) ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom φ).toAlgebra
F : TensorProduct ↑R ↑S ↑S →+* ↑S := (Algebra.TensorProduct.lmul' ↑R).toRingHom
hF : Function.Surjective ⇑F
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom F))
e : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom F)) = Ideal.span {e}
x : ↑(CommRingCat.of (TensorProduct ↑R ↑S ↑S))
hx : e * x ∈ KaehlerDifferential.ideal ↑R ↑S
⊢ e * (e * x) ∈ KaehlerDifferential.ideal ↑R ↑S * KaehlerDifferential.ideal ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ (∀ (x : ↥x✝²), ∃ U, x ∈ U ∧ IsOpenImmersion (U.ι ≫ x✝)) ↔ ∀ (x : ↥x✝²), ∃ U, x ∈ U ∧ IsOpenImmersion (U.ι ≫ x✝)

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion IsOpenImmersion)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion IsOpenImmersion)
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (sourceLocalClosure IsOpenImmersion IsOpenImmersion).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)

Tactic:
]

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) X
h : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
⊢ ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.addY P Q = W.addY P Q

Tactic:
]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f],
    ((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R) → IsOpenImmersion (pullback.diagonal f)
hX : ¬((∃ S, X = Spec S) ∧ ∃ R, Y = Spec R)
𝒰Y : Y.OpenCover := Y.affineCover
𝒰X : (j : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).OpenCover :=
  fun j ↦ ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X j).affineCover
i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰Y).I₀
j : (𝒰X i).I₀
⊢ IsOpenImmersion (pullback.diagonal ((𝒰X i).f j ≫ pullback.snd f (𝒰Y.f i)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))) =
    W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
smul_fin3,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addXYZ P Q x, (u * v) ^ 2 * W'.addXYZ P Q y, (u * v) ^ 2 * W'.addXYZ P Q z]
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))

Tactic:
]

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
⊢ IsOpenImmersion (pullback.diagonal (Spec.map f))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q] =
    ![(u * v) ^ 2 * W'.addX P Q, (u * v) ^ 2 * W'.addY P Q, (u * v) ^ 2 * W'.addZ P Q]

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ ![0, 0, 0] = ![0, 0, 0]

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))

Tactic:
]

Goal state after:
X Y : Scheme
f✝ : X ⟶ Y
S R : CommRingCat
f : R ⟶ S
inst✝¹ : (CommRingCat.Hom.hom f).FormallyUnramified
inst✝ : (CommRingCat.Hom.hom f).FiniteType
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝¹ : Algebra.FormallyUnramified ↑R ↑S
algebraizeInst✝ : Algebra.FiniteType ↑R ↑S
⊢ IsOpenImmersion (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' ↑R).toRingHom))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ ![P y ^ 2 * Q z * Q x, P y ^ 2 * Q z * Q y, P y ^ 2 * Q z * Q z] =
    ![P y ^ 2 * Q z * Q x, P y ^ 2 * Q z * Q y, P y ^ 2 * Q z * Q z]

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ ![-(Q y ^ 2 * P z) * P x, -(Q y ^ 2 * P z) * P y, -(Q y ^ 2 * P z) * P z] =
    ![-(Q y ^ 2 * P z) * P x, -(Q y ^ 2 * P z) * P y, -(Q y ^ 2 * P z) * P z]

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, 0] = addU P Q • ![0, 1, 0]

Tactic:
smul_fin3,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, 0] = ![addU P Q * ![0, 1, 0] x, addU P Q * ![0, 1, 0] y, addU P Q * ![0, 1, 0] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ![0, addU P Q, 0] = ![0, addU P Q, 0]

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
smul_fin3,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          x,
      W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          y,
      W.addZ P Q *
        ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
              (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
            1]
          z]
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this✝ : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
this : Algebra.EssFiniteType ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
this✝ : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x))
this : Algebra.EssFiniteType ↑(Y.presheaf.stalk (f x)) ↑(X.presheaf.stalk x)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallyUnramified
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ ![W.addX P Q, W.addY P Q, W.addZ P Q] = ![W.addX P Q, W.addY P Q, W.addZ P Q]

Tactic:
]

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

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ ↑(0 * Scheme.Hom.ker i).support = Set.univ

Tactic:
]

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ ↑(0 * Scheme.Hom.ker i).support = Set.univ
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g], Q f → P (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
⊢ P fst

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
H : ∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g], Q f → P (pullback.fst f g) → P g
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
this : HasPullback f g
⊢ P fst
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ (g₁ ≫ f) ⁻¹ᵁ U

Tactic:
]

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this✝¹ : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
this✝ : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ ↑W
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ (g₁ ≫ f) ⁻¹ᵁ U
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
A✝ X✝ Y✝ Z✝ : C
fst✝ : A✝ ⟶ X✝
snd✝ : A✝ ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝² : Q.IsStableUnderBaseChange
inst✝¹ : P.HasOfPrecompProperty Q
inst✝ : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P (fst ≫ f)

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P Q W : MorphismProperty C
A✝ X✝ Y✝ Z✝ : C
fst✝ : A✝ ⟶ X✝
snd✝ : A✝ ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝² : Q.IsStableUnderBaseChange
inst✝¹ : P.HasOfPrecompProperty Q
inst✝ : P.RespectsRight Q
A X Y Z : C
fst : A ⟶ X
snd : A ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hf : Q f
hfst : P fst
⊢ P (fst ≫ f)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0

Tactic:
]

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
F : MvPolynomial ι k
hFmin : ∀ (G : MvPolynomial ι k), G ≠ 0 → (aeval a) G = 0 → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : (aeval a) F = 0
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ σ i
hσi : σ i ≠ 0
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis k fun x ↦ a ↑x
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (F.toPolynomialAdjoinImageCompl a i)
this✝ : UniqueFactorizationMonoid ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (Polynomial.map (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
⊢ (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0