mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((aeval (f pb.gen)) (derivative (minpoly K pb.gen)))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I

Tactic:
← hx,

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝¹ : FormallyUnramified K L
this✝ : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
this : IsUnit ((aeval ((Ideal.Quotient.mk I) x)) (derivative (minpoly K pb.gen)))
⊢ ∃ u, (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u * P y) - W'.a₁ * (u * P x) - W'.a₃ * (u * P z) = u * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
ring1

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x - W.a₃ * P z) / P z + -W.a₃ * 1 -
      (-(P y / P z) - W.toAffine.a₁ * (P x / P z) - W.toAffine.a₃ + -W.a₃ * (P z / P z)) =
    0

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hx : P x * Q z = Q x * P z
⊢ P y * Q z - Q y * P z + (P y * Q z - (-Q y - W'.a₁ * Q x - W'.a₃ * Q z) * P z) + -W'.a₁ * (Q x * P z) -
      ((P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) * Q z + -W'.a₁ * (P x * Q z)) =
    0

Tactic:
ring1

Goal state after:
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
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z + ((P y - negY ?m.132 P) * Q z + Q z * W'.negY P + (P y * Q z - W'.negY Q * P z)) -
      (Q y * P z + (P y * Q z - Q y * P z + (P y * Q z - negY ?m.132 Q * P z) + Q z * P y + 0)) =
    0

Tactic:
ring1

Goal state after:
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
hy' : P y * Q z - Q y * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z + ((P y - negY ?m.132 P) * Q z + Q z * W'.negY P + (P y * Q z - Q y * P z)) -
      (W'.negY Q * P z + (P y * Q z - Q y * P z + (P y * Q z - negY ?m.132 Q * P z) + Q z * P y + 0)) =
    0

Tactic:
ring1

Goal state after:
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
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
⊢ (fun a ↦ a * Q z) (P y) + (P y * Q z - Q y * P z + (P y * Q z - negY ?m.104 Q * P z) + Q y * P z + W'.negY Q * P z) -
      ((fun a ↦ a * Q z) (W'.negY P) + ((P y - negY ?m.104 P) * Q z + P y * Q z + P y * Q z)) =
    0

Tactic:
ring1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y * P z + W.a₁ * P x * P z + W.a₃ * P z ^ 2 = (P y - (-P y - W.a₁ * P x - W.a₃ * P z)) * P z

Tactic:
ring1

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
u : R
⊢ u * P z * (u * P y - u * W'.negY P) ^ 3 = u ^ 4 * (P z * (P y - W'.negY P) ^ 3)

Tactic:
ring1

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : IntermediateField.map K⟮x, y⟯.val K⟮⟨α, hα⟩⟯ = IntermediateField.map K⟮x, y⟯.val ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
IntermediateField.adjoin_map,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : IntermediateField.adjoin K (⇑K⟮x, y⟯.val '' {⟨α, hα⟩}) = IntermediateField.map K⟮x, y⟯.val ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul
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
b : B
z : A
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * b) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) b +
      b • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
induction b using h.out.inductionOn with
      | zero => rw [map_zero, zero_smul, smul_zero, zero_add, mul_zero, map_zero]
      | tmul =>
        simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          algebraMap_smul, ← map_mul]
        rw [← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq,
          ← IsScalarTower.toAlgHom_apply R, ← AlgHom.toLinearMap_apply, h.out.lift_eq]
        simp only [LinearMap.coe_comp, Derivation.coeFn_coe, Function.comp_apply,
          Derivation.leibniz, mk_apply, mulActionBaseChange_smul_tmul, TensorProduct.tmul_add]
      | smul _ _ e =>
        rw [mul_comm, smul_mul_assoc, map_smul, mul_comm, e,
            map_smul, smul_add, smul_comm, smul_assoc]
      | add _ _ e₁ e₂ => simp only [mul_add, add_smul, map_add, e₁, e₂, smul_add, add_add_add_comm]

Goal state after:
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
h : Algebra.IsPushout R S A B
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]

Tactic:
have : Algebra.IsPushout R A S B := .symm inferInstance

Goal state after:
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
⊢ B ⊗[A] Ω[A⁄R] ≃ₗ[B] Ω[B⁄S]
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
inst✝ : Algebra.IsPushout R S A B
b : B
a : A
⊢ (tensorKaehlerEquiv R S A B) (b ⊗ₜ[A] (D R A) a) = b • (D S B) ((algebraMap A B) a)

Tactic:
have : Algebra.IsPushout R A S B := .symm inferInstance

Goal state after:
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
inst✝ : Algebra.IsPushout R S A B
b : B
a : A
this : Algebra.IsPushout R A S B
⊢ (tensorKaehlerEquiv R S A B) (b ⊗ₜ[A] (D R A) a) = b • (D S B) ((algebraMap A B) a)
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
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
s : ↥M'
hx : IsLocalization.mk' P' x s ∈ RingHom.ker fP
a : P
ha : a ∈ M
e : a * f₀ x = 0
⊢ IsLocalization.mk' P' x s ∈ Ideal.map (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom)

Tactic:
obtain ⟨a, rfl⟩ := hf₀ a

Goal state after:
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
n : ℕ
f₀ : MvPolynomial (Fin n) R →ₐ[R] P
hf₀ : Function.Surjective ⇑f₀
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
fP : P' →ₐ[R] S := IsLocalization.liftAlgHom ⋯
hf₁ : Function.Surjective ⇑fP
this : (RingHom.ker f₀.toRingHom).FG
x : MvPolynomial (Fin n) R
s : ↥M'
hx : IsLocalization.mk' P' x s ∈ RingHom.ker fP
a : MvPolynomial (Fin n) R
ha : f₀ a ∈ M
e : f₀ a * f₀ x = 0
⊢ IsLocalization.mk' P' x s ∈ Ideal.map (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.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
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 ^ 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) *
      (W'.negY P - W'.negY P) =
    0

Tactic:
ring1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ n * (n + -(P z * d * W.toAffine.a₁)) - P z ^ 2 * d ^ 2 * W.toAffine.a₂ - P z * d ^ 2 * P x - P z * d ^ 2 * P x =
    n * (n - P z * d * W.toAffine.a₁) - P z ^ 2 * d ^ 2 * W.toAffine.a₂ - P z * d ^ 2 * P x * 2

Tactic:
ring1

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

Goal state before:
pp: 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
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = (factor ⋯) y'

Tactic:
hyy',

Goal state after:
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
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ (I ^ n • ⊤).mkQ (f x) = y
Module: Mathlib.RingTheory.Smooth.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
e : S ≃ₐ[R] T
inst✝ : IsStandardSmooth R S
⊢ IsStandardSmooth R T

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
  exact (P.ofAlgEquiv e).isStandardSmooth

Goal state after:
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 : PreSubmersivePresentation R S ι σ
x : ↥P.ker
⊢ P.cotangentComplexAux (Cotangent.mk x) = 0 ↔ ∀ (i : σ), (aeval P.val) ((pderiv (P.map i)) ↑x) = 0

Tactic:
rw [funext_iff]
  simp_rw [cotangentComplexAux_apply, Pi.zero_apply]

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
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

Tactic:
ring1

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
Affine.negAddY,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d * (W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) - P x / P z) + P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(u ^ 4 * W'.negDblY P) - W'.a₁ * (u ^ 4 * W'.dblX P) - W'.a₃ * (u ^ 4 * W'.dblZ P) =
    u ^ 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
ring1

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 : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -P y ^ 4 - W'.a₁ * 0 - W'.a₃ * 0 = P y ^ 4

Tactic:
ring1

Goal state after:
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
hPz : P z ≠ 0
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 - W'.a₁ * 0 - W'.a₃ * 0) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ (-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) *
          (P z * Q z) +
        (Q z ^ 3 * 0 +
          P z ^ 3 *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3))) -
      ((P x * Q z - Q x * P z) ^ 3 +
        (Q z ^ 3 *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          P z ^ 3 * 0)) =
    0

Tactic:
ring1

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
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q z) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P z) +
                        (u * P y) ^ 2 * (v * Q z) ^ 2 -
                      (v * Q y) ^ 2 * (u * P z) ^ 2 +
                    W'.a₁ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 -
                W'.a₂ * (u * P x) ^ 2 * (v * Q z) ^ 2 +
              W'.a₂ * (v * Q x) ^ 2 * (u * P z) ^ 2 +
            W'.a₃ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
          W'.a₃ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * (v * Q z) ^ 2 +
      W'.a₄ * (v * Q x) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-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:
ring1

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
⊢ -3 * P x ^ 2 * P x * P z + 3 * P x * P x ^ 2 * P z + P y ^ 2 * P z ^ 2 - P y ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * P y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * P z ^ 2 +
              W'.a₂ * P x ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * P z ^ 2 -
          W'.a₃ * P y * P z ^ 2 * P z -
        W'.a₄ * P x * P z * P z ^ 2 +
      W'.a₄ * P x * P z ^ 2 * P z =
    0

Tactic:
ring1

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
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q z + 3 * 0 * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * 0 * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * 0 ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * 0 * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z

Tactic:
ring1

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

Tactic:
ring1

Goal state after: