mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝² : PreirreducibleSpace ↥X
inst✝¹ : Nonempty ↥Y
f : X.PartialMap Y
inst✝ : IsDominant f.hom
g : Y ⟶ Z
⊢ f.comp (Hom.toPartialMap g) = f.compHom g

Tactic:
by
  ext1
  · simp
  · simp_rw [comp_hom, Hom.toPartialMap_domain, Hom.toPartialMap_hom, compHom_hom, topIso_hom,
      morphismRestrict_ι_assoc, f.domain.isoImage_ι_inv_ι_assoc, isoOfEq_hom]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective

Goal state before:
pp: case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f

Tactic:
refine ⟨fun x ↦ ⟨pullback.fst f f x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩

Goal state after:
case a
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
⊢ (pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x)) = (pullback.fst f f) x
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)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
g₁ g₂ : Spec (CommRingCat.of K) ⟶ X
hg : (fun g ↦ g ≫ f) g₁ = (fun g ↦ g ≫ f) g₂
e :
  (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) =
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₂.base) (IsLocalRing.closedPoint K))
h :
  CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f (g₁ (IsLocalRing.closedPoint K)) ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo g₁)) =
    CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) ≫
        (Scheme.residueFieldCongr ⋯).hom ≫ Scheme.descResidueField (Scheme.stalkClosedPointTo g₂))
⊢ ∃ (e : ((Scheme.SpecToEquivOfField K X) g₁).fst = ((Scheme.SpecToEquivOfField K X) g₂).fst),
    ((Scheme.SpecToEquivOfField K X) g₁).snd =
      (Scheme.residueFieldCongr e).hom ≫ ((Scheme.SpecToEquivOfField K X) g₂).snd

Tactic:
let x := g₁ (IsLocalRing.closedPoint K)

Goal state after:
X Y : Scheme
f : X ⟶ Y
tfae_1_iff_4 : UniversallyInjective f ↔ Surjective (pullback.diagonal f)
h_inj : Injective ⇑f
hf : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable
K : Type u
inst✝ : Field K
g₁ g₂ : Spec (CommRingCat.of K) ⟶ X
hg : (fun g ↦ g ≫ f) g₁ = (fun g ↦ g ≫ f) g₂
e :
  (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) =
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom g₂.base) (IsLocalRing.closedPoint K))
h :
  CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f (g₁ (IsLocalRing.closedPoint K)) ≫
        Scheme.descResidueField (Scheme.stalkClosedPointTo g₁)) =
    CommRingCat.Hom.hom
      (Scheme.Hom.residueFieldMap f ((TopCat.Hom.hom g₁.base) (IsLocalRing.closedPoint K)) ≫
        (Scheme.residueFieldCongr ⋯).hom ≫ Scheme.descResidueField (Scheme.stalkClosedPointTo g₂))
x : ↥X := g₁ (IsLocalRing.closedPoint K)
⊢ ∃ (e : ((Scheme.SpecToEquivOfField K X) g₁).fst = ((Scheme.SpecToEquivOfField K X) g₂).fst),
    ((Scheme.SpecToEquivOfField K X) g₁).snd =
      (Scheme.residueFieldCongr e).hom ≫ ((Scheme.SpecToEquivOfField K X) g₂).snd
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
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
z : ↥(pullback.diagonalObj f)
φ : Spec ((pullback f f).residueField z) ⟶ pullback f f := (pullback f f).fromSpecResidueField z
hφ₁ : φ ≫ pullback.fst f f = φ ≫ pullback.snd f f
⊢ φ = (φ ≫ pullback.fst f f) ≫ pullback.diagonal f

Tactic:
cat_disch

Goal state after:
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
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
z : ↥(pullback.diagonalObj f)
φ : Spec ((pullback f f).residueField z) ⟶ pullback f f := (pullback f f).fromSpecResidueField z
hφ₁ : φ ≫ pullback.fst f f = φ ≫ pullback.snd f f
⊢ ∃ a, (pullback.diagonal f) a = z

Tactic:
have hφ₂ : φ = (φ ≫ pullback.fst f f) ≫ pullback.diagonal f := by cat_disch

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
h : ∀ (K : Type u) [inst : Field K], Injective fun g ↦ g ≫ f
z : ↥(pullback.diagonalObj f)
φ : Spec ((pullback f f).residueField z) ⟶ pullback f f := (pullback f f).fromSpecResidueField z
hφ₁ : φ ≫ pullback.fst f f = φ ≫ pullback.snd f f
hφ₂ : φ = (φ ≫ pullback.fst f f) ≫ pullback.diagonal f
⊢ ∃ a, (pullback.diagonal f) a = z
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⟩
this : ⟨x, CommRingCat.ofHom σ₁.toRingHom⟩ = ⟨x, CommRingCat.ofHom σ₂.toRingHom⟩
⊢ ↑σ₁ = ↑σ₂

Tactic:
exact congr($(this).2.hom)

Goal state after:
Module: Mathlib.AlgebraicGeometry.RelativeGluing

Goal state before:
pp: S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.73} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.73} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
⊢ (𝒰.f i) ((d.natTrans.app i) ((pullback.fst (colimit.ι d.functor i) (colimit.ι d.functor j)) x)) =
    (𝒰.f j) ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x))

Tactic:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, ← ι_toBase, pullback.condition_assoc]

Goal state after:
S : Scheme
𝒰 : S.OpenCover
inst✝³ : Category.{?u.7, ?u.73} 𝒰.I₀
inst✝² : LocallyDirected 𝒰
d : RelativeGluingData 𝒰
inst✝¹ : Small.{u, ?u.73} 𝒰.I₀
inst✝ : Quiver.IsThin 𝒰.I₀
i j : d.cover.I₀
x : ↥(pullback (d.cover.f i) (d.cover.f j))
xi : ↥(d.cover.X i) := (pullback.fst (d.cover.f i) (d.cover.f j)) x
xj : ↥(d.cover.X j) := (pullback.snd (d.cover.f i) (d.cover.f j)) x
⊢ (pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j) ≫ colimit.ι d.functor j ≫ d.toBase) x =
    (𝒰.f j) ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x))
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝¹ : Module.Free R M
this✝ : Module.Finite R M
x : PrimeSpectrum R
this : zeroLocus (Set.range g.val) = zeroLocus {g.val i}
⊢ x ∈ comap (algebraMap R R[X]) '' (zeroLocus {g.val i} \ zeroLocus {f}) ↔
    x ∈
      ConstructibleSetData.toSet
        (Finset.image
          (fun j ↦
            { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))

Tactic:
mem_image_comap_zeroLocus_sdiff,

Goal state after:
case hP₂.refine_1
R✝ : Type u_2
inst✝² : CommRing R✝
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
g : InductionObj R n
i : Fin n
hi : (g.val i).Monic
hi_min : ∀ (j : Fin n), j ≠ i → g.val j = 0
R₀✝ : Type u_1
R₀ : CommRing R₀✝
inst✝ : Algebra R₀✝ R
f : R[X]
M : Type u_2 := R[X] ⧸ Ideal.span {g.val i}
this✝¹ : Module.Free R M
this✝ : Module.Finite R M
x : PrimeSpectrum R
this : zeroLocus (Set.range g.val) = zeroLocus {g.val i}
⊢ ¬IsNilpotent ((algebraMap R[X] ((R[X] ⧸ Ideal.span {g.val i}) ⊗[R] x.asIdeal.ResidueField)) f) ↔
    x ∈
      ConstructibleSetData.toSet
        (Finset.image
          (fun j ↦
            { f := (LinearMap.charpoly ((Algebra.lmul R M) ((Ideal.Quotient.mk (Ideal.span {g.val i})) f))).coeff j,
              n := 0, g := 0 })
          (Finset.range (Module.finrank R M)))
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: case none
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      none =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app none

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: case some.left
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      (some WalkingPair.left) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app (some WalkingPair.left)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: case some.right
C✝ : Type u_1
inst✝⁶ : Category.{v_1, u_1} C✝
D✝ : Type u_2
inst✝⁵ : Category.{v_2, u_2} D✝
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
X Y : C
f : X ⟶ Y
inst✝² : EffectiveEpi f
F : C ⥤ D
inst✝¹ : F.PreservesEffectiveEpis
inst✝ : PreservesLimitsOfShape WalkingCospan F
c : PullbackCone f f
hc : IsLimit c
⊢ ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                    (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (F.mapCone c)).π.app
      (some WalkingPair.right) =
    (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.one))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.left))
                      (Iso.refl ((cospan f f ⋙ F).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (F.mapCone c)).pt).hom ≫
      (PullbackCone.mk (F.map c.fst) (F.map c.snd) ⋯).π.app (some WalkingPair.right)

Tactic:
cat_disch

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

Goal state before:
pp: R : Type r
inst✝¹⁰ : CommRing R
W : Affine R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
x y : A
⊢ (W⁄B).Equation (f x) (f y) ↔ (W⁄A).Equation x y

Tactic:
rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

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₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : x₁ = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

pp: case neg
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₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

Tactic:
· subst hx
        contradiction

Goal state after:
case neg
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₁
hx₂ : W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = x₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ atom W a |b| = atom W a b

Tactic:
by
  rcases abs_choice b with h | h <;> simp only [h, atom_neg_right]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

Tactic:
simp [hn, complEDS]

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

Goal state before:
pp: case mp.some
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
⊢ some x✝ y✝ ⋯ = 0

Tactic:
· rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩
      apply (p.natDegree_norm_ne_one _).elim
      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.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₂Sq.natDegree ≤ 3

Tactic:
by
  rw [Ψ₂Sq]
  compute_degree

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

Goal state before:
pp: case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : ¬1 < (↑(m + 1)).natAbs
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Goal state after:
case neg.succ.inl
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑↑(m + 1) ≠ 0
hn : m = 0
hm : (↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq ↑(m + 1) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : ¬1 < (-↑(m + 1)).natAbs
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0

Tactic:
rw [hm, Nat.lt_add_left_iff_pos, Nat.not_lt_eq, Nat.le_zero] at hn

Goal state after:
case neg.succ.inr
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
m : ℕ
h : ↑(-↑(m + 1)) ≠ 0
hn : m = 0
hm : (-↑(m + 1)).natAbs = m + 1
⊢ W.ΨSq (-↑(m + 1)) ≠ 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
k✝ : Iᵒᵖ
g₁ g₂ : (D.op ⋙ yoneda.obj X).obj k✝
hg :
  ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k✝ g₁ =
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k✝ g₂
k : I
hik : k ⟶ Opposite.unop k✝
heq : (D ⋙ Over.forget S).map hik ≫ Over.Hom.left g₁ = (D ⋙ Over.forget S).map hik ≫ Over.Hom.left g₂
⊢ (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map hik.op)) g₁ =
    (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map hik.op)) g₂

Tactic:
cat_disch

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
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✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
k : I
u : (D ⋙ Over.forget S).obj k ⟶ X.left
h : ((Over.forget S).mapCone c.unop).π.app k ≫ u = Over.Hom.left g
h' : u ≫ X.hom = { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }.app k
⊢ (D.op ⋙ yoneda.obj X).descColimitType ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c))
      ((D.op ⋙ yoneda.obj X).ιColimitType (Opposite.op k) (Over.homMk u ⋯)) =
    g

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ unzero hxy = unzero hx * unzero hy

Tactic:
← WithZero.coe_inj,

Goal state after:
case neg.e_a.e_6
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * y = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(unzero hxy) = ↑(unzero hx * unzero hy)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ ⟦W.neg P⟧ = ⟦![1, 1, 0]⟧

Tactic:
neg_of_Z_eq_zero hP hPz,

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblY P = (P x ^ 2) ^ 3

Tactic:
rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -(P x ^ 2) ^ 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * 0 ^ 3 = (P x ^ 2) ^ 3
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)

Tactic:
exact hk

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

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) * ↑(B k) ⊆ ↑(B i)

Tactic:
exact hk

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

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x ↦ x₀ * x) ⁻¹' ↑(B i)

Tactic:
exact hk

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

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x ↦ x * x₀) ⁻¹' ↑(B i)

Tactic:
exact hk

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

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
⊢ W.add P Q =
    addZ P Q •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]

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

Goal state before:
pp: case h.right
ι : 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
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)

Tactic:
exact hk

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

Goal state before:
pp: case pos
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_eq_zero hP hPz,

Goal state after:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ toAffine W (-(P y / P x) • ![1, 1, 0]) = -toAffine W P