mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))

Tactic:
wlog hT : ∃ R, T = Spec R generalizing T

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    (∃ R, T = Spec R) → topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
hT : ¬∃ R, T = Spec R
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))

X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
hT : ∃ R, T = Spec R
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace
⊢ Mono
    (PresheafedSpace.Hom.stalkMap
      (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)

Tactic:
apply ConcreteCategory.mono_of_injective

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : Flat f
inst✝ : Surjective f
x : ↑↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace
⊢ Function.Injective
    ⇑(ConcreteCategory.hom
        (PresheafedSpace.Hom.stalkMap
          (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x))
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (SpecIso n S).hom ≫ (Arrow.mk (Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))).hom =
    (Arrow.mk (map n (Spec.map φ))).hom ≫ (SpecIso n R).hom

Tactic:
have := (SpecIso n R).inv_hom_id; simp [map_SpecMap]

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = {x | D x = 0}ᶜ ∩ U
⊢ IsDiscrete ({x | D x = 0}ᶜ ∩ U)

Tactic:
apply isDiscrete_of_codiscreteWithin

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
this : D.support = {x | D x = 0}ᶜ ∩ U
⊢ {x | D x = 0}ᶜᶜ ∈ codiscreteWithin U
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : DecidableEq X
D : locallyFinsupp X ℤ
h : 0 < D
⊢ ∃ z, D z ≠ 0

Tactic:
by simpa [D.ext_iff] using! (ne_of_lt h).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range

Tactic:
let := φRX.hom.toAlgebra

Goal state after:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this✝ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset ↑A
hs : Algebra.adjoin ↑R ↑s = ⊤
W : ↑A → TopologicalSpace.Opens ↥X
hxW : ∀ (t : ↑A), x ∈ W t
f : (t : ↑A) → ToType (X.presheaf.obj (Opposite.op (W t)))
hf : ∀ (t : ↑A), (ConcreteCategory.hom (X.presheaf.germ (W t) x ⋯)) (f t) = (ConcreteCategory.hom φ) t
H : x ∈ s.inf W ⊓ U
this : Algebra ↑R ↑Γ(X, U) := (CommRingCat.Hom.hom φRX).toAlgebra
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
hX : IrreducibleSpace ↥X
inst✝ : IrreducibleSpace ↥Y
⊢ f (genericPoint ↥X) = genericPoint ↥Y

Tactic:
apply ((genericPoint_spec Y).eq _).symm
  convert! (genericPoint_spec X).image f.continuous
  symm
  rw [← Set.univ_subset_iff]
  convert! subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _
  · rw [Set.univ_inter, Set.image_univ]
  · apply PreirreducibleSpace.isPreirreducible_univ (X := Y)
  · exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.FunctionField

Goal state before:
pp: X : Scheme
inst✝¹ : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst✝ : Nonempty ↥↑U
⊢ (Set.univ ∩ ↑U).Nonempty

Tactic:
simpa using ‹Nonempty U›

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.RationalMap

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
dsimp [RationalMap.toPartialMap]

Goal state after:
X Y : Scheme
inst✝¹ : IsReduced X
inst✝ : Y.IsSeparated
f : X.PartialMap Y
⊢ X.homOfLE ⋯ ≫
      Cover.glueMorphisms f.toRationalMap.openCoverDomain (fun x ↦ (X.isoOfEq ⋯).inv ≫ (Exists.choose ⋯).hom) ⋯ =
    f.hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ ((f.comp g).comp h).hom = (X₁.isoOfEq ⋯).hom ≫ (f.comp (g.comp h)).hom

Tactic:
· dsimp
    simp_rw [morphismRestrict_comp, morphismRestrict_ι_image_ι_isoImage_inv_assoc,
      Hom.comp_preimage, Category.assoc]
    conv_lhs => rw [← Category.assoc]
    conv_rhs => rw [← Category.assoc, ← Category.assoc, ← Category.assoc]
    congr 1
    simp [← cancel_mono (Opens.ι _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: case refine_1
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i : 𝒰.I₀
ui : ↥(𝒰.X i)
j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
h : (𝒰.f i) ui = d.toBase ((colimit.ι d.functor j) xj)
⊢ (colimit.ι d.functor j) xj ∈ Set.range ⇑(colimit.ι d.functor i)

Tactic:
obtain ⟨k, fi, fj, uk, rfl, h⟩ := 𝒰.exists_of_f_eq_f ui (d.natTrans.app j xj) <| by
      simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]

Goal state after:
case refine_1
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{u_2, u_1} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, u_1} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : 𝒰.I₀
xj : ↥(d.functor.obj j)
x✝ : (colimit.ι d.functor j) xj ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) xj
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) xj)
⊢ (colimit.ι d.functor j) xj ∈ Set.range ⇑(colimit.ι d.functor i)
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: case h
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ (⋯.isoSpec.hom ≫ ⋯.isoSpec.inv ≫ (V { down := idx s }.down).ι ≫ 𝒰.f (f { down := idx s }.down)) ⟨x s, ⋯⟩ = s

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
case h
P : MorphismProperty Scheme
S : Scheme
𝒰 : Scheme.Cover (Scheme.precoverage P) S
inst✝² : P.RespectsLeft IsOpenImmersion
inst✝¹ : CompactSpace ↥S
inst✝ : QuasiCompactCover 𝒰.toPreZeroHypercover
n : ℕ
f : Fin n → 𝒰.I₀
V : (i : Fin n) → (𝒰.X (f i)).Opens
hV : ∀ (i : Fin n), IsAffineOpen (V i)
idx : ↥S → Fin n
x : (x : ↥S) → ↥(𝒰.X (f (idx x)))
hmem : ∀ (x_1 : ↥S), x x_1 ∈ V (idx x_1)
hx : ∀ (x_1 : ↥S), (𝒰.f (f (idx x_1))) (x x_1) = x_1
s : ↥S
⊢ ((V { down := idx s }.down).ι ≫ 𝒰.f (f { down := idx s }.down)) ⟨x s, ⋯⟩ = s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomial = 0 ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0

Tactic:
evalEval_polynomial

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0 ↔
    y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ Y - W'.polynomialY = W'.negPolynomial

Tactic:
by
  rw [polynomialY, negPolynomial]
  C_simp
  ring1

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₁ y₂ : F
hy : ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃
⊢ W.slope x₂ x₂ y₁ y₂ = (3 * x₂ ^ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃))

Tactic:
by
  simp [slope, hy]

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ (map W' f) ((mk W') x) = (mk (W'.map f)) (Polynomial.map (mapRingHom f) x)

Tactic:
by
  rw [map, AdjoinRoot.lift_mk, ← eval₂_map]
  exact AdjoinRoot.aeval_eq <| x.map <| mapRingHom f

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
⊢ p • 1 + q • (mk W') Y = 0

Tactic:
Polynomial.map_eq_zero_iff hf

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (W'.map f)) Y = 0
hp : p = 0
hq : q = 0
⊢ p • 1 + q • (mk W') Y = 0
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 x₁ (0 + y₁)

Tactic:
zero_add

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₁ y₁
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (W.map f).slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_X_ne fun h => hx <| f.injective h, slope_of_X_ne hx]

Goal state after:
case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (f y₁ - f y₂) / (f x₁ - f x₂) = f ((y₁ - y₂) / (x₁ - x₂))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c d : ℤ
parity : d % 2 = a % 2 ∧ d % 2 = b % 2 ∧ d % 2 = c % 2
⊢ atomRel W ((a + b + c + d) / 2 - d) ((a + b + c + d) / 2 - c) ((a + b + c + d) / 2 - b) ((a + b + c + d) / 2 - a) =
    atomRel W a b c d

Tactic:
simp_rw [add_assoc <| a + b, atomRel, atom, sub_add_sub_comm, ← two_mul]
  repeat rw [Int.mul_ediv_cancel'] <;> grind

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

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C ((y₁ - W.negY x₁ y₁) ^ 2)) *
      (C (C y⁻¹) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃)))) =
    C (C ((y₁ - W.negY x₁ y₁) ^ 2)) *
      (1 + C (C (y⁻¹ * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
          C (C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + b₂ W) * X + C (4 * x₁ ^ 2 + b₂ W * x₁ + 2 * b₄ W))) * C (X - C x₁) +
        0 * C (X - C x₁))

Tactic:
simp only [y, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hxy]

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) =
    C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
          C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
        C
          ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * b₂ W) * X + C (1 * 4 * x₁ ^ 2 + 1 * b₂ W * x₁ + 1 * 2 * b₄ W)) *
            (X - C x₁)) +
      C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some
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
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ - -some x✝ y✝ h✝ = some x✝ y✝ h✝

Tactic:
simp only [neg_some, negY_negY]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ((X * 1 ^ 2 * if Even 1 then 1 else W.Ψ₂Sq) - W.preΨ' (1 + 2) * W.preΨ' 1 * if Even 1 then W.Ψ₂Sq else 1) =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
if_neg Nat.not_even_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * 1 ^ 2 * W.Ψ₂Sq - W.preΨ' (1 + 2) * W.preΨ' 1 * if Even 1 then W.Ψ₂Sq else 1) =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      W.Ψ₃ * 1 * if Even 1 then C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆ else 1) =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
if_neg Nat.not_even_one,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) - W.Ψ₃ * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 4 = X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
rw [show 4 = ((3 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_four, if_neg <| by decide,
    show 3 + 2 = 2 * 2 + 1 by rfl, preΨ'_odd, preΨ'_four, preΨ'_two, if_pos Even.zero, preΨ'_one,
    preΨ'_three, if_pos Even.zero, if_neg <| by decide]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (W.Ψ n) ^ 2 - (mk W) (W.Ψ (n + 1)) * (mk W) (W.Ψ (n - 1)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))

Tactic:
mk_Ψ_sq,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (C X) * (mk W) (C (W.ΨSq n)) - (mk W) (W.Ψ (n + 1)) * (mk W) (W.Ψ (n - 1)) =
    (mk W) (C X) * (mk W) (C (W.ΨSq n)) -
      (mk W) (C (W.preΨ (n + 1))) * (mk W) (C (W.preΨ (n - 1))) * (mk W) (C (if Even n then 1 else W.Ψ₂Sq))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.c₄ = W.b₂ ^ 2

Tactic:
rw [c₄, b₄_of_isCharTwoJNeZeroNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ ^ 2 - 24 * 0 = W.b₂ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case h.a₁
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := 0, s := 0, t := 0 } • E).a₁ = E'.a₁

Tactic:
simp_rw [variableChange_a₁, a₁_of_isCharThreeJNeZeroNF]
    ring1

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

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

Tactic:
linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 6 * hP

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.negY P = -P y

Tactic:
by
  rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]

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

Goal state before:
pp: case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ (W.Φ (↑(n + 1) + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ (↑(n + 1) + 1)).coeff ((n + 1 + 1) ^ 2) = 1

Tactic:
Φ_ofNat

Goal state after:
case succ.succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
          W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      (n + 1 + 1) ^ 2 ∧
    ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
            W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        ((n + 1 + 1) ^ 2) =
      1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (-W.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      (P z * (P y - W.negY P)) ^ 3 =
    W.toAffine.negAddY (P x / P z ^ 2) (P x / P z ^ 2) (P y / P z ^ 3) (-W.dblU P / (P z * (P y - W.negY P)))

Tactic:
toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (-W.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      (P z * (P y - W.negY P)) ^ 3 =
    (-W.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      (P z * (P y - W.negY P)) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P x * Q z) • Q

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := hB.topology
⊢ ∀ x ∈ (B i).carrier, (B i).carrier ∈ 𝓝 x

Tactic:
intro a a_in

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := hB.topology
a : A
a_in : a ∈ (B i).carrier
⊢ (B i).carrier ∈ 𝓝 a