mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ embedRealFun 1 ≤ 1

pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ 1 ≤ embedRealFun 1

Tactic:
· apply csSup_le (ratLt'_nonempty 1)
    suffices ∀ (x : ℚ), x.num • (1 : M) < (x.den : ℤ) • (1 : M) → (x : ℝ) ≤ 1 by simpa using this
    intro x hx
    suffices x ≤ 1 by norm_cast
    simpa [Rat.le_iff] using ((smul_lt_smul_iff_of_pos_right zero_lt_one).mp hx).le

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
⊢ 1 ≤ embedRealFun 1
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : y ∈ closedBall x r
⊢ closedBall x r = closedBall y r

Tactic:
ext
  simp_rw [mem_closedBall] at h ⊢
  constructor <;> intro h' <;>
  exact (dist_triangle_max _ _ _).trans (max_le h' (dist_comm x _ ▸ h))

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
⊢ ∀ x_1 ∉ ball x r, ∃ ε > 0, ball x_1 ε ⊆ (ball x r)ᶜ

Tactic:
intro y hy

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
h : 0 < r
y : X
hy : y ∉ ball x r
⊢ ∃ ε > 0, ball y ε ⊆ (ball x r)ᶜ
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
⊢ ∀ x_1 ∈ closedBall x r, ∃ ε, 0 < ε ∧ ball x_1 ε ⊆ closedBall x r

Tactic:
intro y hy

Goal state after:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x : X
r : ℝ
hr : r ≠ 0
h : 0 < r
y : X
hy : y ∈ closedBall x r
⊢ ∃ ε, 0 < ε ∧ ball y ε ⊆ closedBall x r
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case h
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
x : K
hx : x ≠ 0
hxy : (RankLeOne.hom' valuation) (valuation.restrict x) < ⟨ε, ⋯⟩
⊢ {x_1 | valuation.restrict x_1 < ↑(Units.mk0 (valuation.restrict x) ⋯)} ⊆ U

Tactic:
intro y hy

Goal state after:
case h
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
x : K
hx : x ≠ 0
hxy : (RankLeOne.hom' valuation) (valuation.restrict x) < ⟨ε, ⋯⟩
y : K
hy : y ∈ {x_1 | valuation.restrict x_1 < ↑(Units.mk0 (valuation.restrict x) ⋯)}
⊢ y ∈ U
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x x' : L
⊢ ‖x‖ ≤ ‖x'‖ ↔ v x ≤ v x'

Tactic:
by
  rw [← v.restrict_le_iff, ← (Valuation.RankOne.strictMono val.v).le_iff_le]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
j : R
⊢ ((j - 1728) ^ 2 + 4 * 0) ^ 2 - 24 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) = j * (j - 1728) ^ 3

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
j : R
⊢ -((j - 1728) ^ 2 + 4 * 0) ^ 2 *
            ((j - 1728) ^ 2 * -(j - 1728) ^ 5 + 4 * 0 * -(j - 1728) ^ 5 - (j - 1728) * 0 * (-36 * (j - 1728) ^ 3) +
                0 * 0 ^ 2 -
              (-36 * (j - 1728) ^ 3) ^ 2) -
          8 * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * -(j - 1728) ^ 5) ^ 2 +
      9 * ((j - 1728) ^ 2 + 4 * 0) * (2 * (-36 * (j - 1728) ^ 3) + (j - 1728) * 0) * (0 ^ 2 + 4 * -(j - 1728) ^ 5) =
    j ^ 2 * (j - 1728) ^ 9

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ ↑(ofJ0 R).Δ'⁻¹ * 0 ^ 3 = 0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (IsUnit 3)
⊢ (ofJ0 R).j = 0

Tactic:
by
  rw [j, ofJ0_c₄]
  ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
j : R
inst✝¹ : Fact (IsUnit j)
inst✝ : Fact (IsUnit (j - 1728))
⊢ (j * (j - 1728) ^ 3) ^ 3 = j ^ 2 * (j - 1728) ^ 9 * j

Tactic:
ring1

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

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 - W'.a₁ * P x - W'.a₃ * P z) ^ 2 * P z ^ 2 +
                    W'.a₁ * P x * P y * P z ^ 2 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * 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 - W'.a₁ * P x - W'.a₃ * P z) * 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.Point

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

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q x * Q z = Q x * (↑u * Q z)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q y * Q z = Q y * (↑u * Q z)

Tactic:
ring1

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

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

Tactic:
ring1

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

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

Tactic:
ring1

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Goal state before:
pp: case trans
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)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
⊢ Presieve.IsSeparatedFor F (Presieve.pullbackArrows f (Presieve.ofArrows 𝒰.X 𝒰.f))

Tactic:
← Presieve.ofArrows_pullback

Goal state after:
case trans
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)
Y : C
f : Y ⟶ S
hf : (Sieve.generate (Presieve.ofArrows 𝒱.X 𝒱.f)).arrows f
⊢ Presieve.IsSeparatedFor F (Presieve.ofArrows (fun i ↦ pullback (𝒰.f i) f) fun x ↦ pullback.snd (𝒰.f x) f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

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

Tactic:
ring1

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

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 ^ 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 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + W.toAffine.a₁ * (P x / P z) * (P y / P z) + W.toAffine.a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + W.toAffine.a₂ * (P x / P z) ^ 2 + W.toAffine.a₄ * (P x / P z) + W.toAffine.a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * Y ^ (2 - 1) * 0 * Z + Y ^ 2 * 0 + (((0 * X + C W'.a₁ * 1) * Y + C W'.a₁ * X * 0) * Z + C W'.a₁ * X * Y * 0) +
        ((0 * Y + C W'.a₃ * 0) * Z ^ 2 + C W'.a₃ * Y * (↑2 * Z ^ (2 - 1) * 0)) -
      (↑3 * X ^ (3 - 1) * 1 + ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 1)) * Z + C W'.a₂ * X ^ 2 * 0) +
          ((0 * X + C W'.a₄ * 1) * Z ^ 2 + C W'.a₄ * X * (↑2 * Z ^ (2 - 1) * 0)) +
        (0 * Z ^ 3 + C W'.a₆ * (↑3 * Z ^ (3 - 1) * 0))) =
    C W'.a₁ * Y * Z - (3 * X ^ 2 + 2 * C W'.a₂ * X * Z + C W'.a₄ * Z ^ 2)

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * Y ^ (2 - 1) * 1 * Z + Y ^ 2 * 0 + (((0 * X + C W'.a₁ * 0) * Y + C W'.a₁ * X * 1) * Z + C W'.a₁ * X * Y * 0) +
        ((0 * Y + C W'.a₃ * 1) * Z ^ 2 + C W'.a₃ * Y * (↑2 * Z ^ (2 - 1) * 0)) -
      (↑3 * X ^ (3 - 1) * 0 + ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 0)) * Z + C W'.a₂ * X ^ 2 * 0) +
          ((0 * X + C W'.a₄ * 0) * Z ^ 2 + C W'.a₄ * X * (↑2 * Z ^ (2 - 1) * 0)) +
        (0 * Z ^ 3 + C W'.a₆ * (↑3 * Z ^ (3 - 1) * 0))) =
    2 * Y * Z + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 2

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * Y ^ (2 - 1) * 0 * Z + Y ^ 2 * 1 + (((0 * X + C W'.a₁ * 0) * Y + C W'.a₁ * X * 0) * Z + C W'.a₁ * X * Y * 1) +
        ((0 * Y + C W'.a₃ * 0) * Z ^ 2 + C W'.a₃ * Y * (↑2 * Z ^ (2 - 1) * 1)) -
      (↑3 * X ^ (3 - 1) * 0 + ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 0)) * Z + C W'.a₂ * X ^ 2 * 1) +
          ((0 * X + C W'.a₄ * 0) * Z ^ 2 + C W'.a₄ * X * (↑2 * Z ^ (2 - 1) * 1)) +
        (0 * Z ^ 3 + C W'.a₆ * (↑3 * Z ^ (3 - 1) * 1))) =
    Y ^ 2 + C W'.a₁ * X * Y + 2 * C W'.a₃ * Y * Z - (C W'.a₂ * X ^ 2 + 2 * C W'.a₄ * X * Z + 3 * C W'.a₆ * Z ^ 2)

Tactic:
ring1

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

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

Tactic:
ring1

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

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

Tactic:
ring1

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

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

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
h : 3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0
⊢ 1 + 0 - (0 + (1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2)) = 0

Tactic:
ring1

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
a b : R
h :
  b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
ha : W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄) = 0
hb : 2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0
⊢ b ^ 2 + W'.a₁ * a * b + 2 * W'.a₃ * b - (W'.a₂ * a ^ 2 + 2 * W'.a₄ * a + 3 * W'.a₆) +
        (3 * 0 + a * (W'.a₁ * b - (3 * a ^ 2 + 2 * W'.a₂ * a + W'.a₄)) +
          b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
      (0 +
        (3 *
              (b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
                (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆)) +
            a * 0 +
          b * 0)) =
    0

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Nonsingular P
hPz : P z = 0
⊢ P y ≠ 0

Tactic:
intro hPy
  simp only [nonsingular_of_Z_eq_zero hPz, X_eq_zero_of_Z_eq_zero hP.left hPz, hPy, add_zero,
    sub_zero, mul_zero, zero_pow two_ne_zero, or_self, ne_self_iff_false, and_false] at hP

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
h : (g.comp f).FormallyUnramified
⊢ g.FormallyUnramified

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.FormallyUnramified.of_restrictScalars R _ _

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

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)

Tactic:
FormallyUnramified.pi_iff A,

Goal state after:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ (∀ (i : I), FormallyUnramified R (A i)) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)
Module: Mathlib.RingTheory.Etale.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ (∀ (i : I), FormallyUnramified R (A i)) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)

Tactic:
FormallySmooth.pi_iff A

Goal state after:
R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ ((∀ (i : I), FormallyUnramified R (A i)) ∧ ∀ (i : I), FormallySmooth R (A i)) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)
Module: Mathlib.RingTheory.Etale.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
⊢ FormallyUnramified R ((i : I) → A i) ∧ FormallySmooth R ((i : I) → A i) ↔
    (∀ (x : I), FormallyUnramified R (A x)) ∧ ∀ (x : I), FormallySmooth R (A x)

Tactic:
rw [FormallyUnramified.pi_iff A, FormallySmooth.pi_iff A]

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

Goal state before:
pp: case intro.mp
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
a✝ : FormallyUnramified R ((i : I) → f i)
i : I
⊢ FormallyUnramified R (f i)

Tactic:
exact FormallyUnramified.of_surjective (Pi.evalAlgHom R f i) (Function.surjective_eval i)

Goal state after: