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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
⊢ g₁ ≫ f = g₂ ≫ f

Tactic:
simp only [g₁, g₂, Scheme.SpecToEquivOfField_symm_apply, AlgHom.toRingHom_eq_coe,
        Category.assoc, ← f.SpecMap_residueFieldMap_fromSpecResidueField x, ← Spec.map_comp_assoc]

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
⊢ Spec.map (Scheme.Hom.residueFieldMap f x ≫ CommRingCat.ofHom ↑σ₁) ≫ Y.fromSpecResidueField (f x) =
    Spec.map (Scheme.Hom.residueFieldMap f x ≫ CommRingCat.ofHom ↑σ₂) ≫ Y.fromSpecResidueField (f x)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case e_a
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
a : ↑(Y.residueField (f x))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x ≫ CommRingCat.ofHom ↑σ₁)) a =
    (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x ≫ CommRingCat.ofHom ↑σ₂)) a

Tactic:
simp only [CommRingCat.hom_comp, RingHom.comp_apply]

Goal state after:
case e_a
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
tfae_3_to_2 :
  (Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable) →
    ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
tfae_2_to_4 : (∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f) → Surjective (pullback.diagonal f)
hf : Function.Surjective ⇑(pullback.diagonal f)
this : UniversallyInjective f
x : ↥X
algInst✝ : Algebra ↑(Y.residueField (f x)) ↑(X.residueField x) :=
  (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).toAlgebra
σ₁ σ₂ : Field.Emb ↑(Y.residueField (f x)) ↑(X.residueField x)
g₁ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩
g₂ : Spec (CommRingCat.of (AlgebraicClosure ↑(X.residueField x))) ⟶ X :=
  (Scheme.SpecToEquivOfField (AlgebraicClosure ↑(X.residueField x)) X).symm ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
a : ↑(Y.residueField (f x))
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom ↑σ₁)) ((CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)) a) =
    (CommRingCat.Hom.hom (CommRingCat.ofHom ↑σ₂)) ((CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)) a)
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
apply (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).isOpenEmbedding.injective

Goal state after:
case refine_3
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
      ((pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y) =
    (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝¹ : Category.{u_2, u_1} 𝒰.I₀
inst✝ : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ IsOpenImmersion (d.functor.map hij)

Tactic:
apply MorphismProperty.of_isPullback (d.equifibered hij).flip
  infer_instance

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

Tactic:
obtain ⟨xk, rfl, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      simp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply, ← ι_toBase, Scheme.Hom.comp_apply, ← h]
      simp [← Scheme.Hom.comp_apply]

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 k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
xk : ↥(d.functor.obj k)
h2 : (d.natTrans.app k) xk = uk
x✝ : (colimit.ι d.functor j) ((d.functor.map fj) xk) ∈ ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i)
h✝ : (trans 𝒰 fj) uk = (d.natTrans.app j) ((d.functor.map fj) xk)
h : (𝒰.f i) ((trans 𝒰 fi) uk) = d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk))
⊢ (colimit.ι d.functor j) ((d.functor.map fj) xk) ∈ Set.range ⇑(colimit.ι d.functor i)
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
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ False

Tactic:
refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)

Goal state after:
I : Type u
inst✝³ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
A : ExistsHomHomCompEqCompAux D t f
W : (pullback.diagonalObj f).Opens := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
h :
  ∀ (i' : I) (hii' : i' ⟶ A.i),
    (⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑(Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X))ᶜ).Nonempty
Z : (i' : I) → (i' ⟶ A.i) → Set ↥(D.obj i') := fun i' hii' ↦ ⇑(D.map hii' ≫ pullback.lift A.a A.b ⋯) ⁻¹' (↑W)ᶜ
hZ : ∀ (i' : I) (hii' : i' ⟶ A.i), IsClosed (Z i' hii')
s : ↥A.c.pt
hs : ∀ (i : I) (hij : i ⟶ A.i), (A.c.π.app i) s ∈ Z i hij
⊢ (D.map (𝟙 A.i) ≫ pullback.lift A.a A.b ⋯) ((A.c.π.app A.i) s) ∈ Set.range ⇑(pullback.diagonal f)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₄ = -W.a₄ + W.a₁ * W.a₃

Tactic:
rw [b₄]
  linear_combination W.a₄ * CharP.cast_eq_zero R 3

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₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (if x₁ = x₂ then
      if y₁ = W.negY x₂ y₂ then 0 else (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
    else (y₁ - y₂) / (x₁ - x₂)) =
    (y₁ - y₂) / (x₁ - x₂)

Tactic:
if_neg hx

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (y₁ - y₂) / (x₁ - x₂) = (y₁ - y₂) / (x₁ - x₂)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ (CoordinateRing.basis W') 1 = (mk W') Y

Tactic:
by
  simpa only [basis_apply] using! pow_one _

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 : W'.CoordinateRing
⊢ (mk (W'.map f)) (Polynomial.map (mapRingHom f) (C x)) * (map W' f) y = Polynomial.map f x • (map W' f) y

Tactic:
map_C,

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

Tactic:
hq,

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
⊢ 0 • 1 + 0 • (mk W') Y = 0
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
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.LeftInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
by rintro (_ | _) <;> rfl

Goal state after:
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
p : W'.Point → Prop
p0 : p Point.zero
⊢ Function.RightInverse (fun P ↦ Option.casesOn P ⟨Point.zero, p0⟩ fun xy ↦ ⟨Point.some (↑xy).1 (↑xy).2 ⋯, ⋯⟩) fun x ↦
    match x with
    | ⟨Point.zero, property⟩ => none
    | ⟨Point.some x y h, ph⟩ => some ⟨(x, y), ⋯⟩

Tactic:
by rintro (_ | _) <;> rfl

Goal state after:
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
⊢ ∀ (a : W.Point), 0 + a = a

Tactic:
by rintro (_ | _) <;> rfl

Goal state after:
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
⊢ ∀ (a : W.Point), a + 0 = a

Tactic:
by rintro (_ | _) <;> rfl

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ ((Algebra.norm F[X]) p).natDegree = 1

Tactic:
rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
        ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
        (CoordinateRing.quotientXYIdealEquiv h).toLinearEquiv.finrank_eq, Module.finrank_self]

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

Goal state before:
pp: R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P

Tactic:
by
  ext n; fin_cases n <;> rfl

Goal state after:
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, Units.val_inv_eq_inv_val,
      Units.val_mk0, inv_pow, inv_mul_eq_div, hu]
    simp [field]

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

Goal state before:
pp: case of_j_ne_zero.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ C, C • E = E'

Tactic:
rw [← variableChange_j E C, ← variableChange_j E' C'] at heq

Goal state after:
case of_j_ne_zero.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
heq : (C • E).j = (C' • E').j
inst✝ : (C' • E').IsCharThreeJNeZeroNF
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case of_j_ne_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
have h := (C • E).j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three

Goal state after:
case of_j_ne_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsShortNF
h : (C • E).j ≠ 0
⊢ ∃ C, C • E = E'
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
this : ∀ (E' : WeierstrassCurve F) [inst : E'.IsElliptic], E.j = E'.j → E'.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E'.IsShortNF
C : VariableChange F
heq : E.j = (C • E').j
hE' : (C • E').IsShortNF
C' : VariableChange F
hC : C' • E = C • E'
⊢ (C⁻¹ * C') • E = E'

Tactic:
rw [mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : U ∈ 𝓝 1
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U

Tactic:
rw [nhds_prod_eq, Filter.mem_prod_iff] at hU

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : ∃ t₁ ∈ 𝓝 1.1, ∃ t₂ ∈ 𝓝 1.2, t₁ ×ˢ t₂ ⊆ U
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦W.neg P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧

Tactic:
neg_of_Z_ne_zero hPz,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧ =
    ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * Q z ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z

Tactic:
hQz

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * 0 ^ 2 - Q x * P z ^ 2 = -(Q x * P z) * P z
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (W.neg P) = -toAffine W P

Tactic:
neg_of_Z_ne_zero hPz,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ toAffine W (P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]) = -toAffine W P
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
hQz

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * 0 + P x ^ 2 * Q x * 0 ^ 2 - W'.a₁ * P x * Q y * P z ^ 2 * 0 -
                  W'.a₁ * P y * Q x * P z * 0 ^ 2 +
                2 * W'.a₂ * P x * Q x * P z ^ 2 * 0 ^ 2 -
              W'.a₃ * Q y * P z ^ 4 * 0 -
            W'.a₃ * P y * P z * 0 ^ 4 +
          W'.a₄ * Q x * P z ^ 4 * 0 ^ 2 +
        W'.a₄ * P x * P z ^ 2 * 0 ^ 4 +
      2 * W'.a₆ * P z ^ 4 * 0 ^ 4 =
    (-(Q x * P z)) ^ 2 * P x
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case mk.mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk b₁ b₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : ValueGroupWithZero.mk b₁ b₂ ≤ ValueGroupWithZero.mk c₁ c₂
⊢ ValueGroupWithZero.mk a₁ a₂ ≤ ValueGroupWithZero.mk c₁ c₂

Tactic:
ValueGroupWithZero.mk_le_mk

Goal state after:
case mk.mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ a₁ * ↑c₂ ≤ᵥ c₁ * ↑a₂
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v y = v x} ∈ 𝓝 x

Tactic:
by
  rw [mem_nhds]
  have h' : v.restrict x ≠ 0 := by simp [h]
  use Units.mk0 _ h'
  rw [Units.val_mk0]
  intro y y_in
  exact Valuation.map_eq_of_sub_lt _ (v.restrict_lt_iff.mp y_in)

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝¹ * ↑y✝ ≤ᵥ x✝ * ↑y✝¹ ∨ ValueGroupWithZero.mk x✝ y✝ ≤ ValueGroupWithZero.mk x✝¹ y✝¹

Tactic:
ValueGroupWithZero.mk_le_mk

Goal state after:
case mk.mk
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ x✝¹ * ↑y✝ ≤ᵥ x✝ * ↑y✝¹ ∨ x✝ * ↑y✝¹ ≤ᵥ x✝¹ * ↑y✝
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk 0 1 ≤ ValueGroupWithZero.mk x y

Tactic:
ValueGroupWithZero.mk_le_mk

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
⊢ 0 * ↑y ≤ᵥ x * ↑1