mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.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' : Affine 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
x₁ y₁ x₂ ℓ : A
⊢ (W'⁄B).addY (↑f x₁) (↑f x₂) (↑f y₁) (↑f ℓ) = ↑f ((W'⁄A).addY x₁ x₂ y₁ ℓ)

Tactic:
← map_addY,

Goal state after:
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' : Affine 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
x₁ y₁ x₂ ℓ : A
⊢ (W'⁄B).addY (↑f x₁) (↑f x₂) (↑f y₁) (↑f ℓ) = ((W'⁄A).map ↑f).addY (↑f x₁) (↑f x₂) (↑f y₁) (↑f ℓ)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
simp_rw [atomRel, atom_mul_atom odd a b, mul_comm <| atom W b a, sub_self, zero_add, atom_same]

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
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:
induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _ | m
    iterate 3 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, show (m : ℤ) + 1 + 1 + 1 = m + 1 + 2 by rfl,
      Int.add_sub_cancel]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_even ..
  | neg ih m =>
    simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]
    ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case intro.refine_1
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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k : I
fkj : k ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
⊢ IsOpenCover fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x

pp: case intro.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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k✝ : I
fkj : k✝ ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
k : J
⊢ U k = c.π.app k✝ ⁻¹ᵁ (fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x) k

Tactic:
· refine top_le_iff.mp (e.symm.trans_le ?_)
    simp_rw [Hom.preimage_iSup, ← Hom.comp_preimage, ← D.map_comp]
    simp

Goal state after:
case intro.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)
J : Type u_1
inst✝ : Finite J
U : J → c.pt.Opens
hU : IsOpenCover U
hU' : ∀ (i : J), IsAffineOpen (U i)
j : J → I
V : (k : J) → (D.obj (j k)).Opens
hV : ∀ (k : J), IsAffineOpen (V k)
hVU : ∀ (k : J), c.π.app (j k) ⁻¹ᵁ V k = U k
val✝ : Fintype J
i : I
fi : (k : J) → i ⟶ j k
k✝ : I
fkj : k✝ ⟶ i
e : D.map fkj ⁻¹ᵁ ⨆ k, D.map (fi k) ⁻¹ᵁ V k = ⊤
k : J
⊢ U k = c.π.app k✝ ⁻¹ᵁ (fun x ↦ D.map (fkj ≫ fi x) ⁻¹ᵁ V x) k
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 < 2 • some dq + 3

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Goal state after:
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 < 2 • some dq + 3

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

Goal state after:
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 < 2 • some dq + 3

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

Goal state before:
pp: case neg.some.some.inr.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 : dq + 1 < dp
⊢ some dp + some dq + 1 < 2 • some dp

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

Goal state before:
pp: case neg.some.some.inr.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 : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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

Goal state before:
pp: case neg.some.some.inr.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 : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

Tactic:
exact WithBot.coe_lt_coe.mpr <| by dsimp; linarith only [hpq]

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
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
by
  simp only [add_def, add, dif_neg hxy]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
by
  rw [c₄, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF]
  ring1

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

Goal state before:
pp: case of_j_eq_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 2
heq : E.j = E'.j
C : VariableChange F
inst✝¹ : (C • E).IsCharTwoJEqZeroNF
C' : VariableChange F
inst✝ : (C' • E').IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨C'', hC⟩ := exists_variableChange_of_char_two_of_j_eq_zero (C • E) (C' • E')
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
have : NeZero (2 : F) := NeZero.mk <| by
    rw [show (2 : F) = -1 by linear_combination CharP.cast_eq_zero F 3, neg_ne_zero]
    exact one_ne_zero

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = P y - (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3)

Tactic:
eval_polynomialY

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3 = P y - (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3)
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_2
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)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
k : I
u : (D ⋙ Over.forget S).obj k ⟶ X.left
h : ((Over.forget S).mapCone c.unop).π.app k ≫ u = Over.Hom.left g
h' : u ≫ X.hom = { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }.app k
⊢ ∃ a,
    (D.op ⋙ yoneda.obj X).descColimitType ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)) a =
      g

Tactic:
use Functor.ιColimitType _ (.op k) (Over.homMk u)

Goal state after:
case h
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)
g : ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c)).pt
k : I
u : (D ⋙ Over.forget S).obj k ⟶ X.left
h : ((Over.forget S).mapCone c.unop).π.app k ≫ u = Over.Hom.left g
h' : u ≫ X.hom = { app := fun x ↦ (D.obj x).hom, naturality := ⋯ }.app k
⊢ (D.op ⋙ yoneda.obj X).descColimitType ((D.op ⋙ yoneda.obj X).coconeTypesEquiv.symm ((yoneda.obj X).mapCocone c))
      ((D.op ⋙ yoneda.obj X).ιColimitType (Opposite.op k) (Over.homMk u ⋯)) =
    g
Module: Mathlib.Topology.Algebra.Nonarchimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : U ∈ 𝓝 1
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U

Tactic:
nhds_prod_eq,

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : NonarchimedeanGroup G
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : U ∈ 𝓝 1.1 ×ˢ 𝓝 1.2
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
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
hPz : P z = 0
⊢ W.negMap ⟦P⟧ = ⟦![1, 1, 0]⟧

Tactic:
negMap_eq,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ ⟦W.neg P⟧ = ⟦![1, 1, 0]⟧
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negMap ⟦P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧

Tactic:
negMap_eq,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ⟦W.neg P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)

Tactic:
rintro x ⟨y, y_in, z, z_in, rfl⟩
      exact (B i).add_mem y_in z_in

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u ^ 4) ^ 2 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = u ^ 4 • W'.dblXYZ P

Tactic:
dblY_smul,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u ^ 4) ^ 2 * W'.dblX P, (u ^ 4) ^ 3 * W'.dblY P, W'.dblZ (u • P)] = u ^ 4 • W'.dblXYZ P
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)

Tactic:
rintro x ⟨y, y_in, z, z_in, rfl⟩
      exact (B i).add_mem y_in z_in

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

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦W.add P Q⟧ = ⟦P⟧

Tactic:
add_of_Z_eq_zero_right hQ.left hPz hQz,

Goal state after:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P✝ : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
⊢ ⟦-(Q x * P z) • P⟧ = ⟦P⟧
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: case mp
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
refine ⟨h', ?_⟩

Goal state after:
case mp
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F

Tactic:
refine ⟨h', ?_⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := B.uniformSpace
this✝ : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ F ×ˢ F ≤ uniformity G
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : Q z = 0
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q

Tactic:
add_of_Z_eq_zero_right hQ.left hPz hQz,

Goal state after:
case pos
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : Q z = 0
⊢ toAffine W (-(Q x * P z) • P) = toAffine W P + toAffine W Q
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case inl
K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
h : ∀ (x : K), v x ≠ 0 → ↑r < v x
H : Units.mk0 (v x) hx < 1
k : ℕ
hk : Units.mk0 (v x) hx ^ k < r
⊢ v x = 1

Tactic:
specialize h (x ^ k) (by simp [hx])

Goal state after:
case inl
K : Type u
inst✝² : DivisionRing K
Γ₀ : Type v
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : v x ≠ 0
r : Γ₀ˣ
hr : ↑r ≠ 0
H : Units.mk0 (v x) hx < 1
k : ℕ
h : ↑r < v (x ^ k)
hk : Units.mk0 (v x) hx ^ k < r
⊢ v x = 1
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.2 < a.1} ∈ 𝓝 (a, b)

Tactic:
nhds_prod_eq,

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.2 < a.1} ∈ 𝓝 a ×ˢ 𝓝 b
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 0)

Tactic:
nhds_prod_eq,

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 0 ×ˢ 𝓝 y) (𝓝 0)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
nhds_prod_eq,

Goal state after:
case inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 x ×ˢ 𝓝 y) (𝓝 ((x, y).1 * (x, y).2))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
t s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * ↑s <ᵥ y * ↑t

Tactic:
rw [lt_iff_not_ge, ← not_vle, mk_le_mk]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addY P Q = (-(Q x * P z)) ^ 3 * P y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_right hQ hQz, negY, addX_of_Z_eq_zero_right hQz,
    addZ_of_Z_eq_zero_right hQz]
  ring1

Goal state after:
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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
⊢ v ↑π.val ^ m = v ↑r

Tactic:
hvr_def

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = Units.mk0 (v ↑r) hr₀
⊢ v ↑π.val ^ m = v ↑r
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 Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
⊢ ∃ n u, ↑r = ↑(π.val ^ n) * ↑↑u

Tactic:
have hr₀ : v r ≠ 0 := by rw [ne_eq, zero_iff, Subring.coe_eq_zero_iff]; exact hr
  set vr : Γˣ := Units.mk0 (v r) hr₀ with hvr_def
  have hvr : vr ∈ (valueGroup (.ofClass v)) := by
    apply mem_valueGroup
    rw [hvr_def, Units.val_mk0 hr₀]
    exact mem_range_self _
  rw [π.2.zpowers_eq_valueGroup, mem_zpowers_iff] at hvr
  obtain ⟨m, hm⟩ := hvr
  have hm' : v π.val ^ m = v r := by
    rw [hvr_def] at hm
    rw [← Units.val_mk0 hr₀, ← hm]
    simp [Units.val_zpow_eq_zpow_val, Units.val_mk0]
  have hm₀ : 0 ≤ m := by
    rw [← zpow_le_one_iff_right_of_lt_one₀ π.2.val_pos π.2.val_lt_one, hm']
    exact r.2
  obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hm₀
  use n
  have hpow : v (π.1.1 ^ (-m) * r) = 1 := by
    rw [map_mul, map_zpow₀, ← hm', zpow_neg, hm', inv_mul_cancel₀ hr₀]
  set a : K₀ := ⟨π.1.1 ^ (-m) * r, by apply le_of_eq hpow⟩ with ha
  have ha₀ : (↑a : K) ≠ 0 := by
    simp only [zpow_neg, ne_eq, mul_eq_zero, inv_eq_zero, ZeroMemClass.coe_eq_zero, not_or, ha]
    refine ⟨?_, hr⟩
    rw [hn, zpow_natCast, pow_eq_zero_iff', not_and_or]
    exact Or.inl π.ne_zero
  have h_unit_a : IsUnit a :=
    Integers.isUnit_of_one (integer.integers v) (isUnit_iff_ne_zero.mpr ha₀) hpow
  use h_unit_a.unit
  rw [IsUnit.unit_spec, Subring.coe_pow, ha, ← mul_assoc, zpow_neg, hn, zpow_natCast,
    mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero), one_mul]

Goal state after:
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
I : Ideal ↥v.valuationSubring
this : ∀ (P : Ideal ↥v.valuationSubring), P.IsPrime → Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal I

Tactic:
exact (IsPrincipalIdealRing.of_prime this).principal I

Goal state after: