mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ (C (W.preΨ (2 * m)) * if Even (2 * m) then W.ψ₂ else 1) * W.ψ₂ =
    (C (W.preΨ (m - 1)) * if Even (m - 1) then W.ψ₂ else 1) ^ 2 * (C (W.preΨ m) * if Even m then W.ψ₂ else 1) *
        (C (W.preΨ (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) -
      (C (W.preΨ (m - 2)) * if Even (m - 2) then W.ψ₂ else 1) * (C (W.preΨ m) * if Even m then W.ψ₂ else 1) *
        (C (W.preΨ (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) ^ 2

Tactic:
preΨ_even,

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

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ zero = a₂✝

pp: case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ some x✝ y✝ h = a₂✝

Tactic:
all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]

Goal state after:
case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0

case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ toClass (-some x✝ y✝ h) + toClass (some x✝ y✝ h) = 0
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.Δ = -W.a₂ ^ 3 * W.a₆

Tactic:
rw [Δ_of_isCharThreeJNeZeroNF]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2 = -W.a₂ ^ 3 * W.a₆
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✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
⊢ ∃ k fk,
    ∀ (j : ↥s),
      ∃ ak,
        ak ≫ f = (D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ t.app k ∧
          c.π.app k ∣_ D.map fk ⁻¹ᵁ 𝒱 j ≫ ak = (c.π.app k ⁻¹ᵁ D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ a

Tactic:
let t𝒱 (j : _) : opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj j.1.1.2.1.2 :=
    { app k := (t.app k.left).resLE _ _ <| by
        refine (Hom.preimage_mono _ (hi' _)).trans ?_
        simp only [Functor.const_obj_obj, ← Hom.comp_preimage, t.naturality,
          Functor.const_obj_map, Category.comp_id, le_refl]
      naturality {k₁ k₂} f₁₂ := by simp [Hom.resLE_comp_resLE] }

Goal state after:
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✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
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)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
𝒱' : ↥s → (D.obj i').Opens := fun x ↦ D.map fi'i ⁻¹ᵁ 𝒱 x
h𝒱'𝒰 : ∀ (j : ↥s), c.π.app i' ⁻¹ᵁ 𝒱' j = (↑↑j).1
x✝ : ∀ (j : ↥s) (k : Over i'), IsAffine ((opensDiagram D i' (𝒱' j)).obj k)
t𝒱 : (j : ↥s) → opensDiagram D i' (𝒱' j) ⟶ (Functor.const (Over i')).obj ↑↑(↑(↑↑j).2).2 :=
  fun j ↦ { app := fun k ↦ Hom.resLE (t.app k.left) (↑(↑(↑↑j).2).2) (D.map k.hom ⁻¹ᵁ 𝒱' j) ⋯, naturality := ⋯ }
⊢ ∃ k fk,
    ∀ (j : ↥s),
      ∃ ak,
        ak ≫ f = (D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ t.app k ∧
          c.π.app k ∣_ D.map fk ⁻¹ᵁ 𝒱 j ≫ ak = (c.π.app k ⁻¹ᵁ D.map fk ⁻¹ᵁ 𝒱 j).ι ≫ a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
⊢ ∃ C, (C • W).IsCharTwoNF

Tactic:
classical
  exact ⟨_, W.toCharTwoNF_spec⟩

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

Goal state before:
pp: case odd
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ (W.preΨ' (2 * (m + 2) + 1)).natDegree ≤ expDegree (2 * (m + 2) + 1) ∧
    (W.preΨ' (2 * (m + 2) + 1)).coeff (expDegree (2 * (m + 2) + 1)) = ↑(expCoeff (2 * (m + 2) + 1))

Tactic:
rw [preΨ'_odd]

Goal state after:
case odd
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
⊢ ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
          W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).natDegree ≤
      expDegree (2 * (m + 2) + 1) ∧
    ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
            W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2).coeff
        (expDegree (2 * (m + 2) + 1)) =
      ↑(expCoeff (2 * (m + 2) + 1))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P

Tactic:
by
    rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
    refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩
    contrapose! hP'
    simp only [smul_fin3_ext]
    exact ⟨by linear_combination (norm := ring1) u ^ 4 * hP'.left,
      by linear_combination (norm := ring1) u ^ 3 * hP'.right.left,
      by linear_combination (norm := ring1) u ^ 5 * hP'.right.right⟩

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

Goal state before:
pp: case succ.succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ (X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq).coeff
        (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3) -
      (W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff ((n + 1 + 1) ^ 2) =
    1

Tactic:
hd',

Goal state after:
case succ.succ.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ (X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq).coeff
        (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3) -
      (W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        (expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0) =
    1
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
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = (MvPolynomial.map ↑f) (W'⁄A).polynomialZ

Tactic:
← map_polynomialZ,

Goal state after:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
A : Type u
inst✝⁸ : CommRing A
B : Type v
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W'⁄B).polynomialZ = ((W'⁄A).map ↑f).polynomialZ
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
⊢ x * z * ↑(t * u) ≤ᵥ y * w * ↑(s * v)

Tactic:
grw [Submonoid.coe_mul, Submonoid.coe_mul,
        veq_mul_mul_mul_comm x, veq_mul_mul_mul_comm y]
      exact mul_vle_mul h₁ h₃

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

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝² x✝¹ x✝ : W.Point
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝² x✝¹ x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝² + x✝¹ + x✝) = (toAffineAddEquiv W) (x✝² + (x✝¹ + x✝))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ 0 + x✝ = x✝

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ (toAffineAddEquiv W) (0 + x✝) = (toAffineAddEquiv W) x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ x✝ + 0 = x✝

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝ + 0) = (toAffineAddEquiv W) x✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
⊢ -P + P = 0

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
P : W.Point
⊢ (toAffineAddEquiv W) (-P + P) = (toAffineAddEquiv W) 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝¹ x✝ : W.Point
⊢ x✝¹ + x✝ = x✝ + x✝¹

Tactic:
apply (toAffineAddEquiv W).injective

Goal state after:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Field F
inst✝ : Field K
W' : Jacobian R
W : Jacobian F
x✝¹ x✝ : W.Point
⊢ (toAffineAddEquiv W) (x✝¹ + x✝) = (toAffineAddEquiv W) (x✝ + x✝¹)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
⊢ IsClosed[_i.toTopologicalSpace] {x | v.restrict x < r}

Tactic:
rcases eq_or_ne r 0 with rfl | hr
  · simp
  exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v.restrict (Units.mk0 r hr))
    (isOpen_ball _ _)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ supp R ≠ ⊤

Tactic:
Ideal.ne_top_iff_one

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ 1 ∉ supp R
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3 / (P z * Q z) ^ 3

Tactic:
← negAddY_of_X_eq' hP hQ hx,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = W.negAddY P Q * (P z * Q z) ^ 3 / (P z * Q z) ^ 3
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
⊢ ∃ a, v a ≤ 1 ∧ v a = ↑(generator v)

Tactic:
set g := (valueGroup (.ofClass v)).genLTOne with hg

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
⊢ ∃ a, v a ≤ 1 ∧ v a = ↑(generator v)
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).dblX (⇑f ∘ P) = f ((W'⁄A).dblX P)

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

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v 0 = v y
h : x = 0
⊢ y = 0

Tactic:
v.map_zero

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h✝ : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : 0 = v y
h : x = 0
⊢ y = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
⊢ ContinuousAt (⇑v.restrict) x

Tactic:
have v_ne : (v.restrict x : ValueGroup₀ (.ofClass hv.v)) ≠ 0 :=
      (Valuation.ne_zero_iff _).mpr h

Goal state after:
case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : K
h : x ≠ 0
v_ne : v.restrict x ≠ 0
⊢ ContinuousAt (⇑v.restrict) x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.RightInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

pp: case refine_3
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ (x_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun y_1

pp: case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          b ↔
      a ≤ b

Tactic:
· intro ⟨a, ha⟩
      simpa [hxy.mp hx, closure_singleton_one, eq_comm] using ha

Goal state after:
case refine_3
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ (x_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.toFun y_1

case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
              map_mul' := ?refine_3 }.toFun
          a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
              map_mul' := ?refine_3 }.toFun
          b ↔
      a ≤ b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered Gˣ

Tactic:
← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered

Goal state after:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ Nonempty (Gˣ ≃*o Multiplicative ℤ)