mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₁
R : Type u_2
inst✝ : CommRing R
n : ℕ
⊢ ∀ (R : Type u_2) [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
    Statement R₀ R n { val := 0 }

Tactic:
intro R _ R₀ _ _ f
    refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.coeff j, 0, 0⟩, ?_, ?_⟩
    · convert! image_comap_C_basicOpen f
      · simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_sdiff]
        congr 1
        rw [← Set.univ_subset_iff]
        rintro x _ _ ⟨_, rfl⟩
        exact zero_mem x.asIdeal
      · suffices Set.range f.coeff = ⋃ i < f.natDegree + 2, {f.coeff i} by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_sdiff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]
        trans f.coeff '' (Set.Iio (f.natDegree + 2))
        · refine ((Set.image_subset_range _ _).antisymm ?_).symm
          rintro _ ⟨i, rfl⟩
          by_cases! hi : i ≤ f.natDegree
          · exact ⟨i, hi.trans_lt (by simp), rfl⟩
          · exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩
        · ext; simp [eq_comm]
    · simp

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ ∃ κ,
    ∃ (_ : Finite κ),
      ∃ a V, (∀ (i : κ), V i ∈ B (a i)) ∧ (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ i, f (a i) '' ↑(V i) = U

Tactic:
choose Us UsB hUsf hUs using fun i : s ↦ (hB i.1).exists_finite_of_isCompact (hc i i.2)

Goal state after:
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
B : (i : ι) → Set (Opens (X i))
hB : ∀ (i : ι), IsBasis (B i)
hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier
U : Set S
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hunion : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
Us : (i : ↑s) → Set (Opens (X ↑i))
UsB : ∀ (i : ↑s), Us i ⊆ B ↑i
hUsf : ∀ (i : ↑s), (Us i).Finite
hUs : ∀ (i : ↑s), V ↑i ⋯ = sSup (Us i)
⊢ ∃ κ,
    ∃ (_ : Finite κ),
      ∃ a V, (∀ (i : κ), V i ∈ B (a i)) ∧ (∀ (i : κ), IsCompact (V i).carrier) ∧ ⋃ i, f (a i) '' ↑(V i) = U
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝³ : (i : ι) → TopologicalSpace (X i)
inst✝² : ∀ (i : ι), PrespectralSpace (X i)
inst✝¹ : TopologicalSpace S
σ : Type u_4
Y : σ → Type u_5
inst✝ : (i : σ) → TopologicalSpace (Y i)
g : (i : σ) → Y i → S
a : σ → ι
t : (i : σ) → Y i → X (a i)
ht : ∀ (i : σ), Continuous (t i)
hge : ∀ (i : σ), g i = f (a i) ∘ t i
hf : ∀ (i : ι), Continuous (f i)
U : Set S
ho : IsOpen U
hU : IsCompactOpenCovered g U
⊢ IsCompactOpenCovered f U

Tactic:
by
  rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique] at hU ⊢
  let p : (Σ i, Y i) → (Σ i, X i) := Sigma.map a t
  have hcomp : (fun x ↦ f x.1 x.2) ∘ p = fun x ↦ g x.1 x.2 := by
    ext
    simp [hge, p, Sigma.map]
  have hp : Continuous p := Continuous.sigma_map ht
  have hf : Continuous (fun p : Σ i, X i ↦ f p.1 p.2) := by simp [hf]
  obtain ⟨V, hV, heq⟩ := hU
  obtain ⟨K, hK, ho, hVK, hKU⟩ := PrespectralSpace.exists_isCompact_and_isOpen_between
      (hV.image hp) (ho.preimage hf) <| by
    simp [← heq, ← Set.preimage_comp, hcomp, Set.subset_preimage_image]
  refine ⟨⟨K, ho⟩, hK, subset_antisymm (by simpa) ?_⟩
  rw [← heq, ← hcomp, Set.image_comp]
  exact subset_trans (Set.image_mono hVK) (by simp)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.QuasiCompact

Goal state before:
pp: S : Scheme
𝒰 : PreZeroHypercover S
inst✝ : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact ↑U
⊢ ∃ n f V, (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ i, ⇑(𝒰.f (f i)) '' ↑(V i) = ↑U

Tactic:
obtain ⟨n, a, V, ha, heq⟩ := (isCompactOpenCovered_of_isCompact 𝒰 hU).exists_mem_of_isBasis
    (fun i ↦ (𝒰.X i).isBasis_affineOpens) (fun _ _ h ↦ h.isCompact)

Goal state after:
S : Scheme
𝒰 : PreZeroHypercover S
inst✝ : QuasiCompactCover 𝒰
U : S.Opens
hU : IsCompact ↑U
n : ℕ
a : Fin n → 𝒰.I₀
V : (i : Fin n) → TopologicalSpace.Opens ↥(𝒰.X (a i))
ha : ∀ (i : Fin n), V i ∈ (𝒰.X (a i)).affineOpens
heq : ⋃ i, ⇑(𝒰.f (a i)) '' ↑(V i) = ↑U
⊢ ∃ n f V, (∀ (i : Fin n), IsAffineOpen (V i)) ∧ ⋃ i, ⇑(𝒰.f (f i)) '' ↑(V i) = ↑U
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : D
ε : (a : α) → e.functor.obj (X a) ⟶ W✝
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
m : e.functor.obj B ⟶ W✝
hm : ∀ (a : α), e.functor.map (π a) ≫ m = ε a
this : e.unit.app B ≫ e.inverse.map m = EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯
⊢ m = e.functor.map (EffectiveEpiFamily.desc X π (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) ⋯) ≫ e.counit.app W✝

Tactic:
· simp [← this]

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ ↑(W.map f).Δ' = f ↑W.Δ'

Tactic:
rw [coe_Δ', map_Δ, coe_Δ']

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0

Tactic:
obtain ⟨j, f, hf⟩ := exists_appTop_map_eq_zero_of_isLimit _ _
    (isLimitOpensCone D c hc i U) (i := .mk (𝟙 i))
    ((D.obj i).presheaf.map (homOfLE (show (D.map (𝟙 _) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U by simp)).op s) (by
      rw [← map_zero (c.pt.presheaf.map (homOfLE
        (show (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ c.π.app i ⁻¹ᵁ U by simp)).op).hom, ← hs]
      dsimp [Scheme.Opens.toScheme_presheaf_obj]
      rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
      congr! 2
      simp [Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE])

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)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = 0
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
⊢ (W⁄B).polynomialY = Polynomial.map (mapRingHom ↑f) (W⁄A).polynomialY

Tactic:
← map_polynomialY,

Goal state after:
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
⊢ (W⁄B).polynomialY = ((W⁄A).map ↑f).polynomialY
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case e'_3
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
⊢ Ideal.span s₀ = RingHom.ker g

Tactic:
refine H.antisymm fun p hp ↦ ?_

Goal state after:
case e'_3
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
p : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)
hp : p ∈ RingHom.ker g
⊢ p ∈ Ideal.span s₀
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
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) * 0 = 0

Tactic:
mul_zero

Goal state after:
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ 0 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
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₂
⊢ -((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) +
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) *
            (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) *
          (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) ≠
    0

Tactic:
simp only [neg_ne_zero, sub_self, mul_zero, add_zero]

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₂
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) ≠ 0
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
i : ↥c.pt → I
U : (x : ↥c.pt) → (D.obj (i x)).Opens
hU : ∀ (x : ↥c.pt), IsAffineOpen (U x)
hxU : ∀ (x : ↥c.pt), (c.π.app (i x)) x ∈ U x
t : (x : ↥c.pt) → ↑Γ(D.obj (i x), U x)
ht : ∀ (x : ↥c.pt), (ConcreteCategory.hom (Scheme.Hom.app (c.π.app (i x)) (U x))) (t x) = (s |_ c.π.app (i x) ⁻¹ᵁ U x) ⋯
j : ↥c.pt → ↥c.pt → I
fjx : (x y : ↥c.pt) → j x y ⟶ i x
fjy : (x y : ↥c.pt) → j x y ⟶ i y
hj :
  ∀ (x y : ↥c.pt),
    ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjx x y)) (U x))) (t x) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯ =
      ((ConcreteCategory.hom (Scheme.Hom.app (D.map (fjy x y)) (U y))) (t y) |_
          (D.map (fjx x y) ⁻¹ᵁ U x ⊓ D.map (fjy x y) ⁻¹ᵁ U y))
        ⋯
σ : Finset ↥c.pt
hσ : ⋃ x ∈ σ, (c.π.app (i x) ⁻¹ᵁ U x).carrier = ⊤
σi : ↥c.pt → ↥c.pt
hσiσ : ∀ (x : ↥c.pt), σi x ∈ σ
hσi : ∀ (x : ↥c.pt), x ∈ (c.π.app (i (σi x)) ⁻¹ᵁ U (σi x)).carrier
S : Finset I := Finset.image i σ ∪ Finset.image₂ j σ σ
hiS : ∀ {x : ↥c.pt}, x ∈ σ → i x ∈ S
hjS : ∀ {x y : ↥c.pt}, x ∈ σ → y ∈ σ → j x y ∈ S
k : I
fk : {X : I} → X ∈ S → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ S) (mY : Y ∈ S) {f : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈
        Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑x, ⟨⋯, ⟨⋯, fjx ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach ∪
          Finset.image₂ (fun x y ↦ ⟨j ↑x ↑y, ⟨i ↑y, ⟨⋯, ⟨⋯, fjy ↑x ↑y⟩⟩⟩⟩) σ.attach σ.attach →
      fk mX ≫ f = fk mY
hk₁ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjx x y = fk ⋯
hk₂ : ∀ {x y : ↥c.pt} (hx : x ∈ σ) (hy : y ∈ σ), fk ⋯ ≫ fjy x y = fk ⋯
k' : I
fk'k : k' ⟶ k
hk' : D.map fk'k ⁻¹ᵁ ⨆ x, ⨆ (hx : x ∈ σ), D.map (fk ⋯) ⁻¹ᵁ U x = ⊤
this :
  ∀ (x : (i_1 : ↥σ) → ((D.obj k').presheaf ⋙ forget CommRingCat).obj (Opposite.op (D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U ↑i_1))),
    Presieve.Arrows.Compatible ((D.obj k').presheaf ⋙ forget CommRingCat) (fun x ↦ homOfLE ⋯) x →
      ∃! t,
        ∀ (i_1 : ↥σ), (ConcreteCategory.hom (((D.obj k').presheaf ⋙ forget CommRingCat).map (homOfLE ⋯).op)) t = x i_1
t₀ : ((D.obj k').presheaf ⋙ forget CommRingCat).obj (Opposite.op ⊤)
ht₀ :
  ∀ (i_1 : ↥σ),
    (ConcreteCategory.hom (((D.obj k').presheaf ⋙ forget CommRingCat).map (homOfLE ⋯).op)) t₀ =
      (ConcreteCategory.hom (Scheme.Hom.app (D.map (fk'k ≫ fk ⋯)) (U ↑i_1))) (t ↑i_1)
y : ↥c.pt
hy : y ∈ ⊤
⊢ c.π.app (i (σi y)) ⁻¹ᵁ U (σi y) ≤ c.π.app k' ⁻¹ᵁ D.map (fk'k ≫ fk ⋯) ⁻¹ᵁ U (σi y)

Tactic:
rw [← Scheme.Hom.comp_preimage, Cone.w]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
by
  simp_rw [atomRel, atom_neg_right]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a b c d : ℤ
⊢ f (atom W a b * atom W c d - atom W a c * atom W b d) + f (atom W a d * atom W b c) =
    atom (⇑f ∘ W) a b * atom (⇑f ∘ W) c d - atom (⇑f ∘ W) a c * atom (⇑f ∘ W) b d +
      atom (⇑f ∘ W) a d * atom (⇑f ∘ W) b c

Tactic:
map_sub,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
a b c d : ℤ
⊢ f (atom W a b * atom W c d) - f (atom W a c * atom W b d) + f (atom W a d * atom W b c) =
    atom (⇑f ∘ W) a b * atom (⇑f ∘ W) c d - atom (⇑f ∘ W) a c * atom (⇑f ∘ W) b d +
      atom (⇑f ∘ W) a d * atom (⇑f ∘ W) b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
p q r s : ℤ
⊢ f (W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q) +
      f (W (q + r + s) * W (q - r) * W (p + s) * W p) =
    (⇑f ∘ W) (p + q + s) * (⇑f ∘ W) (p - q) * (⇑f ∘ W) (r + s) * (⇑f ∘ W) r -
        (⇑f ∘ W) (p + r + s) * (⇑f ∘ W) (p - r) * (⇑f ∘ W) (q + s) * (⇑f ∘ W) q +
      (⇑f ∘ W) (q + r + s) * (⇑f ∘ W) (q - r) * (⇑f ∘ W) (p + s) * (⇑f ∘ W) p

Tactic:
map_sub,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
W : ℤ → R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
p q r s : ℤ
⊢ f (W (p + q + s) * W (p - q) * W (r + s) * W r) - f (W (p + r + s) * W (p - r) * W (q + s) * W q) +
      f (W (q + r + s) * W (q - r) * W (p + s) * W p) =
    (⇑f ∘ W) (p + q + s) * (⇑f ∘ W) (p - q) * (⇑f ∘ W) (r + s) * (⇑f ∘ W) r -
        (⇑f ∘ W) (p + r + s) * (⇑f ∘ W) (p - r) * (⇑f ∘ W) (q + s) * (⇑f ∘ W) q +
      (⇑f ∘ W) (q + r + s) * (⇑f ∘ W) (q - r) * (⇑f ∘ W) (p + s) * (⇑f ∘ W) p
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₂ y₂ h✝ = 0 ↔ -some x₂ y₂ h✝ = 0

Tactic:
neg_eq_iff_eq_neg,

Goal state after:
case zero.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₂ y₂ h✝ = 0 ↔ some x₂ y₂ h✝ = -0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 2 = X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈

Tactic:
rw [show 2 = ((1 : ℕ) + 1 : ℤ) by rfl, Φ_ofNat, preΨ'_two, if_neg Nat.not_even_one, Ψ₂Sq,
    preΨ'_three, preΨ'_one, if_neg Nat.not_even_one, Ψ₃]
  C_simp
  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 * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)) =
    (mk W) (C (X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq))

Tactic:
map_sub,

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

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

Tactic:
compute_degree!

Goal state after:
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:
by
  rw [leadingCoeff, W.natDegree_Ψ₂Sq h, coeff_Ψ₂Sq]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3

Tactic:
compute_degree!

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
            C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
          C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff
      6 =
    2

Tactic:
compute_degree!

Goal state after:
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:
b₂_of_isCharThreeJNeZeroNF

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ = W.a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case even.left
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 := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m := ⋯
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (2 * (m + 3))).natDegree ≤ expDegree (2 * (m + 3))

Tactic:
nth_rw 1 [preΨ'_even, ← max_self <| expDegree _, (expDegree_rec m).1.1, (expDegree_rec m).1.2]
      exact natDegree_sub_le_of_le (dm (dm (dp h₂.1) h₃.1) h₅.1) (dm (dm h₁.1 h₃.1) (dp h₄.1))

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

Goal state before:
pp: case inr
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
heq : E.j = E'.j
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
this : ∀ (E : WeierstrassCurve F) [inst : E.IsElliptic], E.j = E'.j → E.IsShortNF → ∃ C, C • E = E'
h✝ : ¬E.IsShortNF
⊢ ∃ C, C • E = E'

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
heq : E.j = E'.j
h✝ : E.IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
· obtain ⟨C, hE⟩ := E.exists_variableChange_isShortNF
    rw [← variableChange_j E C] at heq
    obtain ⟨C', hC⟩ := this _ heq hE
    exact ⟨C' * C, by rwa [mul_smul]⟩

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
heq : E.j = E'.j
h✝ : E.IsShortNF
⊢ ∃ C, C • E = E'