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

Goal state before:
pp: case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom = (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom

Tactic:
← cancel_epi (Scheme.Hom.isoImage _ _).hom

Goal state after:
case refine_2
X Y : Scheme
inst✝¹ : IrreducibleSpace ↥X
x : ↥X
inst✝ : X.IsGermInjectiveAt x
f g : X.PartialMap Y
hxf : x ∈ f.domain
hxg : x ∈ g.domain
H : f.fromSpecStalkOfMem hxf = g.fromSpecStalkOfMem hxg
hdense : Dense (↑f.domain ⊓ ↑g.domain)
this : (↑(f.domain ⊓ g.domain)).IsGermInjectiveAt ⟨x, ⋯⟩
U : (↑(f.domain ⊓ g.domain)).Opens
hxU : ⟨x, ⋯⟩ ∈ U
e : U.ι ≫ X.homOfLE ⋯ ≫ f.hom = U.ι ≫ X.homOfLE ⋯ ≫ g.hom
⊢ (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (f.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom =
    (Hom.isoImage (f.domain ⊓ g.domain).ι U).hom ≫ (g.restrict ((f.domain ⊓ g.domain).ι ''ᵁ U) ⋯ ⋯).hom
Module: Mathlib.AlgebraicGeometry.Birational.Birational

Goal state before:
pp: X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
f : X.PartialIso Y
hf : IsOver sX sY f
⊢ IsOver sY sX f.symm

Tactic:
simpa [IsOver, ← cancel_epi f.iso.hom] using Eq.symm hf

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

Goal state before:
pp: case hxy
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := ⋯
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update c.val j (c.val j %ₘ c.val i) j).degree < (c.val j).degree

Tactic:
simpa using (degree_modByMonic_lt _ hi).trans_le hle

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

Goal state before:
pp: case u
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑(C.u⁻¹ * C.u) = ↑1

pp: case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0

pp: case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

pp: case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0

Tactic:
· exact C.u.inv_mul

Goal state after:
case r
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ -C.r * ↑C.u⁻¹ ^ 2 * ↑C.u ^ 2 + C.r = 0

case s
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ ↑C.u * (-C.s * ↑C.u⁻¹) + C.s = 0

case t
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ (C.r * C.s - C.t) * ↑C.u⁻¹ ^ 3 * ↑C.u ^ 3 + -C.r * ↑C.u⁻¹ ^ 2 * C.s * ↑C.u ^ 2 + C.t = 0
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case zero.refine_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ comap MvPolynomial.C '' S.toSet = (ConstructibleSetData.map (isEmptyRingEquiv R (Fin 0)).toRingHom S).toSet

Tactic:
ConstructibleSetData.toSet_map

Goal state after:
case zero.refine_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)
⊢ comap MvPolynomial.C '' S.toSet = comap (isEmptyRingEquiv R (Fin 0)).toRingHom ⁻¹' S.toSet
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: case a₂
R : Type u
inst✝ : CommRing R
W✝ : WeierstrassCurve R
C✝ C C' : VariableChange R
W : WeierstrassCurve R
⊢ (↑C.u⁻¹ * ↑C'.u⁻¹) ^ 2 *
      (W.a₂ - (↑C'.u * C.s + C'.s) * W.a₁ + 3 * (C.r * ↑C'.u ^ 2 + C'.r) - (↑C'.u * C.s + C'.s) ^ 2) =
    ↑C.u⁻¹ ^ 2 *
      (↑C'.u⁻¹ ^ 2 * (W.a₂ - C'.s * W.a₁ + 3 * C'.r - C'.s ^ 2) - C.s * (↑C'.u⁻¹ * (W.a₁ + 2 * C'.s)) + 3 * C.r -
        C.s ^ 2)

Tactic:
linear_combination
        C.s * (-C'.s * 2 - W.a₁) * C.u⁻¹ ^ 2 * ↑C'.u⁻¹ * C'.u.inv_mul
          + (C.r * 3 - C.s ^ 2) * C.u⁻¹ ^ 2 * pow_mul_pow_eq_one 2 C'.u.inv_mul

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

Goal state before:
pp: S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ finrank F (S ⧸ span {f}) = ∑ i, (smithCoeffs b (span {f}) h i).natDegree

Tactic:
finrank_quotient_eq_sum F h b

Goal state after:
S : Type u_2
ι : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
F : Type u_4
inst✝⁴ : Field F
inst✝³ : Algebra F[X] S
inst✝² : Finite ι
inst✝¹ : Algebra F S
inst✝ : IsScalarTower F F[X] S
b : Basis ι F[X] S
f : S
hf : f ≠ 0
this : Fintype ι
h : ¬span {f} = ⊥
⊢ ∑ i, finrank F (F[X] ⧸ span {smithCoeffs b (span {f}) h i}) = ∑ i, (smithCoeffs b (span {f}) h i).natDegree
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case C
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
q : MvPolynomial (Fin m) R
⊢ ∃ q₁ q₂, q₁ ∈ Ideal.span s₀ ∧ MvPolynomial.C q = (commAlgEquiv R (Fin n) (Fin m)).symm (q₁ + σ q₂)

Tactic:
exact ⟨0, q, by simp, (commAlgEquiv _ _ _).injective <|
          by simp [commAlgEquiv_C, σ]⟩

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ 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₂} ⊔
        (span {XClass W x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} ⊔
          (span {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * XClass W x₂} ⊔
            span
              {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₂))})

Tactic:
sup_rw,

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₂} ⊔
            span
              {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 x₁ * YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))} ⊔
        span {YClass W (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * 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.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
atom_abs_left odd

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ (c.π.app l) x ∈ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r)

Tactic:
change x ∈ c.π.app l ⁻¹ᵁ (D.obj l).basicOpen _

Goal state after:
case refine_2
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)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
l : I
flk : l ⟶ k
hl :
  D.map flk ⁻¹ᵁ (D.obj k).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map fkj))) r) ≤ D.map flk ⁻¹ᵁ D.map fki ⁻¹ᵁ U
⊢ x ∈ c.π.app l ⁻¹ᵁ (D.obj l).basicOpen ((ConcreteCategory.hom (Hom.appTop (D.map (flk ≫ fkj)))) r)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ ((p • (CoordinateRing.basis W').repr 1) 0 + (q • (CoordinateRing.basis W').repr ((mk W') Y)) 0) *
        (((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • (CoordinateRing.basis W').repr 1) 1 +
          ((p - q * (C W'.a₁ * X + C W'.a₃)) • (CoordinateRing.basis W').repr ((mk W') Y)) 1) -
      (((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • (CoordinateRing.basis W').repr 1) 0 +
          ((p - q * (C W'.a₁ * X + C W'.a₃)) • (CoordinateRing.basis W').repr ((mk W') Y)) 0) *
        ((p • (CoordinateRing.basis W').repr 1) 1 + (q • (CoordinateRing.basis W').repr ((mk W') Y)) 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
Finsupp.smul_apply,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (p • ((CoordinateRing.basis W').repr 1) 0 + q • ((CoordinateRing.basis W').repr ((mk W') Y)) 0) *
        ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • ((CoordinateRing.basis W').repr 1) 1 +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • ((CoordinateRing.basis W').repr ((mk W') Y)) 1) -
      ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • ((CoordinateRing.basis W').repr 1) 0 +
          (p - q * (C W'.a₁ * X + C W'.a₃)) • ((CoordinateRing.basis W').repr ((mk W') Y)) 0) *
        (p • ((CoordinateRing.basis W').repr 1) 1 + q • ((CoordinateRing.basis W').repr ((mk W') Y)) 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.none
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
hp' : p.degree = none
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • none) (2 • q.degree + 3)

pp: case neg.some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hp' : p.degree = some dp
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • q.degree + 3)

Tactic:
· exact (hp hp').elim

Goal state after:
case neg.some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hdp : (p ^ 2).degree = 2 • p.degree
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ p.degree + q.degree + 1
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • q.degree + 3
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hp' : p.degree = some dp
⊢ (p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree =
    max (2 • some dp) (2 • q.degree + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_3.e'_4
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dq + 3 = (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree

Tactic:
rw [hdq]

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

Goal state before:
pp: case neg.some.some.inl.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree

Tactic:
rw [hdq]

Goal state after:
case neg.some.some.inl.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inl.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ some dp + some dq + 1 < (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree

Tactic:
rw [hdq]

Goal state after:
case neg.some.some.inl.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ some dp + some dq + 1 < 2 • some dq + 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inl.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree

Tactic:
rw [hdq]

Goal state after:
case neg.some.some.inl.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dp ≤ dq + 1
⊢ 2 • some dp < 2 • some dq + 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 0 = 1

Tactic:
by
  simp [Φ]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 1 = X

Tactic:
by
  simp [Φ]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
by
  rw [Δ_of_isCharNeTwoNF, a₂_of_isShortNF]
  ring1

Goal state after:
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
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).ψ n = Polynomial.map (mapRingHom ↑f) ((W⁄A).ψ n)

Tactic:
← map_ψ,

Goal state after:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).ψ n = ((W⁄A).map ↑f).ψ n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ W.j ≠ 0

Tactic:
j_of_isCharTwoJNeZeroNF_of_char_two,

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP F 2
⊢ 1 / W.a₆ ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
ha₁ : W.a₁ = 0
⊢ (W.toCharTwoJEqZeroNF • W).IsCharTwoJEqZeroNF

Tactic:
by
  constructor
  · simp [toCharTwoJEqZeroNF, ha₁, variableChange_a₁]
  · simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]
    linear_combination 2 * W.a₂ * CharP.cast_eq_zero R 2

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

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

Tactic:
j_of_isCharTwoJNeZeroNF_of_char_two,

Goal state after:
case of_j_ne_zero.of_j_ne_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJNeZeroNF
heq : 1 / (C • E).a₆ = 1 / (C' • E').a₆
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ W.ΨSq n ≠ 0

Tactic:
by_cases hn : 1 < n.natAbs

Goal state after:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : 1 < n.natAbs
⊢ W.ΨSq n ≠ 0

case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
hn : ¬1 < n.natAbs
⊢ W.ΨSq n ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.dblU P = -3 * P x ^ 2

Tactic:
rw [dblU_eq, hPz]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.a₁ * P y * 0 - (3 * P x ^ 2 + 2 * W'.a₂ * P x * 0 ^ 2 + W'.a₄ * 0 ^ 4) = -3 * P x ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W'.map f).polynomialY = (MvPolynomial.map f) W'.polynomialY

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Goal state after: