mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ (∀ (x : ↥W),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
                    f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.f
                i)) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
            f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.I₀),
      P
        ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
              f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.f
          i)

Tactic:
refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
x : ↥W
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
                f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.f
            i)

case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
      f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.I₀
⊢ P
    ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left,
          f := fun x ↦ (pullback.fst (Hom.asOverProp f S) (Hom.asOverProp (𝒰.f x) S)).left }.f
      j)
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
⊢ (∀ (x : ↥W),
      ∃ i,
        x ∈
          Set.range
            ⇑({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
                    f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.f
                i)) ∧
    ∀
      (i :
        { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
            f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.I₀),
      P
        ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
              f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.f
          i)

Tactic:
refine ⟨fun x ↦ ?_, fun j ↦ ?_⟩

Goal state after:
case refine_1
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
x : ↥W
⊢ ∃ i,
    x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
                f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.f
            i)

case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
      f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.I₀
⊢ P
    ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left,
          f := fun x ↦ (pullback.snd (Hom.asOverProp (𝒰.f x) S) (Hom.asOverProp f S)).left }.f
      j)
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
inst✝² : IsRegularEpiCategory D
F : C ⥤ D
inst✝¹ : F.PreservesEpimorphisms
inst✝ : HasPullbacks D
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ EffectiveEpi (F.map x✝¹)

Tactic:
rw [← isRegularEpi_iff_effectiveEpi]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
inst✝² : IsRegularEpiCategory D
F : C ⥤ D
inst✝¹ : F.PreservesEpimorphisms
inst✝ : HasPullbacks D
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : EffectiveEpi x✝¹
⊢ IsRegularEpi (F.map x✝¹)
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
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a b : D.obj i ⟶ X
ha : t.app i = a ≫ f
hb : t.app i = b ≫ f
hab : c.π.app i ≫ a = c.π.app i ≫ b
this✝ : ∀ (i : I), IsAffineHom (c.π.app i)
A : ExistsHomHomCompEqCompAux D t f :=
  { c := c, hc := hc, i := i, a := a, ha := ha, b := b, hb := hb, hab := hab, 𝒰S := S.affineCover, h𝒰S := ⋯,
    𝒰X := fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).X i).affineCover, h𝒰X := ⋯ }
𝒰 : (pullback.diagonalObj f).OpenCover := Pullback.diagonalCover f A.𝒰S A.𝒰X
W : (pullback.diagonalObj f).Opens := Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
k : A.𝒰D.I₀ → I
hki' : (j : A.𝒰D.I₀) → k j ⟶ A.i'
heq :
  ∀ (j : A.𝒰D.I₀),
    (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.a =
      (Precoverage.ZeroHypercover.pullback₁ (D.map (hki' j)) A.𝒰D).f j ≫ D.map (hki' j ≫ A.hii') ≫ A.b
𝒰Df : (D.obj A.i').OpenCover := A.𝒰D.finiteSubcover
h : Nonempty ↥(D.obj A.i')
O : Finset I := {A.i'} ∪ Finset.image (fun i ↦ k (Cover.idx A.𝒰D ↑i)) Finset.univ
o : 𝒰Df.I₀ := ⋯.some
ho : k (Cover.idx A.𝒰D ↑o) ∈ O
l : I
hl1 : {X : I} → X ∈ O → (l ⟶ X)
hl2 :
  ∀ {X_1 Y : I} (mX : X_1 ∈ O) (mY : Y ∈ O) {f_1 : X_1 ⟶ Y},
    ⟨X_1, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈
        Finset.image (fun i ↦ ⟨k (Cover.idx A.𝒰D ↑i), ⟨A.i', ⟨⋯, ⟨⋯, hki' (Cover.idx A.𝒰D ↑i)⟩⟩⟩⟩) Finset.univ →
      hl1 mX ≫ f_1 = hl1 mY
this : ∀ (w v : 𝒰Df.I₀), hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑w) = hl1 ⋯ ≫ hki' (Cover.idx A.𝒰D ↑v)
u : (Precoverage.ZeroHypercover.pullback₁ (D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o))) 𝒰Df).I₀
⊢ D.map (hl1 ho ≫ hki' (Cover.idx A.𝒰D ↑o)) ≫ 𝟙 (D.obj A.i') = D.map (hl1 ⋯) ≫ D.map (hki' (Cover.idx A.𝒰D ↑u))

Tactic:
rw [Category.comp_id, ← D.map_comp, this]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).b₄ = f W.b₄

Tactic:
simp only [b₄, map_a₁, map_a₃, map_a₄]
  map_simp

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
⊢ W.Equation 0 0 ↔ W.Nonsingular 0 0

Tactic:
simp only [equation_zero, nonsingular_zero, iff_self_and]
  contrapose! hΔ
  simp only [b₂, b₄, b₆, b₈, Δ, hΔ]
  ring1

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Norm

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (if i ∈ Finset.univ then (smithCoeffs b (span {f}) ⋯ i * 1) • b' i else 0) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))

Tactic:
mul_one,

Goal state after:
R : Type u_1
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬span {f} = ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf)
i : ι
⊢ (if i ∈ Finset.univ then smithCoeffs b (span {f}) ⋯ i • b' i else 0) =
    (↑(Algebra.lmul R S).toRingHom f)
      ((LinearEquiv.restrictScalars R (LinearEquiv.coord S S f hf))
        ((b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι)) (b' i)))
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: 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))
⊢ Ideal.span s₀ ≤ RingHom.ker g

Tactic:
simp only [Ideal.span_le, Set.range_subset_iff, SetLike.mem_coe, RingHom.mem_ker, map_sub,
        hσ', s₀]

Goal state after:
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))
⊢ ∀ (y : Fin n), g (MvPolynomial.C (MvPolynomial.X y)) - f (MvPolynomial.X y) = 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₂
hx : ¬x₁ = x₂
⊢ W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
    (W.slope x₁ x₂ y₁ y₂ * -(x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₁)

Tactic:
mul_neg,

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.slope x₁ x₂ y₁ y₂ * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + 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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {XClass W x₁, YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
        span {XClass W x₂, YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
span_pair_mul_span_pair

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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span
        {XClass W x₁ * XClass W x₂, XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)),
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂,
          YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
            YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} *
      span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Tactic:
by_cases hy : y₁ = W.negY x₂ y₂

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

case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (W.map f).slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ 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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span
            {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
              (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
                (mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  -XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
          span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})

Tactic:
mul_neg,

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₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
⊢ span {(mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} *
      (span
            {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))),
              (mk W) (Y - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                  XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
                -((mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) *
                    XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))} ⊔
          span {XClass W x₁} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {XClass W x₂} * span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))}) =
    YIdeal W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
      (span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)))} ⊔
        span {XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))})
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (s ^ 2 - C W.b₄ * s * u - C W.b₆ * t * u - C W.b₈ * u ^ 2).IsHomogeneous 2

pp: case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2).IsHomogeneous 2

pp: case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (t ^ 2 - C 4 * s * u).IsHomogeneous 2

Tactic:
· exact isHomogeneous_X_pow .. |>.sub CXY |>.sub CXY |>.sub CXX

Goal state after:
case «1»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (C 2 * t * s + C W.b₂ * s * u + C W.b₄ * t * u + C W.b₆ * u ^ 2).IsHomogeneous 2

case «2»
R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (t ^ 2 - C 4 * s * u).IsHomogeneous 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
mul_neg,

Goal state after:
R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
p q r s : ℤ
⊢ atomRel W (-(2 * p) + -s) (-(2 * q) + -s) (-(2 * r) + -s) (-s) = atomRel W (2 * p + s) (2 * q + s) (2 * r + s) s
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ rel W (m + 1) (m - 1) 1 0 =
    W (2 * m) * W 2 * W 1 ^ 2 - W (m - 1) ^ 2 * W m * W (m + 2) + W (m - 2) * W m * W (m + 1) ^ 2

Tactic:
rw [rel]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
m : ℤ
⊢ rel W (m + 1) m 1 0 = W (2 * m + 1) * W 1 ^ 3 - W (m + 2) * W m ^ 3 + W (m - 1) * W (m + 1) ^ 3

Tactic:
rw [rel]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ preNormEDS b c d (2 * -↑m) =
    preNormEDS b c d (-↑m - 1) ^ 2 * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 2) -
      preNormEDS b c d (-↑m - 2) * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 1) ^ 2

Tactic:
mul_neg,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ preNormEDS b c d (-(2 * ↑m)) =
    preNormEDS b c d (-↑m - 1) ^ 2 * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 2) -
      preNormEDS b c d (-↑m - 2) * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (preNormEDS (b ^ 4) c d (2 * k) * if Even k then b else b * 1) =
    preNormEDS (b ^ 4) c d (2 * k) * if Even (2 * k) then b else 1

Tactic:
mul_one,

Goal state after:
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
⊢ (preNormEDS (b ^ 4) c d (2 * k) * if Even k then b else b) =
    preNormEDS (b ^ 4) c d (2 * k) * if Even (2 * k) then b else 1