mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
x : PrimeSpectrum A
hx : x ∈ smoothLocus R A
f : A
hxf : x ∈ ↑(basicOpen f)
hf : Module.Projective (Localization.Away f) (LocalizedModule.Away f Ω[A⁄R])
Af : Type u_2 := Localization.Away f
this✝¹ : FinitePresentation A (Localization.Away f)
this✝ : FinitePresentation R (Localization.Away f)
this : IsOpen (smoothLocus R A ∩ ↑(basicOpen f))
⊢ ∃ t ⊆ smoothLocus R A, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨_, Set.inter_subset_left, this, hx, hxf⟩

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₂ e - f₁ e * f₂ e = 0

Tactic:
← h₂,

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
⊢ f₂ e - f₁ e * f₂ e = f₂ e * (1 - f₁ e)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
s : S
a : A
x : S ⊗[R] Ω[A⁄R]
⊢ s • a • x = a • s • x

Tactic:
induction x
    · simp only [smul_zero]
    · rw [mulActionBaseChange_smul_tmul, smul_tmul', smul_tmul', mulActionBaseChange_smul_tmul]
    · simp only [smul_add, *]

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

Goal state before:
pp: case mpr
K : Type u_1
A : Type u
inst✝³ : Field K
inst✝² : CommRing A
inst✝¹ : Algebra K A
inst✝ : EssFiniteType K A
I : Type u
w✝² : Finite I
Ai : I → Type u
w✝¹ : (i : I) → Field (Ai i)
w✝ : (i : I) → Algebra K (Ai i)
e : A ≃ₐ[K] (i : I) → Ai i
h✝ : ∀ (i : I), Algebra.IsSeparable K (Ai i)
⊢ ∀ (i : I), FormallyEtale K (Ai i)

Tactic:
exact fun I ↦ of_isSeparable K (Ai I)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Module.support A Ω[A⁄R] = ∅ ∧ Module.support A (H1Cotangent R A) = ∅ ↔ FormallyEtale R A

Tactic:
Module.support_eq_empty_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Subsingleton Ω[A⁄R] ∧ Module.support A (H1Cotangent R A) = ∅ ↔ FormallyEtale R A
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Subsingleton Ω[A⁄R] ∧ Module.support A (H1Cotangent R A) = ∅ ↔ FormallyEtale R A

Tactic:
Module.support_eq_empty_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ Subsingleton Ω[A⁄R] ∧ Subsingleton (H1Cotangent R A) ↔ FormallyEtale R A
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
this : Algebra.IsPushout R A S B
e₁ : B ⊗[A] Ω[A⁄R] ≃ₗ[A] Ω[A⁄R] ⊗[R] S :=
  AlgebraTensorModule.congr (↑(Algebra.IsPushout.equiv R A S B).symm) (LinearEquiv.refl A Ω[A⁄R]) ≪≫ₗ
      TensorProduct.comm A (A ⊗[R] S) Ω[A⁄R] ≪≫ₗ
    AlgebraTensorModule.cancelBaseChange R A A Ω[A⁄R] S
e₂ : B ⊗[A] Ω[A⁄R] ≃ₗ[R] Ω[B⁄S] :=
  LinearEquiv.restrictScalars R e₁ ≪≫ₗ TensorProduct.comm R Ω[A⁄R] S ≪≫ₗ
    LinearEquiv.restrictScalars R (tensorKaehlerEquivBase R S A B)
a : A
b : S
y✝ : Ω[A⁄R]
x y : A ⊗[R] S
a✝¹ :
  e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) x ⊗ₜ[A] y✝) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) x ⊗ₜ[A] y✝)
a✝ :
  e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) y ⊗ₜ[A] y✝) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) y ⊗ₜ[A] y✝)
⊢ e₂ ((Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • (Algebra.IsPushout.equiv R A S B) (x + y) ⊗ₜ[A] y✝) =
    (Algebra.IsPushout.equiv R A S B) (a ⊗ₜ[R] b) • e₂ ((Algebra.IsPushout.equiv R A S B) (x + y) ⊗ₜ[A] y✝)

Tactic:
simp only [smul_add, map_add, *, add_tmul]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_2
R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
y : AdicCompletion I N
⊢ y ∈ (map I g).ker → y ∈ (map I f).range

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
    intro hz
    obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (LinearMap.range f)
    have hb (n : ℕ) : g (b n) ∈ (I ^ n • ⊤ : Submodule R P) := by
      simpa using congrArg (fun x ↦ x.val n) hz
    let a := mapExactAux hf hfg hg hk b hb
    refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
    · refine fun n ↦ SModEq.symm ?_
      simp [a, mapExactAux, SModEq]
    · ext n
      suffices h : Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f (a n)) =
            Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (b (k + n)) by
        simp [h, AdicCauchySequence.mk_eq_mk (show n ≤ k + n by lia)]
      rw [Submodule.Quotient.eq]
      have hle : (I ^ (k + n) • ⊤ : Submodule R N) ≤ (I ^ n • ⊤ : Submodule R N) :=
        Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))
      exact hle (a n).property

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
⊢ Disjoint (Submodule.span R (Set.range (v ∘ a))) g.ker

Tactic:
rw [Submodule.disjoint_def, hfg.linearMap_ker_eq]

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
s : M →ₗ[R] K
hs : s ∘ₗ f = LinearMap.id
hfg : Function.Exact ⇑f ⇑g
ι : Type u_5
κ : Type u_6
v : ι → M
a : κ → ι
hainj : Function.Injective a
hsa : ∀ (i : κ), s (v (a i)) = 0
hli : LinearIndependent R v
⊢ ∀ x ∈ Submodule.span R (Set.range (v ∘ a)), x ∈ f.range → x = 0
Module: Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
obtain ⟨g', hg', hstd⟩ := this (R := R) (p.map (algebraMap S (Localization.Away g))) hsm

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
x✝ : (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime
g' : Localization.Away g
hg' : g' ∉ Ideal.map (algebraMap S (Localization.Away g)) p
hstd : IsStandardSmooth R (Localization.Away g')
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.g ^ 1 • RingHom.ker (algebraMap P.Ring S) ≤ RingHom.ker (algebraMap P.Ring D.T)

Tactic:
simpa using! D.hg

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
i : D.vars
⊢ ↑(D.q i).coeffs ⊆ Set.range ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))

Tactic:
by
  intro q hq
  have : (q.coeffs : Set A) ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x) :=
    Set.subset_iUnion_of_subset i (Set.subset_iUnion₂_of_subset q hq subset_rfl)
  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
  without the `rw`. It is not yet clear whether this is due to defeq abuse in Mathlib or a
  problem in the new canonicalizer; a minimization would help. The original proof was:
  `grind [MvPolynomial.mem_range_map_iff_coeffs_subset, subalgebra,
    Subalgebra.setRange_algebraMap, Algebra.subset_adjoin]` -/
  rw [MvPolynomial.mem_range_map_iff_coeffs_subset, Subalgebra.setRange_algebraMap]
  grind [subalgebra, Algebra.subset_adjoin]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (U.2.preimage f.continuous)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
⊢ x ∈ smoothLocus f

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (U.2.preimage f.continuous)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
⊢ x ∈ smoothLocus 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
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
⊢ ¬LinearIndependent k fun x ↦ (aeval a) ((monomial (σ' ↑x)) 1 ^ p)

Tactic:
monomial_pow,

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
⊢ ¬LinearIndependent k fun x ↦ (aeval a) ((monomial (p • σ' ↑x)) (1 ^ p))
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Etale) f

Tactic:
rw [etale_iff, affineLocally_iff_forall_isAffineOpen]

Goal state after:
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
hpm : p * F''.totalDegree ≤ F.totalDegree
⊢ False

Tactic:
by
    have hF''0' : F''.totalDegree ≠ 0 := by
      contrapose hF''0
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, aeval_C, map_eq_zero] at hF''
      rw [totalDegree_eq_zero_iff_eq_C.mp hF''0, hF'', map_zero]
    replace this := hpm.trans ((HF F'' hF''0 hF'').trans_eq (one_mul _).symm)
    exact hp.one_lt.not_ge ((mul_le_mul_iff_of_pos_right hF''0'.bot_lt).mp this)

Goal state after:
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 (Spec.map (CommRingCat.ofHom F) ≫ (pullbackSpecIso ↑R ↑S ↑S).inv)

Tactic:
← AlgebraicGeometry.diagonal_SpecMap R S

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.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ -(⇑f ∘ P) y - (W'.map f).a₁ * (⇑f ∘ P) x - (W'.map f).a₃ * (⇑f ∘ P) z = f (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
map_simp

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Projective F
f : F →+* K
P : Fin 3 → F
⊢ ((W.map f).a₁ * (⇑f ∘ P) y * (⇑f ∘ P) z -
          (3 * (⇑f ∘ P) x ^ 2 + 2 * (W.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ P) z + (W.map f).a₄ * (⇑f ∘ P) z ^ 2)) ^
        3 /
      (⇑f ∘ P) z ^ 2 =
    f ((W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) ^ 3 / P z ^ 2)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z * ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (W'.map f).a₁ * (⇑f ∘ P) x - (W'.map f).a₃ * (⇑f ∘ P) z)) ^ 3 =
    f (P z * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) ^ 3)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ -f (W'.negDblY P) - (W'.map f).a₁ * f (W'.dblX P) - (W'.map f).a₃ * f (W'.dblZ P) =
    f (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
map_simp

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -((⇑f ∘ P) y * (⇑f ∘ Q) z - (⇑f ∘ Q) y * (⇑f ∘ P) z) ^ 3 / ((⇑f ∘ P) z * (⇑f ∘ Q) z) =
    f (-(P y * Q z - Q y * P z) ^ 3 / (P z * Q z))

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ -3 * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z + 3 * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z +
                        (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z ^ 2 -
                      (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z ^ 2 +
                    (W'.map f).a₁ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) z ^ 2 -
                  (W'.map f).a₁ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 -
                (W'.map f).a₂ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) z ^ 2 +
              (W'.map f).a₂ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z ^ 2 +
            (W'.map f).a₃ * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
          (W'.map f).a₃ * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z -
        (W'.map f).a₄ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 +
      (W'.map f).a₄ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * P z ^ 2 * Q z)

Tactic:
map_simp

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ -(⇑f ∘ P) x * (⇑f ∘ Q) y ^ 2 * (⇑f ∘ P) z + (⇑f ∘ Q) x * (⇑f ∘ P) y ^ 2 * (⇑f ∘ Q) z -
                                2 * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ Q) z +
                              2 * (⇑f ∘ Q) x * (⇑f ∘ P) y * (⇑f ∘ Q) y * (⇑f ∘ P) z -
                            (W'.map f).a₁ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) y * (⇑f ∘ Q) z +
                          (W'.map f).a₁ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) y * (⇑f ∘ P) z +
                        (W'.map f).a₂ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) x * (⇑f ∘ Q) z -
                      (W'.map f).a₂ * (⇑f ∘ P) x * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z -
                    (W'.map f).a₃ * (⇑f ∘ P) x * (⇑f ∘ P) y * (⇑f ∘ Q) z ^ 2 +
                  (W'.map f).a₃ * (⇑f ∘ Q) x * (⇑f ∘ Q) y * (⇑f ∘ P) z ^ 2 -
                2 * (W'.map f).a₃ * (⇑f ∘ P) x * (⇑f ∘ Q) y * (⇑f ∘ P) z * (⇑f ∘ Q) z +
              2 * (W'.map f).a₃ * (⇑f ∘ Q) x * (⇑f ∘ P) y * (⇑f ∘ P) z * (⇑f ∘ Q) z +
            (W'.map f).a₄ * (⇑f ∘ P) x ^ 2 * (⇑f ∘ Q) z ^ 2 -
          (W'.map f).a₄ * (⇑f ∘ Q) x ^ 2 * (⇑f ∘ P) z ^ 2 +
        3 * (W'.map f).a₆ * (⇑f ∘ P) x * (⇑f ∘ P) z * (⇑f ∘ Q) z ^ 2 -
      3 * (W'.map f).a₆ * (⇑f ∘ Q) x * (⇑f ∘ P) z ^ 2 * (⇑f ∘ Q) z =
    f
      (-P x * Q y ^ 2 * P z + Q x * P y ^ 2 * Q z - 2 * P x * P y * Q y * Q z + 2 * Q x * P y * Q y * P z -
                              W'.a₁ * P x ^ 2 * Q y * Q z +
                            W'.a₁ * Q x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * Q x * Q z -
                        W'.a₂ * P x * Q x ^ 2 * P z -
                      W'.a₃ * P x * P y * Q z ^ 2 +
                    W'.a₃ * Q x * Q y * P z ^ 2 -
                  2 * W'.a₃ * P x * Q y * P z * Q z +
                2 * W'.a₃ * Q x * P y * P z * Q z +
              W'.a₄ * P x ^ 2 * Q z ^ 2 -
            W'.a₄ * Q x ^ 2 * P z ^ 2 +
          3 * W'.a₆ * P x * P z * Q z ^ 2 -
        3 * W'.a₆ * Q x * P z ^ 2 * Q z)

Tactic:
map_simp

Goal state after: