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

Goal state before:
pp: case e'_3
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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1✝ :
  ↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    ↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op ≫ c.pt.presheaf.map (homOfLE H).op)) s

Tactic:
← Functor.map_comp

Goal state after:
case e'_3
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
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
H : c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ (c.π.app i ⁻¹ᵁ U).ι ''ᵁ ⊤
e_1✝ :
  ↑Γ(((Functor.const I).obj c.pt).obj j.left, c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤) =
    ↑(c.pt.presheaf.obj (Opposite.op (c.π.app j.left ⁻¹ᵁ (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)))
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE H).op))) s
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) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op ≫ c.pt.presheaf.map (homOfLE ⋯).op)) s =
    (ConcreteCategory.hom (c.pt.presheaf.map (homOfLE ⋯).op ≫ c.pt.presheaf.map (homOfLE ⋯).op)) s

Tactic:
← Functor.map_comp

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)
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) ⋯
x y : ↥c.pt
j : I
fjx : j ⟶ i x
fjy : j ⟶ i y
⊢ (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s =
    (ConcreteCategory.hom (c.pt.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) s
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
n : Fin 2
⊢ (CoordinateRing.basis W') n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n

Tactic:
nontriviality R
  rw [CoordinateRing.basis, Or.by_cases, dif_neg <| not_subsingleton R, Basis.reindex_apply,
    PowerBasis.basis_eq_pow, finCongr_symm_apply, Fin.val_cast]

Goal state after:
Module: Mathlib.Data.Nat.EvenOddRec

Goal state before:
pp: P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ evenOddRec h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n)

Tactic:
apply binaryRec_eq true n

Goal state after:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → true = true)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 1 + 1)) =
    preNormEDS b c d (↑m + 1 + 1) ^ 2 * preNormEDS b c d (↑m + 1 + 1 + 1) * preNormEDS b c d (↑m + 1 + 1 + 1 + 2) -
      preNormEDS b c d (↑m + 1 + 1 + 1 - 2) * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 1) ^ 2

Tactic:
show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
n : ℤ
⊢ normEDS b c d (-n) = -normEDS b c d n

Tactic:
simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]

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

Goal state before:
pp: case inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * ↑(expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1

Tactic:
push_cast [expDegree, show (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1 by ring1,
      n.not_even_two_mul_add_one, Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]

Goal state after:
case inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 1)) = (2 * ↑n + 1) ^ 2 - 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₂ = 4 * W.a₂

Tactic:
rw [b₂, a₁_of_isCharNeTwoNF]
  ring1

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
inst✝ : CharP R 3
⊢ W.Δ = -W.a₄ ^ 3

Tactic:
Δ_of_isShortNF

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : W.Δ ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
Δ_of_isShortNF

Goal state after:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsShortNF
inst✝ : CharP F 3
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isShortNF_of_char_three]

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsShortNF
inst✝ : CharP F 3
⊢ ↑W.Δ'⁻¹ * 0 ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

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

Tactic:
rw [variableChange_j, heq, ← variableChange_j E' C', j_of_isShortNF_of_char_three] at h

Goal state after:
case of_j_ne_zero.of_j_eq_zero
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharThreeJNeZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsShortNF
h : 0 ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
rcases Int.natAbs_eq_iff.mp hm with rfl | rfl

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

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) +
        (Q z ^ 6 * 0 +
            P z ^ 6 *
              (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (Q x * P z ^ 2)) -
      (0 +
        (Q z ^ 6 *
              (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
                (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) +
            P z ^ 6 * 0 +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (P x * Q z ^ 2))) =
    0

Tactic:
rw [negY]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        (Q z ^ 6 * 0 +
            P z ^ 6 *
              (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (Q x * P z ^ 2)) -
      (0 +
        (Q z ^ 6 *
              (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
                (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) +
            P z ^ 6 * 0 +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (P x * Q z ^ 2))) =
    0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_1
I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
⊢ ∀ (j : Iᵒᵖ) (x x' : (D.op ⋙ yoneda.obj X).obj j),
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι j x =
        ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι j x' →
      ∃ k f,
        (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) x'

Tactic:
intro k g₁ g₂ hg

Goal state after:
case refine_1
I : Type u
inst✝⁵ : Category.{u, u} I
S X✝ : Scheme
D✝ : I ⥤ Scheme
t : D✝ ⟶ (Functor.const I).obj S
f : X✝ ⟶ S
c✝ : Cone D✝
hc✝ : IsLimit c✝
D : I ⥤ Over S
inst✝⁴ : IsCofiltered I
inst✝³ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (Over.Hom.left (D.map f))
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i).left
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i).left
X : Over S
inst✝ : LocallyOfFinitePresentation X.hom
c : Cocone D.op
hc : IsColimit c
this✝¹ : ∀ (i : I), CompactSpace ↥((D ⋙ Over.forget S).obj i)
this✝ : ∀ (i : I), QuasiSeparatedSpace ↥((D ⋙ Over.forget S).obj i)
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom ((D ⋙ Over.forget S).map f)
k : Iᵒᵖ
g₁ g₂ : (D.op ⋙ yoneda.obj X).obj k
hg :
  ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k g₁ =
    ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).ι k g₂
⊢ ∃ k_1 f,
    (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₁ = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map f)) g₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2

Tactic:
exact (W.natDegree_coeff_Φ_ofNat n).left

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

Goal state before:
pp: e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
⊢ (toNNReal he0) m = 1 ↔ m = 1

Tactic:
by_cases hm : m = 0

Goal state after:
case pos
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1

case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
⊢ (toNNReal he0) m = 1 ↔ m = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
hP : W.NonsingularLift P
⊢ W.NonsingularLift (W.negMap P)

Tactic:
rcases P with ⟨_⟩

Goal state after:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : ¬W.Nonsingular P
⊢ toAffine W P = 0

Tactic:
by
  rw [toAffine, dif_neg <| not_and_of_not_left _ hP]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
this : ↑x ∈ posSubmonoid R
⊢ ↑x ≠ 0

Tactic:
rw [posSubmonoid_def] at this

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x : ↥(posSubmonoid R)
this : 0 <ᵥ ↑x
⊢ ↑x ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P P + -2 * P z ^ 2 * 0 -
      (0 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
rw [addX]; ring1

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
x : R
s : Set R
⊢ (∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) ↔ ∃ γ, {a | (valuation R) (a - x) < ↑γ} ⊆ s

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v).symm, ?_⟩,
    fun ⟨r, hr⟩ ↦ ⟨r.mapEquiv (orderMonoidIso v), ?_⟩⟩
  all_goals convert! hr; simp

Goal state after:
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: case refine_1
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ IsClosed {a | ((f + g).completion ⋯) a = (f.completion hf + g.completion hg) a}

pp: case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a

Tactic:
· exact isClosed_eq ((f + g).continuous_completion hfg)
      ((f.continuous_completion hf).add (g.continuous_completion hg))

Goal state after:
case refine_2
α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
hfg : Continuous (⇑f + ⇑g)
x : Completion α
⊢ ∀ (a : α), ((f + g).completion ⋯) ↑a = (f.completion hf + g.completion hg) ↑a
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (range coe')
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
      image_union] at this

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.negAddY P P = 0

Tactic:
rw [negAddY]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝² : v.Compatible
Γ' : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst✝ : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
⊢ h.orderMonoidIso ((embed w) x) = (embed v) x

Tactic:
simp only [embed, coe_mk, ZeroHom.coe_mk]

Goal state after:
R : Type u_2
Γ : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝² : v.Compatible
Γ' : Type u_4
inst✝¹ : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst✝ : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
⊢ h.orderMonoidIso (ValueGroupWithZero.lift (fun r s ↦ (restrict₀ (ofClass w)) r / (restrict₀ (ofClass w)) ↑s) ⋯ x) =
    ValueGroupWithZero.lift (fun r s ↦ (restrict₀ (ofClass v)) r / (restrict₀ (ofClass v)) ↑s) ⋯ x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

Tactic:
rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz hd]

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / (P z * Q z * d) *
        ((n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2) /
              (P z * Q z) ^ 2 /
            d ^ 2 -
          P x / P z ^ 2) +
      P y / P z ^ 3 =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
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
P : Fin 3 → A
⊢ (W'⁄B).dblU (⇑f ∘ P) = f ((W'⁄A).dblU P)

Tactic:
by
  rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]

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

Goal state before:
pp: R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Jacobian R
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
P Q : Fin 3 → A
⊢ (W'⁄B).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'⁄A).addXYZ P Q

Tactic:
by
  rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

Goal state after: