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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₂ = 0

Tactic:
rw [b₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 + 4 * 0 = 0
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 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
⊢ ∃ C, C • E = E'

Tactic:
have ha₃ := E.Δ'.ne_zero
  rw [E.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃
  have ha₃' := E'.Δ'.ne_zero
  rw [E'.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃'
  have : NeZero (3 : F) := NeZero.mk <| by
    rw [show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
    exact one_ne_zero
  obtain ⟨u, hu⟩ := IsSepClosed.exists_pow_nat_eq (E.a₃ / E'.a₃) 3
  obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 4
    1 _ (E.a₄ - u ^ 4 * E'.a₄) (by simp) (by simp) ha₃
  obtain ⟨t, ht⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 _ (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) (by simp) (by simp) ha₃
  have hu0 : u ≠ 0 := by
    rw [← pow_ne_zero_iff three_ne_zero, hu, div_ne_zero_iff]
    exact ⟨ha₃, ha₃'⟩
  use ⟨Units.mk0 u hu0, s ^ 2, s, t⟩
  ext
  · simp_rw [variableChange_a₁, a₁_of_isCharTwoJEqZeroNF,
      show (2 : F) = 0 from CharP.cast_eq_zero F 2]
    ring1
  · simp_rw [variableChange_a₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF,
      show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
    ring1
  · simp_rw [variableChange_a₃, Units.val_inv_eq_inv_val, Units.val_mk0, inv_pow, inv_mul_eq_div,
      hu, a₁_of_isCharTwoJEqZeroNF, show (2 : F) = 0 from CharP.cast_eq_zero F 2]
    simp [field]
  · simp [field, variableChange_a₄, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
    linear_combination hs + (s ^ 4 - s * t - E.a₃ * s) * CharP.cast_eq_zero F 2
  · simp [field, variableChange_a₆, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
    linear_combination ht - (t ^ 2 + E.a₃ * t) * CharP.cast_eq_zero F 2

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 4 +
        (W.a₁ * P y / P z ^ 3 * 1 + 2 * W.a₂ * P x / P z ^ 2 * (P z ^ 2 / P z ^ 2) + W.a₄ * (P z ^ 4 / P z ^ 4)) -
      (Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialX +
        (W.a₁ * P y / P z ^ 3 * (P z / P z) + 2 * W.a₂ * P x / P z ^ 2 * 1 + W.a₄ * 1)) =
    0

Tactic:
(rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1)

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ 6 * (eval P) W'.polynomial =
    2 * P x * (eval P) W'.polynomialX + 3 * P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
by
  rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
  ring1

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

Goal state before:
pp: case succ.succ
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
⊢ (W.Φ ↑(n + 1 + 1)).natDegree ≤ (n + 1 + 1) ^ 2 ∧ (W.Φ ↑(n + 1 + 1)).coeff ((n + 1 + 1) ^ 2) = 1

Tactic:
rw [Nat.cast_add, Nat.cast_one, Φ_ofNat]

Goal state after:
case succ.succ
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) -
          W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
      (n + 1 + 1) ^ 2 ∧
    ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
            W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).coeff
        ((n + 1 + 1) ^ 2) =
      1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P = (P x ^ 2) ^ 2

Tactic:
by
  linear_combination (norm := (rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]; ring1))
    -8 * P x * (equation_of_Z_eq_zero hPz).mp hP

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 ↦ x1 * x2) a b = v
⊢ v ∈ ↑U

Tactic:
have hy := H (Set.mk_mem_prod ha hb)

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 ↦ x1 * x2) a b = v
hy : (a, b) ∈ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
⊢ v ∈ ↑U
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.add P Q = W.dblU P • ![1, 1, 0]

Tactic:
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']

Goal state after:
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 : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)

Tactic:
· rintro _ ⟨a, -, m, hm, rfl⟩
        exact (B i).smul_mem _ hm

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

Goal state before:

Tactic:
y * u * s * z
          _ =ᵥ y * s * (z * u) := by grw [veq_mul_comm z, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ x * t * (w * v) := by gcongr
          _ =ᵥ x * v * (t * w) := by grw [veq_mul_comm w, veq_mul_mul_mul_comm, mul_assoc]
          _ ≤ᵥ z * s * (t * w) := by gcongr
          _ =ᵥ w * t * s * z := by grw [veq_mul_comm, veq_mul_comm _ w, veq_mul_comm z, ← mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : TopologicalSpace R
inst✝ : IsValuativeTopology R
x✝¹ : (ValueGroupWithZero R)ˣ
x✝ : R
⊢ x✝ = x✝ - 0

Tactic:
rw [sub_zero]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s = (valuation R) r / (valuation R) ↑s

Tactic:
rw [eq_div_iff (valuation_posSubmonoid_ne_zero _)]
  simp [valuation, mk_eq_mk]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ 0 * ↑a = 0

Tactic:
rw [← coe_zero, ← coe_mul, zero_mul]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (⇑f) (map (fun x ↦ x⁻¹) F))

Tactic:
have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
    ext; simp only [Function.comp_apply, map_inv₀]

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ Cauchy (map (⇑f) (map (fun x ↦ x⁻¹) F))
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
h1 : ∀ (x : A), v x ≠ 0 → v x = 1
hvalueGroup : (MonoidWithZeroHom.ofClass v).valueGroup = ⊥
⊢ False

Tactic:
aesop (add safe forward [generator_lt_one, generator_zpowers_eq_valueGroup])

Goal state after:
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
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.toAffine.negY
      (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)))
      (![W.addX P Q, W.negAddY P Q, addZ P Q] y / ![W.addX P Q, W.negAddY P Q, addZ P Q] z ^ 3) =
    W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / 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))

Tactic:
negAddY_of_Z_ne_zero hP hQ hPz hQz hx,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq 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.toAffine.negY
      (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)))
      (W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / 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.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / 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))
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 Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ v 1 ≠ 0

Tactic:
Valuation.map_one

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
⊢ 1 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₁
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ r₁, (algebraMap R K) r₁ = ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₁

Tactic:
apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_

Goal state after:
case h.h₁
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
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₂
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ r₂, (algebraMap R K) r₂ = ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₂

Tactic:
apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_

Goal state after:
case h.h₂
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
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₃
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ r₃, (algebraMap R K) r₃ = ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₃

Tactic:
apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_

Goal state after:
case h.h₃
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
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 3
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2.inl
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 ℤ
b : G₀
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun b ↔
    0 ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2.inr.inl
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 : G₀
ha : a ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans ↑(OrderMonoidIso.withZero f)).toFun 0 ↔
    a ≤ 0

Tactic:
simp [WithZero.withZeroUnitsEquiv]

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

Goal state before:
pp: case h.h₄
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ r₄, (algebraMap R K) r₄ = ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₄

Tactic:
apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_

Goal state after:
case h.h₄
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
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₆
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ∃ r₆, (algebraMap R K) r₆ = ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₆

Tactic:
apply (mem_integer_iff _ _ _).mp
      simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
      apply (Valuation.mem_integer_iff _ _).mpr
      simp only [map_mul, map_inv₀, map_pow, ha]
      refine inv_mul_le_one_of_le₀ ?_ zero_le
      refine (hlmax _ (by simp [l₀, l])).trans ?_

Goal state after:
case h.h₆
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
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 6
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ (coeff n) (C a) = if n = 0 then a else 0

Tactic:
← monomial_zero_eq_C_apply,

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
⊢ (coeff n) ((monomial 0) a) = if n = 0 then a else 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff d) (p * X ^ n) = if n ≤ d then (coeff (d - n)) p else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff d) (p * X ^ n) = (coeff (d - n)) p

case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (p * X ^ n) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1

Tactic:
v.intValuationDef_if_neg one_ne_zero,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {1})).factors)) = 1
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.factors 1))) = 1

Tactic:
Associates.factors_one,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ exp (-↑((Associates.mk v.asIdeal).count 0)) = 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff d) (X ^ n * p) = if n ≤ d then (coeff (d - n)) p else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff d) (X ^ n * p) = (coeff (d - n)) p

case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
⊢ f (if n = 0 then 1 else 0) = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
h : n = 0
⊢ f 1 = 1

case neg
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
n : σ →₀ ℕ
h : ¬n = 0
⊢ f 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
⊢ (if n✝ = 0 then a ^ n✝ else 0) = if n✝ = 0 then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
h : n✝ = 0
⊢ a ^ n✝ = 1

case neg
R : Type u_1
inst✝ : CommSemiring R
a : R
n✝ : ℕ
h : ¬n✝ = 0
⊢ 0 = 0