mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y✝ : Y
x✝ : y✝ ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y✝ ∈ U ∧ U ⊆ ⊤
h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
y : Y
hy : y ∈ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x
⊢ y ∈ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}

Tactic:
obtain ⟨x, (hx : f x = y), h'⟩ := exists_ne_zero_of_finsum_mem_ne_zero hy

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
hf✝ : IsSpectralMap f
w : X → R
inst✝¹ : Semiring R
W : Set Y
hW : IsOpen[inst✝²] W
c✝ : locallyFinsupp X R
inst✝ : PrespectralSpace Y
hf : IsSpectralMap f
c : locallyFinsupp X R
y✝ : Y
x✝ : y✝ ∈ univ
U : Set Y
hU : U ∈ {U | IsOpen[inst✝²] U ∧ IsCompact U} ∧ y✝ ∈ U ∧ U ⊆ ⊤
h : (U ∩ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}).Finite
y : Y
hy : y ∈ support fun z ↦ ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {z}), c x * w x
x : X
hx : f x = y
h' : c x * w x ≠ 0
⊢ y ∈ {z | (f ⁻¹' {z} ∩ support ⇑c).Nonempty}
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
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

Tactic:
let := (φRX ≫ X.presheaf.germ U x hxU).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
this : Algebra ↑R ↑(X.presheaf.stalk x) := (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU)).toAlgebra
⊢ (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H)).range
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX

Tactic:
simp only [Category.assoc]

Goal state after:
case refine_2
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
y : ↥Y
e : sX x = sY y
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : sX x ∈ ↑U
hyU : sY y ∈ U
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ ↑V
iVU : ↑V ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst✝¹ : LocallyOfFiniteType sY
x : ↥X
inst✝ : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ sX x = sY (φ (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)))

Tactic:
rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]

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

Goal state before:
pp: X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
⊢ (f.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom = (h.restrict (W₁ ⊓ W₂) ⋯ ⋯).hom

Tactic:
simp only [restrict_domain, restrict_hom, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_left hW₁l,
    Category.assoc, e₁, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_right hW₂r, ← e₂]

Goal state after:
X Y : Scheme
f g h : X.PartialMap Y
W₁ : X.Opens
hW₁ : Dense ↑W₁
hW₁l : W₁ ≤ f.domain
hW₁r : W₁ ≤ g.domain
e₁ : X.homOfLE hW₁l ≫ f.hom = X.homOfLE hW₁r ≫ g.hom
W₂ : X.Opens
hW₂ : Dense ↑W₂
hW₂l : W₂ ≤ g.domain
hW₂r : W₂ ≤ h.domain
e₂ : X.homOfLE hW₂l ≫ g.hom = X.homOfLE hW₂r ≫ h.hom
⊢ X.homOfLE ⋯ ≫ X.homOfLE hW₁r ≫ g.hom = X.homOfLE ⋯ ≫ X.homOfLE hW₂l ≫ g.hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.comp g).IsDominant

Tactic:
by
  rw [← g.toRationalMap_representative, RationalMap.comp_def]
  infer_instance

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

Goal state before:
pp: X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ (f₁.comp f₂).comp f₃.representative.toRationalMap = f₁.comp (f₂.comp f₃.representative.toRationalMap)

Tactic:
comp_def,

Goal state after:
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f₁ : X₁ ⤏ X₂
inst✝¹ : f₁.IsDominant
f₂ : X₂ ⤏ X₃
inst✝ : f₂.IsDominant
f₃ : X₃ ⤏ Y
⊢ ((f₁.comp f₂).representative.comp f₃.representative).toRationalMap =
    (f₁.representative.comp (f₂.representative.comp f₃.representative)).toRationalMap
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: 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))
⊢ ∃ k hki hkj y,
    (pullback.lift (IsOpenImmersion.lift (𝒰.f i) (𝒰.f k) ⋯) (IsOpenImmersion.lift (𝒰.f j) (𝒰.f k) ⋯) ⋯) y = x

Tactic:
by
    have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈
      (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩
    obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this
    refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
    · rw [Scheme.Hom.opensRange_comp]
      exact Set.image_subset_range _ _
    · simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]
      exact Set.image_subset_range _ _
    · apply (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).isOpenEmbedding.injective
      rw [← Scheme.Hom.comp_apply, pullback.lift_fst_assoc, IsOpenImmersion.lift_fac, hy]

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

Goal state before:
pp: S : Scheme
𝒰✝ 𝒰 : PreZeroHypercover S
K : Precoverage Scheme
inst✝ : IsEmpty ↥S
U : S.Opens
hU : IsAffineOpen U
⊢ IsCompactOpenCovered (fun x ↦ ⇑(𝒰.f x)) ↑U

Tactic:
by
    convert! IsCompactOpenCovered.empty
    simp [eq_bot_iff]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
x✝ : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ (g₁ ≫ i a₁) ≫ g a₁ ≫ f a₁ = (g₂ ≫ i a₂) ≫ g a₂ ≫ f a₂

Tactic:
simp only [Category.assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
α : Type u_2
B : C
X Y : α → C
f : (a : α) → X a ⟶ B
g : (a : α) → Y a ⟶ X a
i : (a : α) → X a ⟶ Y a
hi : ∀ (a : α), i a ≫ g a = 𝟙 (X a)
inst✝ : EffectiveEpiFamily X f
W✝ : C
e : (a : α) → Y a ⟶ W✝
w : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ g a₂ ≫ f a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z✝ : C
a₁ a₂ : α
g₁ : Z✝ ⟶ X a₁
g₂ : Z✝ ⟶ X a₂
x✝ : g₁ ≫ f a₁ = g₂ ≫ f a₂
⊢ g₁ ≫ i a₁ ≫ g a₁ ≫ f a₁ = g₂ ≫ i a₂ ≫ g a₂ ≫ f a₂
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
h : ∀ (i : 𝒰.I₀), ∃ u, pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u
⊢ ∃ u, π ≫ u = f

Tactic:
choose u hfac using h

Goal state after:
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
⊢ ∃ u, π ≫ u = f
Module: Mathlib.AlgebraicGeometry.EffectiveEpi

Goal state before:
pp: case refine_1
X Y : Scheme
inst✝³ : IsAffine X
inst✝² : IsAffine Y
π : X ⟶ Y
inst✝¹ : Surjective π
inst✝ : Flat π
this : Epi π
Z : Scheme
f : X ⟶ Z
hf : pullback.fst π π ≫ f = pullback.snd π π ≫ f
𝒰 : Y.OpenCover
u : (i : 𝒰.I₀) → 𝒰.X i ⟶ Z
hfac : ∀ (i : 𝒰.I₀), pullback.fst π (𝒰.f i) ≫ f = pullback.snd π (𝒰.f i) ≫ u i
⊢ ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ u x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ u y

Tactic:
intro i j
    have : Epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)) :=
      Flat.epi_of_flat_of_surjective _
    rw [← cancel_epi (pullback.snd π (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)),
      ← cancel_epi (pullback.congrHom rfl pullback.condition.symm).hom]
    conv_rhs =>
      simp only [pullback.congrHom_hom, limit.lift_π_assoc, PullbackCone.mk_pt, cospan_right,
      PullbackCone.mk_π_app, Category.comp_id]
    rw [← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc,
      ← pullbackLeftPullbackSndIso_inv_snd_snd, Category.assoc, ← pullback.condition_assoc,
      ← hfac i, ← pullback.condition_assoc, ← hfac j]
    simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.ColimitsOver

Goal state before:
pp: case h₀
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.499} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.499} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
m : d.gluedCocone.pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone.ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (Comma.Hom.hom ((d.cocone i).ι.app a)).left ≫ colimit.ι d.relativeGluingData.functor i ≫ m.left =
    pullback.fst (D.obj a).hom (𝒰.f i) ≫ (d.gluedCocone.ι.app a ≫ m).left

Tactic:
simp [fst_gluedCocone_ι_assoc]

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

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

Tactic:
by
  rw [c₄]
  linear_combination -8 * W.b₄ * CharP.cast_eq_zero R 3

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

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ 0 ≤ numBound k₂ D₂ 0

Tactic:
by simpa using hk

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ W'.addPolynomial x y ℓ =
    -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
          c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
          d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly

Tactic:
rw [addPolynomial, linePolynomial, polynomial, Cubic.toPoly]
  eval_simp
  C_simp
  ring1

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (C • W).Δ = ↑C.u⁻¹ ^ 12 * W.Δ

Tactic:
by
  simp only [b₂, b₄, b₆, b₈, Δ, variableChange_a₁, variableChange_a₂, variableChange_a₃,
    variableChange_a₄, variableChange_a₆]
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
hpq : p • 1 + q • (mk W') Y = 0
h : ![p, q] 0 • 1 + ![p, q] 1 • (mk W') Y = 0 → ∀ (i : Fin 2), ![p, q] i = 0
⊢ p = 0 ∧ q = 0

Tactic:
exact ⟨h hpq 0, h hpq 1⟩

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W') (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃))) +
          (mk W') (C (X - C (W'.addX x₁ x₂ ℓ)) * C (C (W'.a₁ + ℓ)))} =
    span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))), (mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)}

Tactic:
← map_add

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ span
      {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))),
        (mk W')
          (Y - C (C (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) +
            C (X - C (W'.addX x₁ x₂ ℓ)) * C (C (W'.a₁ + ℓ)))} =
    span {(mk W') (C (X - C (W'.addX x₁ x₂ ℓ))), (mk W') (C (C W'.a₁ * X + C W'.a₃) + C (C ℓ * (X - C x₁) + C y₁) + Y)}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ span {(mk W') (C (X - C x)), (mk W') (Y - C (C y)) + (mk W') (C (X - C x) * C (C (-ℓ)))} =
    span {(mk W') (C (X - C x)), (mk W') (Y - C (C ℓ * (X - C x) + C y))}

Tactic:
← map_add

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ span {(mk W') (C (X - C x)), (mk W') (Y - C (C y) + C (X - C x) * C (C (-ℓ)))} =
    span {(mk W') (C (X - C x)), (mk W') (Y - C (C ℓ * (X - C x) + C y))}
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ span
      {(mk W) (C (X - C x₂)),
        (mk W) (Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)))) +
          (mk W) (C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)))} =
    span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))}

Tactic:
← map_add

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₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
⊢ span
      {(mk W) (C (X - C x₂)),
        (mk W)
          (Y - C (C (eval x₂ (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))) +
            C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)))} =
    span {(mk W) (C (X - C x₂)), (mk W) (Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁))}
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₂) *
      (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) =
    0

Tactic:
sub_self,

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₂)
⊢ (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) * 0 = 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₁ (W.slope x₁ x₂ y₁ y₂ * (x₁ - x₁) + y₁)

Tactic:
sub_self,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a : ℤ
⊢ W a * W ((a - a).tdiv 2) = W a * W 0

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a : ℤ
⊢ W a * W (Int.tdiv 0 2) = W a * W 0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((2 * (a + b + 1)).tdiv 2) * W ((2 * a - 2 * b + (1 - 1)).tdiv 2) = W (a + b + 1) * W (a - b)

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b : ℤ
⊢ W ((2 * (a + b + 1)).tdiv 2) * W ((2 * a - 2 * b + 0).tdiv 2) = W (a + b + 1) * W (a - b)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atom W a c * atom W b a - atom W a c * atom W b a + atom W a a * atom W b c = W a * W 0 * atom W b c

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ 0 + atom W a a * atom W b c = W a * W 0 * atom W b c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ atom W a b * atom W b c - atom W a b * atom W b c + atom W a c * (W b * W 0) = W b * W 0 * atom W a c

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
a b c : ℤ
⊢ 0 + atom W a c * (W b * W 0) = W b * W 0 * atom W a c
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a |b| c d = atomRel W a b c d

Tactic:
simp_rw [atomRel, atom_abs_left odd, atom_abs_right]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c d : ℤ
⊢ atomRel W a b |c| d = atomRel W a b c d

Tactic:
simp_rw [atomRel, atom_abs_left odd, atom_abs_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) * f (atom W c d) - f (atom W a c) * f (atom W b d) + f (atom W a d) * f (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_atom

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * (p + q + s)).tdiv 2) * W ((2 * p - 2 * q + (s - s)).tdiv 2) *
          (W ((2 * (r + s)).tdiv 2) * W ((2 * r + (s - s)).tdiv 2)) -
        W ((2 * (p + r + s)).tdiv 2) * W ((2 * p - 2 * r + (s - s)).tdiv 2) *
          (W ((2 * (q + s)).tdiv 2) * W ((2 * q + (s - s)).tdiv 2)) +
      W ((2 * (p + s)).tdiv 2) * W ((2 * p + (s - s)).tdiv 2) *
        (W ((2 * (q + r + s)).tdiv 2) * W ((2 * q - 2 * r + (s - s)).tdiv 2))

Tactic:
sub_self,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
p q r s : ℤ
⊢ W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q +
      W (q + r + s) * W (q - r) * W (p + s) * W p =
    W ((2 * (p + q + s)).tdiv 2) * W ((2 * p - 2 * q + 0).tdiv 2) *
          (W ((2 * (r + s)).tdiv 2) * W ((2 * r + 0).tdiv 2)) -
        W ((2 * (p + r + s)).tdiv 2) * W ((2 * p - 2 * r + 0).tdiv 2) *
          (W ((2 * (q + s)).tdiv 2) * W ((2 * q + 0).tdiv 2)) +
      W ((2 * (p + s)).tdiv 2) * W ((2 * p + 0).tdiv 2) *
        (W ((2 * (q + r + s)).tdiv 2) * W ((2 * q - 2 * r + 0).tdiv 2))
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⟩

Goal state after:
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
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ some x✝ y✝ ⋯ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
rw [← coe_mapRingHom]
  simp [Ψ, apply_ite <| mapRingHom _]

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₂ * W.a₆

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

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

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

Tactic:
b₈_of_isCharTwoJNeZeroNF

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆