mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : 2 ^ 16 * 3 ^ 6 ≠ 0
⊢ 47775744 ≠ 0

Tactic:
norm_num1 at this

Goal state after:
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 :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : 47775744 ≠ 0
⊢ 47775744 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

Tactic:
induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat]
      using! W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n => simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg]
        using! ih n <| neg_ne_zero.mp <| by exact_mod_cast h

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

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

Tactic:
exact (W.natDegree_coeff_ΨSq_ofNat n).left

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
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
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) / u ^ 6 = E'.a₆

Tactic:
hu6

Goal state after:
case h.a₆
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
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) / (E.a₆ / E'.a₆) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] =
    ![P x ^ 2 * P x / P x ^ 2 * ![1, 1, 0] x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
hX.mul_div_cancel_left,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x * ![1, 1, 0] x, (-(P y / P x)) ^ 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
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
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ Odd 3

Tactic:
decide

Goal state after:
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
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -(P x ^ 3 * P y / P x ^ 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]

Tactic:
hX.mul_div_cancel_left,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

pp: case neg
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
· exact ⟨hu.unit ^ 4, by convert! (add_smul_of_equiv h hu hv).symm⟩

Goal state after:
case neg
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
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'.dblU P ^ 2, W'.dblY P, W'.dblZ P] = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]

Tactic:
dblY_of_Y_eq hQz hx hy hy',

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
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'.dblU P ^ 2, W'.dblU P ^ 3, W'.dblZ P] = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
· rw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

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

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝² : Semiring R
inst✝¹ : ValuativeRel R
α : Type u_2
inst✝ : Mul α
f : R → ↥(posSubmonoid R) → α
hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t
hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s
x✝¹ : R
y✝¹ : ↥(posSubmonoid R)
x✝ : R
y✝ : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x✝¹ y✝¹ * ValueGroupWithZero.mk x✝ y✝) =
    ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x✝¹ y✝¹) *
      ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x✝ y✝)

Tactic:
simpa using hdist _ _ _ _

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
have hu : ValueGroup₀.embedding u⁻¹.1 = γx⁻¹ := by
          simp [restrict₀_apply, embedding_apply, hu_def, Hx]

Goal state after:
case inr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
⊢ ∃ j,
    ↑(v.ltAddSubgroup ((Units.map ↑embedding) j)) ⊆
      (fun x_1 ↦ x * x_1) ⁻¹' ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.WithZeroTopology

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

Tactic:
by
  rw [nhds_nhdsAdjoint, sup_of_le_right]
  exact le_iInf₂ fun γ hγ ↦ le_principal_iff.2 <| zero_lt_iff.2 hγ

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

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

Tactic:
rw [nhds_eq_update, update_self]

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

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

Tactic:
← negAddY_eq',

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.negAddY P Q = W.negAddY P Q * (P z * Q z) ^ 3 / (P z * Q z) ^ 3
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ x * x.hatInv = 1

Tactic:
by
  have : T1Space (hat K) := T2Space.t1Space
  let f := fun x : hat K => x * hatInv x
  let c := (fun (x : K) => (x : hat K))
  change f x = 1
  have cont : ContinuousAt f x := by fun_prop
  have clo : x ∈ closure (c '' {0}ᶜ) := by
    have := isDenseInducing_coe.dense x
    rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
      image_union] at this
    apply mem_closure_of_mem_closure_union this
    rw [image_singleton]
    exact compl_singleton_mem_nhds x_ne
  have fxclo : f x ∈ closure (f '' c '' {0}ᶜ) := mem_closure_image cont clo
  have : f '' c '' {0}ᶜ ⊆ {1} := by
    rw [image_image]
    rintro _ ⟨z, z_ne, rfl⟩
    rw [mem_singleton_iff]
    rw [mem_compl_singleton_iff] at z_ne
    dsimp [f]
    rw [hatInv_extends z_ne, ← coe_mul]
    rw [mul_inv_cancel₀ z_ne, coe_one]
  replace fxclo := closure_mono this fxclo
  rwa [closure_singleton, mem_singleton_iff] at fxclo

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩

Tactic:
by_cases hb : v b = 0

Goal state after:
case pos
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩

case neg
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
R : Type u_3
inst✝ : Ring R
v : Valuation R Γ₀
b : R
hb : ¬v b = 0
⊢ (WithZero.map' ↑(valueGroupEquiv v).symm) (if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩) =
    if h : v b = 0 then 0 else ↑⟨Units.mk0 (v b) ⋯, ⋯⟩
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
a b : A
H : (valuation K (maximalIdeal A)) ((algebraMap A K) a / (algebraMap A K) b) ≤ 1
hb : b ∈ nonZeroDivisors A
h_frac : (algebraMap A K) a / (algebraMap A K) b = x
ha : ¬a = 0
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
obtain ⟨n, u, rfl⟩ := eq_unit_mul_pow_irreducible ha hπ

Goal state after:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
b : A
hb : b ∈ nonZeroDivisors A
n : ℕ
u : Aˣ
H : (valuation K (maximalIdeal A)) ((algebraMap A K) (↑u * π ^ n) / (algebraMap A K) b) ≤ 1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) b = x
ha : ¬↑u * π ^ n = 0
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.ValuedField

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

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:
· rw [ContinuousAt, map_zero, WithZeroTopology.tendsto_zero]
    intro γ hγ
    rw [Filter.Eventually, Valued.mem_nhds_zero]
    use Units.mk0 γ hγ; rfl

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
⊢ ContinuousAt (⇑v.restrict) x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
⊢ ∃ C, IsMinimal R (C • W)

Tactic:
obtain ⟨C, hC⟩ := exists_maximalFor_of_wellFoundedGT
    (fun (C : VariableChange K) ↦ IsIntegral R (C • W))
    (fun (C : VariableChange K) ↦ valuation_Δ_aux R (C • W))
    (exists_isIntegral R W)

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
⊢ ∃ C, IsMinimal R (C • W)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
⊢ ∀ m < 1, (coeff m) φ = 0

Tactic:
intro m hm

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
m : ℕ
hm : m < 1
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (↑(antidiagonal d)).PairwiseDisjoint fun p ↦
    Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
        Prod.forall, Prod.mk.injEq]
      rintro u v rfl u' v' huv h k - l - hkl
      obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
      simp only [add_right_inj] at huv
      exact h rfl huv.symm

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

Goal state before:
pp: case inr.succ
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
⊢ (0, 1) ∉ {(1, 0)}

Tactic:
decide

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
inhabited_h : Inhabited σ
x : R
⊢ ¬(algebraMap R (MvPowerSeries σ R)) x = X default

Tactic:
rw [MvPowerSeries.ext_iff, not_forall]

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
B : Type u_4
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
inhabited_h : Inhabited σ
x : R
⊢ ∃ x_1, ¬(coeff x_1) ((algebraMap R (MvPowerSeries σ R)) x) = (coeff x_1) (X default)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
⊢ MvPolynomial.coeff x ((truncFinset R s) f * (truncFinset R t) g) = (coeff x) (f * g)

Tactic:
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
⊢ ∑ x ∈ antidiagonal x, MvPolynomial.coeff x.1 ((truncFinset R s) f) * MvPolynomial.coeff x.2 ((truncFinset R t) g) =
    ∑ p ∈ antidiagonal x, (coeff p.1) f * (coeff p.2) g
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ 0 = (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g)

Tactic:
symm

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
⊢ (coeff d) ((weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g) = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i ↦ 0) (𝓝 r) (𝓝 0)

Tactic:
exact tendsto_const_nhds

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁴ : Field K
inst✝³ : CommSemiring S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝ : Algebra S K
r : S
x : (valuation K v).Completion
⊢ r • x = (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * x

Tactic:
induction x using Completion.induction_on with
    | hp =>
      exact isClosed_eq (continuous_const_smul _) (continuous_const_mul _)
    | ih x =>
      simp [Algebra.smul_def, Completion.algebraMap_def, WithVal.algebraMap_right_apply,
        Completion.coeRingHom]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ min φ.order ψ.order

Tactic:
le_inf_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
this : (φ + ψ).order = φ.order
⊢ (φ + ψ).order ≤ φ.order ∧ (φ + ψ).order ≤ ψ.order
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ((trunc (n + 1)) f).natDegree < n + 1

Tactic:
by
  simp +contextual [natDegree_le_iff_coeff_eq_zero, coeff_trunc]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
⊢ IsNonarchimedean (v.intAdicAbvDef hb)

Tactic:
by
  intro x y
  simp only [intAdicAbvDef]
  have h_mono := (toNNReal_strictMono hb).monotone
  rw [← h_mono.map_max]
  exact h_mono <| v.intValuation.map_add x y

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = f.coeff m

Tactic:
symm

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ f.coeff m = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff n) (f * g) = (coeff n) (↑((trunc a) f) * ↑((trunc b) g))

Tactic:
symm

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ (coeff n) (↑((trunc a) f) * ↑((trunc b) g)) = (coeff n) (f * g)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n : ℕ
⊢ ∀ (b : ℕ), n ≤ b → ↑n < (-X ^ (b + 1)).order

Tactic:
intro m hm

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
a✝ : Nontrivial R
n m : ℕ
hm : n ≤ m
⊢ ↑n < (-X ^ (m + 1)).order
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order ≤ p.order

Tactic:
refine le_order _ _ fun d hd => by simp [coeff_of_lt_order d hd, ← coeff_toSubring p T hp]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f_max < cantorFunction c g_min

Tactic:
have : c / (1 - c) < 1 := by
      rw [div_lt_one, lt_sub_iff_add_lt]
      · convert! _root_.add_lt_add h2 h2
        norm_num
      rwa [sub_pos]

Goal state after:
case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c f_max < cantorFunction c g_min
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
ha' : ∀ (i : σ), constantCoeff (a i) = 0
f : MvPowerSeries σ R
hf : constantCoeff f = 0
d : σ →₀ ℕ
hd : ¬d = 0
i : σ
hi : d i ≠ 0
⊢ (fun a b ↦ 0 ^ b) i (d i) = 0

Tactic:
by simp [zero_pow hi]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
by_cases hn : n = 1 <;>
  simp [hn, delta]

Goal state after: