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
n : ℤ
⊢ (X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even (-n) then 1 else W.Ψ₂Sq) =
    X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq

Tactic:
even_neg

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

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

Tactic:
← sq,

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.toShortNFOfCharThree • W).IsShortNF

Tactic:
have H := W.toCharNeTwoNF_spec

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
hb₂ : W.b₂ = 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
H : (W.toCharNeTwoNF • W).IsCharNeTwoNF
⊢ (W.toShortNFOfCharThree • W).IsShortNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := ⋯
W' : WeierstrassCurve F := ⋯
this : W'.IsCharNeTwoNF
⊢ ({ u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 } • W').a₄ = 0

Tactic:
· have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂
    simp [field, variableChange_a₄, -mul_eq_zero]
    linear_combination (W'.a₄ * W'.a₂ ^ 2 + W'.a₄ ^ 2) * CharP.cast_eq_zero F 3

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

Goal state before:
pp: case h.a₂
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ({ u := Units.mk0 u hu0, r := r, s := 0, t := 0 } • E).a₂ = E'.a₂

Tactic:
simp_rw [variableChange_a₂, a₁_of_isShortNF, a₂_of_isShortNF,
      show (3 : F) = 0 from CharP.cast_eq_zero F 3]
    ring1

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

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ -(W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even (-↑n) then 4 else 1) / 2) = ↑(if Even (-↑n) then -↑n / 2 else -↑n)

Tactic:
even_neg

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ -(W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then -↑n / 2 else -↑n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
⊢ ∃ C, C • E = E'

Tactic:
have hu0 : u ≠ 0 := by
      rw [← pow_ne_zero_iff four_ne_zero, hu, div_ne_zero_iff]
      exact ⟨ha₄, ha₄'⟩

Goal state after:
case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
hu0 : u ≠ 0
⊢ ∃ 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
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ False) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
or_false

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
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ (eval P) W.polynomialX ≠ 0 ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P

Tactic:
simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
  rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz, dblU_eq, dblZ]
  simp [field]

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

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

Tactic:
simpa only [add_of_Z_eq_zero_right hQ.left hPz hQz,
        nonsingular_smul _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]

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

Goal state before:
pp: case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Y_eq hPz hQz hxy.left hy hxy.right, nonsingular_smul _ <|
              isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, nonsingular_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
⊢ U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U

Tactic:
hU

Goal state after:
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := hB.topology
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ addZ P Q = P x * Q z * Q z

Tactic:
rw [addZ, hPz]

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z
Module: Mathlib.Topology.Algebra.Nonarchimedean.Bases

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
⊢ U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U

Tactic:
hU

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
this : TopologicalSpace M := hB.topology
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), ValueGroupWithZero.mk x y ^ 0 = 1

Tactic:
HPow.hPow,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)), Pow.pow (ValueGroupWithZero.mk x y) 0 = 1
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    ValueGroupWithZero.mk x y ^ (n + 1) = ValueGroupWithZero.mk x y ^ n * ValueGroupWithZero.mk x y

Tactic:
HPow.hPow,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
n : ℕ
⊢ ∀ (x : R) (y : ↥(posSubmonoid R)),
    Pow.pow (ValueGroupWithZero.mk x y) (n + 1) = Pow.pow (ValueGroupWithZero.mk x y) n * ValueGroupWithZero.mk x y
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ 𝓝 = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))

Tactic:
nhds_nhdsAdjoint,

Goal state after:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
⊢ update pure 0 (pure 0 ⊔ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)) = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
h' : v.restrict x ≠ 0
⊢ {y | v.restrict (y - x) < v.restrict x} ⊆ {y | v y = v x}

Tactic:
intro y y_in

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
h' : v.restrict x ≠ 0
y : R
y_in : y ∈ {y | v.restrict (y - x) < v.restrict x}
⊢ y ∈ {y | v y = v x}
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x : R
h : v x ≠ 0
h' : v.restrict x ≠ 0
⊢ {z | v.restrict (z - x) < v.restrict x} ⊆ {y | v y = v x}

Tactic:
intro y y_in

Goal state after:
case h
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : TopologicalSpace R
v : Valuation R Γ₀
inst✝¹ : v.Compatible
inst✝ : IsValuativeTopology R
x : R
h : v x ≠ 0
h' : v.restrict x ≠ 0
y : R
y_in : y ∈ {z | v.restrict (z - x) < v.restrict x}
⊢ y ∈ {y | v y = v x}
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ v.IsNontrivial

Tactic:
apply IsNontrivial.mk

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ ∃ x, v x ≠ 0 ∧ v x ≠ 1
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:
rw [hvr_def] at hm

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.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

Goal state after:
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set X
⊢ DenselyOrdered ↑s ↔ s.Subsingleton

Tactic:
simp [LocallyFiniteOrder.denselyOrdered_iff_subsingleton]

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ofClass v).ValueGroup₀ˣ
hs : {y | v.restrict (y - x⁻¹) < ↑γ} ⊆ s
γ' : (ofClass v).ValueGroup₀ˣ := ⋯
⊢ {y | v.restrict (y - x) < ↑(min (γ * (γ' * γ')) γ')} ⊆ Inv.inv ⁻¹' s

Tactic:
intro y y_in

Goal state after:
case h
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
s : Set K
γ : (ofClass v).ValueGroup₀ˣ
hs : {y | v.restrict (y - x⁻¹) < ↑γ} ⊆ s
γ' : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
y : K
y_in : y ∈ {y | v.restrict (y - x) < ↑(min (γ * (γ' * γ')) γ')}
⊢ y ∈ Inv.inv ⁻¹' s
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
⊢ IsClosed[hv.toTopologicalSpace] U → U.Nonempty → IsClosed (⇑v.restrict '' U)

Tactic:
hU

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU : IsClosed[hv.toTopologicalSpace] U
⊢ U.Nonempty → IsClosed (⇑v.restrict '' U)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.a₄
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₄ = (algebraMap R K) h₄.choose

pp: case h.a₆
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₆ = (algebraMap R K) h₆.choose

Tactic:
· apply h₄.choose_spec.symm

Goal state after:
case h.a₆
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
h₁ : ∃ r₁, (algebraMap R K) r₁ = W.a₁
h₂ : ∃ r₂, (algebraMap R K) r₂ = W.a₂
h₃ : ∃ r₃, (algebraMap R K) r₃ = W.a₃
h₄ : ∃ r₄, (algebraMap R K) r₄ = W.a₄
h₆ : ∃ r₆, (algebraMap R K) r₆ = W.a₆
⊢ W.a₆ = (algebraMap R K) h₆.choose
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₁

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).a₁
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₂

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₃

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).a₃
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
this : ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h
    · simpa [this h] using ⟨h⟩
    · simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
      exact ⟨fun H ↦ (this H) h⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.a₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₂

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).b₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).b₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).b₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.b₈

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).b₈
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.c₄

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).c₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.c₆

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).c₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| W.Δ

Tactic:
rw [← baseChange_integralModel_eq R W]

Goal state after:
R : Type u_1
inst✝² : CommRing R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
W : WeierstrassCurve K
hW : IsIntegral R W
| ((integralModel R W)⁄K).Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
⊢ ∃ a, (valuation R K) a = lmax

Tactic:
have hi : i < l.length := List.idxOf_lt_length_of_mem hlmax_mem

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
hi : i < l.length
⊢ ∃ a, (valuation R K) a = lmax
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2.inr.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    a ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff (n + 1)) (φ * X) = (coeff n) φ

Tactic:
by
  simp only [coeff, Finsupp.single_add]
  convert! φ.coeff_add_mul_monomial (single () n) (single () 1) _
  rw [mul_one]

Goal state after: