mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ (if 2 ^ 6 * 3 ^ 3 = 0 then if 3 = 0 then ofJ1728 F else ofJ0 F
    else if 2 ^ 6 * 3 ^ 3 = 2 ^ 6 * 3 ^ 3 then ofJ1728 F else ofJNe0Or1728 (2 ^ 6 * 3 ^ 3)) =
    ofJ1728 F

Tactic:
if_neg (mul_ne_zero (pow_ne_zero 6 h2) (pow_ne_zero 3 h3)),

Goal state after:
case neg
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h2 : 2 ≠ 0
h3 : ¬3 = 0
⊢ (if 2 ^ 6 * 3 ^ 3 = 2 ^ 6 * 3 ^ 3 then ofJ1728 F else ofJNe0Or1728 (2 ^ 6 * 3 ^ 3)) = ofJ1728 F
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f)

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Limits.HasPullbacks C
K : Precoverage C
inst✝ : K.IsStableUnderBaseChange
S : C
F : Cᵒᵖ ⥤ Type u_2
𝒰 : K.ZeroHypercover S
𝒱 : K.ZeroHypercover S
f : Hom K 𝒰 𝒱
H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)
H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)
⊢ Presieve.IsSheafFor F (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
R : Presieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
E : PreOneHypercover X
F : Cᵒᵖ ⥤ Type u_2
h₁ : E.IsStronglySheafFor F
h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows
R : Presieve X
H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
H' :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hf : Presieve.IsSheaf J F
⊢ Presieve.IsSheafFor F (Sieve.generate E.presieve₀).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
R : Presieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F R

Tactic:
rw [Presieve.isSheafFor_iff_generate]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
J : GrothendieckTopology C
X : C
E : J.OneHypercover X
F : Cᵒᵖ ⥤ Type u_2
hF : Presieve.IsSheaf J F
R : Presieve X
h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows
h₂ :
  ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (E.p₁ k ≫ E.f i) (Sieve.generate R)).arrows
⊢ Presieve.IsSheafFor F (Sieve.generate R).arrows
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ P ≈ Q

Tactic:
by
  use (isUnit_Y_of_Z_eq_zero hP hPz).unit / (isUnit_Y_of_Z_eq_zero hQ hQz).unit
  simp only [Units.smul_def, smul_fin3, X_eq_zero_of_Z_eq_zero hQ.left hQz, hQz, mul_zero,
    Units.val_div_eq_div_val, IsUnit.unit_spec, (isUnit_Y_of_Z_eq_zero hQ hQz).div_mul_cancel]
  conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]

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

Goal state before:
pp: case refine_1
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) ∈ Scheme.zariskiTopology (⊥_ Scheme)

Tactic:
convert! (⊥_ Scheme).bot_mem_grothendieckTopology

Goal state after:
case e'_5
F : Schemeᵒᵖ ⥤ Type v
ι : Type u_1
inst✝¹ : Small.{u, u_1} ι
inst✝ : Small.{v, u_1} ι
hF : Presieve.IsSheaf Scheme.zariskiTopology F
X : ι → Schemeᵒᵖ
this : ∀ (i : ι), Mono (Cofan.inj (Sigma.cocone (Discrete.functor (unop ∘ X))) i)
⊢ Sieve.generate (Presieve.ofArrows Empty.elim fun a ↦ Empty.instIsEmpty.elim a) = ⊥
Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology

Goal state before:
pp: case refine_1.refine_3
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq : ∀ (i : 𝒰.I₀) (y : ↑(𝒰.X i)), (ConcreteCategory.hom (𝒰.f i)) y = ↑⟨(ConcreteCategory.hom (𝒰.f i)) y, ⋯⟩
x : (i : 𝒰.I₀) → (yoneda.obj X).obj (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (yoneda.obj X) 𝒰.f x
⊢ ∀ (x : ↑Y), ∃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.f i)) ∈ nhds x

Tactic:
· intro x
      obtain ⟨i, hi⟩ := exists_mem_zeroHypercover_range 𝒰 x
      exact ⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Projective R
W : Projective F
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
apply (toAffineAddEquiv W).injective
    simp only [map_add, toAffineAddEquiv_apply, toAffineLift_zero, add_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).Smooth ↔ Algebra.Smooth R S

Tactic:
RingHom.Smooth,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.Smooth R S ↔ Algebra.Smooth R S
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
⊢ (eval P) W.polynomialX ^ 3 / P z ^ 2 =
    (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:
eval_polynomialX

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → 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 =
    (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
Module: Mathlib.RingTheory.Smooth.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module.Flat R S
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : IsLocalRing R
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalHom (algebraMap R S)
inst✝² : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
M : Submonoid P
inst✝¹ : IsLocalization M S
inst✝ : FinitePresentation R P
⊢ FormallySmooth R S

Tactic:
by
  /-
  By the fact that `S` is essentially of finite presentation, we get
  `S = (P/I)[M⁻¹] = P[M⁻¹]/I[M⁻¹]`, where `P` is a polynomial ring and `M` some submonoid of `P/I`.
  We then apply `FormallySmooth.of_formallySmooth_residueField_tensor_aux` to this presentation.
  -/
  obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp
    (inferInstance : Algebra.FiniteType R P)
  let M' := M.comap f₀
  let P' := Localization M'
  let fP : P' →ₐ[R] S := IsLocalization.liftAlgHom (M := M')
      (f := (IsScalarTower.toAlgHom R P S).comp f₀) fun x ↦ by
    simpa using IsLocalization.map_units (M := M) _ ⟨f₀ x.1, x.2⟩
  have hf₁ : Function.Surjective fP := by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := hf₀ x
    obtain ⟨s, rfl⟩ := hf₀ s
    refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
    simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]
  have hfP : (RingHom.ker fP).FG := by
    have := Algebra.FinitePresentation.ker_fG_of_surjective _ hf₀
    convert! this.map (algebraMap _ P')
    refine le_antisymm ?_ (Ideal.map_le_iff_le_comap.mpr fun x hx ↦ by simp_all [fP])
    intro x hx
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M' x
    obtain ⟨a, ha, e⟩ : ∃ a ∈ M, a * f₀ x = 0 := by
      simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx
    obtain ⟨a, rfl⟩ := hf₀ a
    rw [IsLocalization.mk'_mem_map_algebraMap_iff]
    exact ⟨a, ha, by simpa⟩
  algebraize [fP.toRingHom]
  have : FormallyEtale (MvPolynomial (Fin n) R) P' := .of_isLocalization M'
  have : FormallySmooth R P' := .comp _ (MvPolynomial (Fin n) R) _
  have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')
  exact FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP

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

Goal state before:
pp: case h.right
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
y : N
n : ℕ
hxy : f x ≡ y [SMOD I ^ n • ⊤]
z : M
hz : z ∈ I ^ n • ⊤
hz' : f z ≡ y - f x [SMOD I ^ (n + 1) • ⊤]
⊢ f (x + z) ≡ y [SMOD I ^ (n + 1) • ⊤]

Tactic:
simpa [SModEq.sub_mem, sub_sub_eq_add_sub, add_comm] using hz'

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
y : K
hy : f y ∈ Submodule.span R (Set.range (v ∘ a))
⊢ f y = 0

Tactic:
have hz : s (f y) = 0 := by
    revert hy
    generalize f y = x
    intro hy
    induction hy using Submodule.span_induction with
    | mem m hm => obtain ⟨i, rfl⟩ := hm; apply hsa
    | zero => simp_all
    | add => simp_all
    | smul => simp_all

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
y : K
hy : f y ∈ Submodule.span R (Set.range (v ∘ a))
hz : s (f y) = 0
⊢ f y = 0
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ (aeval P.val) ((rename ⇑e) ((rename ⇑e.symm).mapMatrix (P.jacobiMatrix.submatrix ⇑f ⇑f)).det) =
    (aeval P.val) P.jacobiMatrix.det

Tactic:
← Matrix.det_submatrix_equiv_self f,

Goal state after:
case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ
val✝ : Fintype σ'
⊢ (aeval P.val) ((rename ⇑e) ((rename ⇑e.symm).mapMatrix (P.jacobiMatrix.submatrix ⇑f ⇑f)).det) =
    (aeval P.val) (P.jacobiMatrix.submatrix ⇑f ⇑f).det
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ LinearIndependent S fun i j ↦ (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
simp_rw [← SubmersivePresentation.basisDeriv_apply]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ LinearIndependent S fun i j ↦ P.basisDeriv i j
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
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.negDblY P * P z ^ 2 = -(eval P) W'.polynomialX ^ 3

Tactic:
rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ -(eval P) W'.polynomialX *
        ((eval P) W'.polynomialX ^ 2 - W'.a₁ * (eval P) W'.polynomialX * P z * (W'.negY P - W'.negY P) -
              W'.a₂ * P z ^ 2 * (W'.negY P - W'.negY P) ^ 2 -
            2 * P x * P z * (W'.negY P - W'.negY P) ^ 2 -
          P x * P z * (W'.negY P - W'.negY P) ^ 2) +
      W'.negY P * P z ^ 2 * (W'.negY P - W'.negY P) ^ 3 =
    -(eval P) W'.polynomialX ^ 3
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
⊢ Function.Injective ⇑P.toExtension.cotangentComplex

Tactic:
have := P.cotangentComplexAux_injective

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Function.Injective ⇑P.cotangentComplexAux
⊢ Function.Injective ⇑P.toExtension.cotangentComplex
Module: Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ = P.basisDeriv r x✝

Tactic:
basisDeriv_apply

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
r x✝ : σ
⊢ P.cotangentEquiv (Cotangent.mk ⟨P.relation r, ⋯⟩) x✝ = (aeval P.val) ((pderiv (P.map x✝)) (P.relation r))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -(P y * Q z - Q y * P z) ^ 3 / (P z * Q z) = 0

Tactic:
hQz,

Goal state after:
F : Type u
inst✝ : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ -(P y * 0 - Q y * P z) ^ 3 / (P z * 0) = 0
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
⊢ -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 =
    -(Q y ^ 2 * P z) * P z

Tactic:
hQz,

Goal state after:
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
⊢ -3 * P x ^ 2 * Q x * 0 + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * Q x * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * Q x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * Q x * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0

Tactic:
simp only [Submonoid.smul_def]

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ g ^ n • Extension.Cotangent.mk x = 0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := ⋯
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ⋯
f : P.Ring ⧸ P.ker ^ 2 := ⋯
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) := ⋯
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
⊢ ((localizationAway T g).toComp P).toAlgHom ↑x ∈ ((localizationAway T g).comp P).ker ^ 2

Tactic:
simpa only [LinearEquiv.coe_coe, LinearMap.ringLmapEquivSelf_symm_apply,
    mk_apply, lift.tmul, LinearMap.coe_restrictScalars, LinearMap.coe_smulRight,
    Module.End.one_apply, LinearMap.smul_apply, one_smul, Algebra.Extension.Cotangent.map_mk,
    Extension.Cotangent.mk_eq_zero_iff] using! hx

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
⊢ -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 =
    -(Q y ^ 2 * P z) * P x

Tactic:
hQz,

Goal state after:
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
⊢ -P x * Q y ^ 2 * P z + Q x * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * Q x * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * Q x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * Q x * 0 -
                      W'.a₂ * P x * Q x ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * Q x * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * Q x * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * Q x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * Q x * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x