mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑m + 1) * k)

Tactic:
rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]

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

Goal state before:
pp: case inl
n : ℕ
hn : 2 * n ≠ 0
⊢ 2 * ↑(expDegree (2 * n)) = ↑(2 * n) ^ 2 - if Even (2 * n) then 4 else 1

Tactic:
rcases n with _ | n
    · contradiction
    push_cast [expDegree, show (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4 by ring1, even_two_mul,
      Nat.add_sub_cancel, Nat.mul_div_cancel_left _ two_pos]
    ring1

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

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

Tactic:
simp only [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv x)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4)

Tactic:
pderiv_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * Y ^ (2 - 1) * 0 + (((0 * X + C W'.a₁ * 1) * Y + C W'.a₁ * X * 0) * Z + C W'.a₁ * X * Y * 0) +
        ((0 * Y + C W'.a₃ * 0) * Z ^ 3 + C W'.a₃ * Y * (↑3 * Z ^ (3 - 1) * 0)) -
      (↑3 * X ^ (3 - 1) * 1 +
            ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 1)) * Z ^ 2 + C W'.a₂ * X ^ 2 * (↑2 * Z ^ (2 - 1) * 0)) +
          ((0 * X + C W'.a₄ * 1) * Z ^ 4 + C W'.a₄ * X * (↑4 * Z ^ (4 - 1) * 0)) +
        (0 * Z ^ 6 + C W'.a₆ * (↑6 * Z ^ (6 - 1) * 0))) =
    C W'.a₁ * Y * Z - (3 * X ^ 2 + 2 * C W'.a₂ * X * Z ^ 2 + C W'.a₄ * Z ^ 4)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv y)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C 2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3

Tactic:
pderiv_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * Y ^ (2 - 1) * 1 + (((0 * X + C W'.a₁ * 0) * Y + C W'.a₁ * X * 1) * Z + C W'.a₁ * X * Y * 0) +
        ((0 * Y + C W'.a₃ * 1) * Z ^ 3 + C W'.a₃ * Y * (↑3 * Z ^ (3 - 1) * 0)) -
      (↑3 * X ^ (3 - 1) * 0 +
            ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 0)) * Z ^ 2 + C W'.a₂ * X ^ 2 * (↑2 * Z ^ (2 - 1) * 0)) +
          ((0 * X + C W'.a₄ * 0) * Z ^ 4 + C W'.a₄ * X * (↑4 * Z ^ (4 - 1) * 0)) +
        (0 * Z ^ 6 + C W'.a₆ * (↑6 * Z ^ (6 - 1) * 0))) =
    2 * Y + C W'.a₁ * X * Z + C W'.a₃ * Z ^ 3
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
i' : I
fi'i : i' ⟶ i
hi' : ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2
k : I
fki : k ⟶ i
ak : (j : ↥s) → ↑(D.map fki ⁻¹ᵁ 𝒱 j) ⟶ X
hak : ∀ (j : ↥s), ak j ≫ f = (D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ t.app k
hak' : ∀ (j : ↥s), c.π.app k ∣_ D.map fki ⁻¹ᵁ 𝒱 j ≫ ak j = (c.π.app k ⁻¹ᵁ D.map fki ⁻¹ᵁ 𝒱 j).ι ≫ a
𝒱' : ↥s → (D.obj k).Opens := fun x ↦ D.map fki ⁻¹ᵁ 𝒱 x
j₁ j₂ : ↥s
x✝ : ∀ (x : Over k), CompactSpace ↥((opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).obj x)
l : I
flk : (𝟭 I).obj l ⟶ (Functor.fromPUnit k).obj { as := PUnit.unit }
flk' : { left := l, right := { as := PUnit.unit }, hom := flk }.left ⟶ (Over.mk (𝟙 k)).left
h :
  (𝟭 I).map flk' ≫ (Over.mk (𝟙 k)).hom =
    { left := l, right := { as := PUnit.unit }, hom := flk }.hom ≫ (Functor.fromPUnit k).map { down := { down := ⋯ } }
e :
  (opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).map { left := flk', right := { down := { down := ⋯ } }, w := h } ≫
      (D.obj (Over.mk (𝟙 k)).left).homOfLE ⋯ ≫ ak j₁ =
    (opensDiagram D k (𝒱' j₁ ⊓ 𝒱' j₂)).map { left := flk', right := { down := { down := ⋯ } }, w := h } ≫
      (D.obj (Over.mk (𝟙 k)).left).homOfLE ⋯ ≫ ak j₂
⊢ flk = flk'

Tactic:
by simpa using! h.symm

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv z)
      (Y ^ 2 + C W'.a₁ * X * Y * Z + C W'.a₃ * Y * Z ^ 3 -
        (X ^ 3 + C W'.a₂ * X ^ 2 * Z ^ 2 + C W'.a₄ * X * Z ^ 4 + C W'.a₆ * Z ^ 6)) =
    C W'.a₁ * X * Y + C (3 * W'.a₃) * Y * Z ^ 2 -
      (C (2 * W'.a₂) * X ^ 2 * Z + C (4 * W'.a₄) * X * Z ^ 3 + C (6 * W'.a₆) * Z ^ 5)

Tactic:
pderiv_simp

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * Y ^ (2 - 1) * 0 + (((0 * X + C W'.a₁ * 0) * Y + C W'.a₁ * X * 0) * Z + C W'.a₁ * X * Y * 1) +
        ((0 * Y + C W'.a₃ * 0) * Z ^ 3 + C W'.a₃ * Y * (↑3 * Z ^ (3 - 1) * 1)) -
      (↑3 * X ^ (3 - 1) * 0 +
            ((0 * X ^ 2 + C W'.a₂ * (↑2 * X ^ (2 - 1) * 0)) * Z ^ 2 + C W'.a₂ * X ^ 2 * (↑2 * Z ^ (2 - 1) * 1)) +
          ((0 * X + C W'.a₄ * 0) * Z ^ 4 + C W'.a₄ * X * (↑4 * Z ^ (4 - 1) * 1)) +
        (0 * Z ^ 6 + C W'.a₆ * (↑6 * Z ^ (6 - 1) * 1))) =
    C W'.a₁ * X * Y + 3 * C W'.a₃ * Y * Z ^ 2 -
      (2 * C W'.a₂ * X ^ 2 * Z + 4 * C W'.a₄ * X * Z ^ 3 + 6 * C W'.a₆ * Z ^ 5)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
induction n using Int.negInduction with
  | nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.natDegree_preΨ'_le n
  | neg ih => simp_rw [preΨ_neg, natDegree_neg, Int.natAbs_neg, even_neg, ih]

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
K : Type v
inst✝ : Field K
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
  · by_cases hz : f (P z) = 0
    · exact equiv_of_Z_eq_zero hP hQ ((map_eq_zero_iff f f.injective).mp hz) <|
        (map_eq_zero_iff f f.injective).mp <| (Z_eq_zero_of_equiv h).mp hz
    · refine equiv_of_X_eq_of_Y_eq ((map_ne_zero_iff f f.injective).mp hz)
        ((map_ne_zero_iff f f.injective).mp <| hz.comp (Z_eq_zero_of_equiv h).mpr) ?_ ?_
      all_goals apply f.injective; map_simp
      exacts [X_eq_of_equiv h, Y_eq_of_equiv h]
  · rcases h with ⟨u, rfl⟩
    exact ⟨Units.map f u, (comp_smul ..).symm⟩

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 : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
· simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
      nonsingular_neg_of_Z_ne_zero hP hPz]

Goal state after:
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
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ (fun y ↦ a + y) '' ↑(B i) ⊆ s

Tactic:
rw [image_subset_iff]
        rintro b b_in
        apply hi
        simpa using b_in

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

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
x : Γ₀
h : x ≠ 0
⊢ (𝓝 x).HasBasis (fun x ↦ True) fun x_1 ↦ {x}

Tactic:
rw [nhds_of_ne_zero h]
  exact hasBasis_pure _

Goal state after:
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✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : ¬w ≤ᵥ 0
hz : ¬z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ w * ↑t * (↑s * z) =ᵥ z * ↑s * ↑t * w

Tactic:
grw [veq_mul_comm, veq_mul_comm _ z, veq_mul_comm w, ← mul_assoc]

Goal state after:
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) (pure (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
exact pure_le_nhds (x * y)

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClopen {x | v.restrict x = r}

Tactic:
have h : {x : R | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r} := by
    ext x
    simp [← le_antisymm_iff]

Goal state after:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen {x | v.restrict x = r}
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
⊢ IsClopen {x | v.restrict x = r}

Tactic:
have h : {x : R | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r} := by
    ext x
    simp [← le_antisymm_iff]

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
h : {x | v.restrict x = r} = {x | v.restrict x ≤ r} \ {x | v.restrict x < r}
⊢ IsClopen {x | v.restrict x = r}
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
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
⊢ f x = 1

Tactic:
have fxclo : f x ∈ closure (f '' c '' {0}ᶜ) := mem_closure_image cont clo

Goal state after:
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
this : T1Space (hat K)
f : hat K → hat K := fun x ↦ x * x.hatInv
c : K → hat K := fun x ↦ ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
⊢ f x = 1
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst✝¹ : Field K
w : Valuation K Γ
inst✝ : w.IsRankOneDiscrete
⊢ Units.val '' ↑(zpowers (generator w)) = range ⇑w \ {0}

Tactic:
by
  simp [generator_zpowers_eq_valueGroup, valueGroup_eq_range]

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 (WithBot X)
H : DenselyOrdered ↑s
⊢ ∀ (a₁ a₂ : ↑(some ⁻¹' s)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
simp only [Subtype.exists, Set.mem_preimage, Subtype.forall, Subtype.mk_lt_mk, exists_and_right,
    exists_prop]

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ ∀ (a : X), ↑a ∈ s → ∀ (a_1 : X), ↑a_1 ∈ s → a < a_1 → ∃ a_3, (↑a_3 ∈ s ∧ a < a_3) ∧ a_3 < a_1
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 : K
y_in : y ∈ {y | v.restrict (y - x) < ↑(min (γ * (γ' * γ')) γ')}
⊢ y⁻¹ ∈ {y | v.restrict (y - x⁻¹) < ↑γ}

Tactic:
simp only [mem_ofPred_eq, Units.min_val, Units.val_mul] at 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 : v.restrict (y - x) < min (↑γ * (↑γ' * ↑γ')) ↑γ'
⊢ y⁻¹ ∈ {y | v.restrict (y - x⁻¹) < ↑γ}
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ ∃ U ∈ 𝓝 0, x ∉ U

Tactic:
refine ⟨{ k | v k < v x }, ?_, fun h => lt_irrefl _ h⟩

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
x : K
x_ne : x ≠ 0
⊢ {k | v k < v x} ∈ 𝓝 0
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : IsLeast {y | y ∈ ⊤ ∧ 0 < y} x
⊢ G ≃+o ℤ

Tactic:
replace this := AddSubgroup.cyclic_of_min this

Goal state after:
G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
⊢ G ≃+o ℤ
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 Γ₀
⊢ embedding (extension 1) = 1

Tactic:
← Completion.coe_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ embedding (extension ↑1) = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m) ((monomial n) a * φ) = if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.HasAntidiagonal.filter_fst_eq_antidiagonal
    _ n, Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, zero_mul]
    have := mem_antidiagonal.mp hx
    rw [add_comm] at this
    exact ((le_of_add_le_right this.le).trans_lt <| not_le.mp h).ne

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

Goal state before:
pp: case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ f (Classical.choose ⋯) = (coeff k) g

Tactic:
exact Classical.choose_spec (hf (coeff k g))

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

Goal state before:
pp: a b c : ℕ
⊢ ofAdd (-↑c) ≤ ofAdd (-↑a) ∨ ofAdd (-↑c) ≤ ofAdd (-↑b) ↔ min a b ≤ c

Tactic:
ofAdd_le,

Goal state after:
a b c : ℕ
⊢ -↑c ≤ -↑a ∨ ofAdd (-↑c) ≤ ofAdd (-↑b) ↔ min a b ≤ c
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: a b c : ℕ
⊢ -↑c ≤ -↑a ∨ ofAdd (-↑c) ≤ ofAdd (-↑b) ↔ min a b ≤ c

Tactic:
ofAdd_le,

Goal state after:
a b c : ℕ
⊢ -↑c ≤ -↑a ∨ -↑c ≤ -↑b ↔ min a b ≤ c
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ X ∣ φ ↔ constantCoeff φ = 0

Tactic:
rw [← pow_one (X : R⟦X⟧), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff m) φ = 0) ↔ (coeff 0) φ = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : (ofClass extensionValuation).ValueGroup₀
k' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hk' : (restrict₀ (ofClass extensionValuation)) k' = x
this : embedding ((restrict₀ (ofClass v)) ⋯.choose) = embedding (extension k')
⊢ valueGroup₀_hom_extensionValuation (extension k') = x

Tactic:
simpa [← embedding_inj, valueGroup₀_hom_extensionValuation, Valuation.restrict_def, ← hk',
      ← extensionValuation_toFun] using this

Goal state after:
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)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ (coeff (x i)) (f i) = (coeff (Function.update (⇑x) a u i)) (f i)

Tactic:
Function.update_of_ne

Goal state after:
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)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ (coeff (x i)) (f i) = (coeff (x i)) (f i)

case insert.h
σ : 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)
u v : σ →₀ ℕ
x : ι →₀ σ →₀ ℕ
i : ι
hi : i ∈ s
⊢ i ≠ a
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
h1 : ∃ n d, (coeff d) f ≠ 0 ∧ (weight w) d = n
⊢ ∃ d, (coeff d) f ≠ 0 ∧ (weight w) d = Nat.find h1

Tactic:
exact Nat.find_spec h1

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
⊢ weightedOrder w f ≠ ⊤

Tactic:
exact ne_top_of_lt H

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

Goal state before:
pp: case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) (f + g) ≠ 0

Tactic:
(coeff _).map_add,

Goal state after:
case left
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < weightedOrder w g
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ (coeff d) f + (coeff d) g ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
this : ↑((weight w) b) < weightedOrder w f
⊢ (coeff b) (f + g) = 0

Tactic:
(coeff _).map_add,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
hb : (weight w) b < n
this : ↑((weight w) b) < weightedOrder w f
⊢ (coeff b) f + (coeff b) g = 0
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: ⊢ Tendsto Nat.cast atTop (𝓝 ⊤)

Tactic:
tendsto_nhds_top_iff_natCast_lt

Goal state after:
⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ) in atTop, ↑n < ↑a
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
this : ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, ↑a - b = 0
⊢ ContinuousAt (Function.uncurry fun x1 x2 ↦ x1 - x2) (↑a, ⊤)

Tactic:
simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 0

Tactic:
(coeff _).map_add,

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ + (coeff i) ψ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : ↑i < φ.order
⊢ (coeff i) (φ + ψ) = 0

Tactic:
(coeff _).map_add,

Goal state after:
case right
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
H : φ.order < ψ.order
i : ℕ
hi : ↑i < φ.order
⊢ (coeff i) φ + (coeff i) ψ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a : (adicCompletion K v)ˣ
h : Valued.v ↑a = 1
⊢ a ∈ ↑(Submonoid.comap (Units.coeHom (adicCompletion K v)) (adicCompletionIntegers K v).toSubmonoid)⁻¹

Tactic:
by simp [mem_adicCompletionIntegers, inv_le_one_iff₀, h.symm.le]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ 1 = Polynomial.X.coeff d

pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d

Tactic:
· rw [h₂, coeff_X_one]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ 0 = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : 2 ≤ n
⊢ (trunc n) X = Polynomial.X

Tactic:
by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
  exact trunc_X n

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ divXPowOrder 1 = 1

Tactic:
by
  ext k
  simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 𝔠 ≤ x ^ ℵ₀

Tactic:
← two_power_aleph0

Goal state after:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ 2 ^ ℵ₀ ≤ x ^ ℵ₀