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

Goal state before:
pp: case inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 0 ∧ g.degree = 3
⊢ 1 < (f + g).degree

pp: case inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 1 ∧ g.degree = 2
⊢ 1 < (f + g).degree

pp: case inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

pp: case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree

Tactic:
iterate 2 rw [degree_add_eq_right_of_degree_lt] <;> simp only [h] <;> decide

Goal state after:
case inr.inr.inl
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 2 ∧ g.degree = 1
⊢ 1 < (f + g).degree

case inr.inr.inr
R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
h✝ : ¬Irreducible W.polynomial
f g : R[X]
h0 : 3 = f.degree + g.degree
h1 : { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly.degree = (f + g).degree
h : f.degree = 3 ∧ g.degree = 0
⊢ 1 < (f + g).degree
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 0)

Tactic:
by
  rw [Nonsingular, equation_zero, evalEval_polynomialX_zero, neg_ne_zero, evalEval_polynomialY_zero,
    or_comm]

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) = y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)

Tactic:
ring

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case refine_2
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT₁ : comap Polynomial.C '' S'.toSet = T.toSet
hT₂ :
  ∀ C ∈ T,
    C.n ≤ S'.degBound ∧
      ∀ (i : Fin C.n),
        C.g i ∈ (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) ^ S'.degBound ^ S'.degBound
N : ℕ := (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d))
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
a : Fin C.n
⊢ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B) ^ S'.degBound ^ S'.degBound ≤
    Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))

Tactic:
rw [degreesLE_nsmul, Submodule.restrictScalars_pow Nat.pow_self_pos.ne']
      refine pow_le_pow_right' ?_ (Nat.pow_self_mono hS')
      simp

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case mul_X.refine_2
R : Type u_2
inst✝ : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf : ∀ (i : Fin n), (f (MvPolynomial.X i)).degrees ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg : g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))) = ↑f
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' : ∀ (x : MvPolynomial (Fin m) R), g (σ x) = x
hg' : Surjective ⇑g
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun x ↦
      match x with
      | { f := fk, n := k, g := gk } =>
        { f := σ fk, n := k + n,
          g := fun s ↦
            Sum.elim (⇑σ ∘ gk) (fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i)))
              (finSumFinEquiv.symm s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun i ↦ MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))
H : Ideal.span s₀ ≤ RingHom.ker g
i : Fin n
q₁ : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
q₂ : MvPolynomial (Fin m) R
hq₁ : q₁ ∈ Ideal.span s₀
⊢ (q₁ + σ q₂) * MvPolynomial.C (MvPolynomial.X i) =
    q₁ * MvPolynomial.C (MvPolynomial.X i) + σ q₂ * (MvPolynomial.C (MvPolynomial.X i) - σ (f (MvPolynomial.X i))) +
      σ q₂ * σ (f (MvPolynomial.X i))

Tactic:
ring

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + y₁)

Tactic:
hx₁,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx₁ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₁
⊢ W.Nonsingular x₁ (W.slope x₁ x₂ y₁ y₂ * (x₁ - x₁) + y₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ eval₂ (mapRingHom f) (C (f ℓ) * (X - C (f x)) + C (f y)) W'.polynomial =
    Polynomial.map f (eval (linePolynomial x y ℓ) W'.polynomial)

Tactic:
← coe_mapRingHom,

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ eval₂ (mapRingHom f) (C (f ℓ) * (X - C (f x)) + C (f y)) W'.polynomial =
    (mapRingHom f) (eval (linePolynomial x y ℓ) W'.polynomial)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
⊢ ∃ i f, IsAffineOpen ((D.obj i).basicOpen f) ∧ (c.π.app i) x ∈ (D.obj i).basicOpen f

Tactic:
obtain ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ ∃ i f, IsAffineOpen ((D.obj i).basicOpen f) ∧ (c.π.app i) x ∈ (D.obj i).basicOpen f
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * s ^ 2 +
              C (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * s * t +
            C (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * s * u +
          C (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * t ^ 2 +
        C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t * u).IsHomogeneous
    2

Tactic:
exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * s ^ 2 +
              C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * s * t +
            C (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * s * u +
          C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * t ^ 2 +
        C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * t * u).IsHomogeneous
    2

Tactic:
exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «5»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C (-(12 * W.b₂ * W.b₆)) * s ^ 2 + C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * s * t + C (-(12 * W.b₆ ^ 2)) * s * u +
          C (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * t ^ 2 +
        C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * t * u).IsHomogeneous
    2

Tactic:
exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial

Tactic:
ψ₂,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) = W.toAffine.polynomialY ^ 2 - 4 * W.toAffine.polynomial
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝² x✝¹ x✝ : W.Point
⊢ toClass (x✝² + x✝¹ + x✝) = toClass (x✝² + (x✝¹ + x✝))

Tactic:
by simp only [map_add, add_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ c.π.app i ≫ e.app i ≫ g = a

Tactic:
← Category.assoc

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (c.π.app i ≫ e.app i) ≫ g = a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ W.Ψ₂Sq.leadingCoeff = 4

Tactic:
rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).ψ₂ = Polynomial.map (mapRingHom f) W.ψ₂

Tactic:
ψ₂,

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).toAffine.polynomialY = Polynomial.map (mapRingHom f) W.toAffine.polynomialY
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.b₆ = W.a₆

Tactic:
by
  rw [b₆_of_isCharThreeJNeZeroNF]
  linear_combination W.a₆ * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: n : ℕ
⊢ ↑(expCoeff n) = if Even n then ↑n / 2 else ↑n

Tactic:
by
  rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;> simp [expCoeff, n.not_even_two_mul_add_one]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialY / P z ^ 3 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialY

Tactic:
linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    W.a₁ * P x / P z ^ 2 * div_self hPz + W.a₃ * div_self (pow_ne_zero 3 hPz)

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
j₁ j₂ : ↥s
x✝ : ∀ (x : Over k), CompactSpace ↥((opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).obj x)
l : I
flk : (𝟭 I).obj l ⟶ (Functor.fromPUnit k).obj { as := PUnit.unit }
flk' : { left := l, right := { as := PUnit.unit }, hom := flk }.left ⟶ (Over.mk (𝟙 k)).left
h :
  (𝟭 I).map flk' ≫ (Over.mk (𝟙 k)).hom =
    { left := l, right := { as := PUnit.unit }, hom := flk }.hom ≫ (Functor.fromPUnit k).map { down := { down := ⋯ } }
e :
  (opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).map { left := flk', right := { down := { down := ⋯ } }, w := h } ≫
      (D.obj (Over.mk (𝟙 k)).left).homOfLE ⋯ ≫ ak j₁ =
    (opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).map { left := flk', right := { down := { down := ⋯ } }, w := h } ≫
      (D.obj (Over.mk (𝟙 k)).left).homOfLE ⋯ ≫ ak j₂
⊢ flk = flk'

Tactic:
simpa using! h.symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : ↑n ≠ 0
⊢ 0 < (W.preΨ n).natDegree

Tactic:
induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat] using! W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, natDegree_neg]
        using! ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : 0 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False

Tactic:
zero_eq_mul,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E'.a₄ ^ 3 = 0 ∨ E.a₆ ^ 2 = 0
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ ↑1 = 1

Tactic:
coe_one

Goal state after:
case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : unzero hm = 1
⊢ 1 = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.addX P (W'.neg P), W'.negAddY P (W'.neg P), addZ P (W'.neg P)] = -W'.dblZ P ^ 3

Tactic:
addX_neg hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negY ![W'.dblZ P ^ 2, W'.negAddY P (W'.neg P), addZ P (W'.neg P)] = -W'.dblZ P ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), addZ P (W'.neg P)] = -W'.dblZ P • ![1, 1, 0]

Tactic:
addX_neg hP,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![W'.dblZ P ^ 2, W'.addY P (W'.neg P), addZ P (W'.neg P)] = -W'.dblZ P • ![1, 1, 0]
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ {U | ∃ i, U = ↑(B i)} → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
rintro m₀ _ ⟨i, rfl⟩
    exact hB.smul m₀ i

Goal state after:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
← and_forall_ne (0 : Γ₀)

Goal state after:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ ((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
⊢ (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | (valuation R) x < ↑γ}

Tactic:
by
  convert! hasBasis_nhds (0 : R)
  rw [sub_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClosed[_i.toTopologicalSpace] {x | v.restrict x < r}

Tactic:
exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _ _)

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x y : R
⊢ x =ᵥ y ↔ v x = v y

Tactic:
veq_def,

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x y : R
⊢ x ≤ᵥ y ∧ y ≤ᵥ x ↔ v x = v y
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ (↑a + ↑b) * ↑c = ↑a * ↑c + ↑b * ↑c

Tactic:
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul]

Goal state after: