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

Goal state before:
pp: case refine_2
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
h : P ≈ Q
⊢ ⇑f ∘ P ≈ ⇑f ∘ Q

Tactic:
· rcases h with ⟨u, rfl⟩
    exact ⟨Units.map f u, (comp_smul ..).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
x y : B
⊢ (↑(f.lift h)).toFun (x + y) ≤ max ((↑(f.lift h)).toFun x) ((↑(f.lift h)).toFun y)

Tactic:
by
      obtain ⟨a, b, s, rfl, rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y := by
        obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
        obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
        use a * t, b * s, s * t
        constructor <;>
          · rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf
      convert_to! f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)
      · refine congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 ?_)
        rw [add_mul, map_add]
        rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
      iterate 3 rw [f.lift_mk']
      dsimp
      grw [max_mul_mul_right, v.map_add a b]

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
hy : (a, b) ∈ (fun p ↦ p.1 * p.2) ⁻¹' ↑U
⊢ v ∈ ↑U

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy

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 : v ∈ U
⊢ v ∈ ↑U
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / ![W.dblX P, W.negDblY P, W.dblZ P] z ^ 2)
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] 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:
dblX_of_Z_ne_zero hP hQ hPz hQz hx hy,

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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ 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.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] 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.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'.dblXYZ P = P x ^ 2 • ![1, 1, 0]

Tactic:
by
  simp [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz,
    smul_fin3]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : x * y ≤ᵥ x * z
⊢ y ≤ᵥ z

Tactic:
veq_mul_comm,

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y * x ≤ᵥ x * z
⊢ y ≤ᵥ z
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ x * y ≤ᵥ x * z

Tactic:
veq_mul_comm,

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y z : R
hx : 0 <ᵥ x
h : y ≤ᵥ z
⊢ y * x ≤ᵥ x * z
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : x * y ≤ᵥ x * 0
⊢ y ≤ᵥ 0

Tactic:
veq_mul_comm,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x y : R
hx : 0 <ᵥ x
hy : y * x ≤ᵥ x * 0
⊢ y ≤ᵥ 0
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑v * ↑u
⊢ r * ↑w ≤ᵥ t * ↑u

Tactic:
veq_mul_right_comm t

Goal state after:
case left
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z r : R
u : ↥(posSubmonoid R)
s : R
v : ↥(posSubmonoid R)
t : R
w : ↥(posSubmonoid R)
h1 : r * ↑v ≤ᵥ s * ↑u
h2 : s * ↑u ≤ᵥ r * ↑v
h3 : s * ↑w ≤ᵥ t * ↑v
h4 : t * ↑v ≤ᵥ s * ↑w
this✝ : r * ↑v * ↑w ≤ᵥ s * ↑w * ↑u
this : r * ↑w * ↑v ≤ᵥ t * ↑u * ↑v
⊢ r * ↑w ≤ᵥ t * ↑u
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos.refine_2
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
⊢ y * ↑u * ↑s * ↑v ≤ᵥ 0 * (↑t * ↑u)

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h s) v).trans

Goal state after:
case pos.refine_2
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 * ↑v ≤ᵥ 0 * (↑t * ↑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✝ 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 : x * ↑v ≤ᵥ z * ↑s
⊢ z * ↑s * (↑t * w) =ᵥ w * ↑t * ↑s * z

Tactic:
veq_mul_comm,

Goal state after:
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 : x * ↑v ≤ᵥ z * ↑s
⊢ ↑t * w * (z * ↑s) =ᵥ w * ↑t * ↑s * z
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:
veq_mul_comm,

Goal state after:
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
⊢ ↑s * z * (w * ↑t) =ᵥ z * ↑s * ↑t * w
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case neg.h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑s * ↑⟨y, hy⟩ ≤ᵥ ↑t * ↑⟨x, hx⟩

Tactic:
veq_mul_comm,

Goal state after:
case neg.h₁
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑⟨y, hy⟩ * ↑s ≤ᵥ ↑t * ↑⟨x, hx⟩
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑t * ↑⟨x, hx⟩ ≤ᵥ ↑s * ↑⟨y, hy⟩

Tactic:
veq_mul_comm,

Goal state after:
case h₂
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ ↑⟨x, hx⟩ * ↑t ≤ᵥ ↑s * ↑⟨y, hy⟩
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 : R
y : ↥(posSubmonoid R)
h : ¬(x * ↑1 ≤ᵥ 0 * ↑y ∧ 0 * ↑y ≤ᵥ x * ↑1)
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1

Tactic:
simp only [Submonoid.coe_one, mul_one, zero_mul, zero_vle, and_true] at h

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
h : ¬x ≤ᵥ 0
⊢ ValueGroupWithZero.mk x y * (ValueGroupWithZero.mk x y)⁻¹ = 1
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
a : α
⊢ (extensionHom f hf) ↑a = f a

Tactic:
by
  simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

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

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : R
⊢ (embed v) ((valuation R) x) = (restrict₀ (ofClass v)) x

Tactic:
by
  convert! embed_mk v x 1
  simp

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

Goal state before:
pp: A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
hπ : exp (-1) ∈ range ⇑v
⊢ generator v = Units.mk0 (exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

Tactic:
by
  rw [← Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator]
  suffices Units.mk0 (exp (-1)) (by simp) = (Subgroup.genLTOne (valueGroup (.ofClass v))) by
    simp [← this]
  apply Subgroup.genLTOne_unique
  · exact compareOfLessAndEq_eq_lt.mp rfl
  · ext n
    simp_all only [Int.reduceNeg, exp_neg, Subgroup.mem_zpowers_iff, mem_valueGroup_iff_of_comm,
      ne_eq]
    refine ⟨fun ⟨k, h⟩ ↦ ?_ , fun _ ↦ ⟨-WithZero.log n, by aesop⟩⟩
    rw [← h]
    have ⟨π, hπ⟩ := hπ
    cases k with
    | ofNat n => refine ⟨1, ?_, π ^ n, ?_⟩ <;> simp [hπ]
    | negSucc n => refine ⟨π ^ (n + 1), ?_, 1, ?_⟩ <;> simp [hπ, Int.negSucc_eq, mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case neg
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : ∃ x y, 0 < y ∧ ∀ (n : ℕ), n • y < x
⊢ Nonempty (G ≃+o ℤ)

Tactic:
exfalso
      obtain ⟨x, y, hy0, H⟩ := H
      obtain ⟨_, ⟨n, rfl⟩, hz⟩ :=
        h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
      refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
      simp [add_smul, hy0]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
⊢ ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
let e : G ≃o Additive G := OrderIso.refl G
  suffices Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Set.WellFoundedOn {x | e g ≤ x} (· < ·) by
    rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete,
      OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
  refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_,
    fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩ <;>
  simp [Function.onFun]

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (coeff m) (φ * (monomial n) a) = (coeff m) ((monomial n) a * φ)

Tactic:
· rw [coeff_mul_monomial, coeff_monomial_mul]
    split_ifs <;> [apply h; rfl]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = (coeff (single s 1)) (X t)
⊢ s = t

Tactic:
coeff_X

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = if single s 1 = single t 1 then 1 else 0
⊢ s = t
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
have h_dvd_x : x ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff x nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
          · exact min_le_left _ _
          exact v.associates_irreducible

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
nmin : ℕ :=
  min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
    ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
h_dvd_x : x ∈ v.asIdeal ^ nmin
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : v x = v y
⊢ embedding a = embedding b

Tactic:
rwa [← hx, ← hy]

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
⊢ n ≤ weightedOrder w f

Tactic:
cases n
  · rw [top_le_iff, weightedOrder_eq_top_iff]
    ext d; exact h d (ENat.natCast_lt_top _)
  · apply nat_le_weightedOrder;
    simpa only [ENat.some_eq_natCast, Nat.cast_lt] using h

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ Tendsto (fun x ↦ X x) cofinite (𝓝 0)

Tactic:
by
  classical
  simp only [tendsto_iff_coeff_tendsto, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases! h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using
      Eventually.of_forall fun x h' ↦ (h x h').elim

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
φ : R⟦X⟧
⊢ ((trunc n) φ).coeff m = if m < n then (coeff m) φ else 0

Tactic:
by
  simp [trunc, coeff_truncAux]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    ∑ m ∈ Ico 0 n, (Polynomial.monomial m) ((coeff m) f) + (Polynomial.monomial n) ((coeff n) f)

Tactic:
Ico_zero_eq_range

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ ∑ x ∈ range n, (Polynomial.monomial x) ((coeff x) f) + (Polynomial.monomial n) ((coeff n) f) =
    ∑ m ∈ range n, (Polynomial.monomial m) ((coeff m) f) + (Polynomial.monomial n) ((coeff n) f)
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then (coeff d) X else 0) = Polynomial.X.coeff d

Tactic:
coeff_X

Goal state after:
R : Type u_1
inst✝ : Semiring R
n d : ℕ
⊢ (if d < n + 2 then if d = 1 then 1 else 0 else 0) = Polynomial.X.coeff d
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : ¬f.order.toNat ≤ n
⊢ 0 = (coeff n) f

Tactic:
push Not at h

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
h : n < f.order.toNat
⊢ 0 = (coeff n) f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f ≠ 0 ∧ g ≠ 0
⊢ X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder =
    X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)

Tactic:
calc
    _ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by
        rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
    _ = f * g := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) := by
        simp [X_pow_order_mul_divXPowOrder]
    _ = f.divXPowOrder * g.divXPowOrder * X ^ (g.order.toNat + f.order.toNat) := by
        rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
    _ = X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder) := by
        rw [X_pow_mul, add_comm]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ UniformContinuous (eval₂ φ a)

Tactic:
← coe_eval₂Hom hφ ha

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ UniformContinuous ⇑(eval₂Hom hφ ha)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p
⊢ ε = eval₂ φ a

Tactic:
← coe_eval₂Hom hφ ha

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
ε : MvPowerSeries σ R → S
hε : Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] ε
h : ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ φ a p
⊢ ε = ⇑(eval₂Hom hφ ha)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ ¬g n = f n

Tactic:
apply Ne.symm

Goal state after:
case false
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := ⋯
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ f n ≠ g n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ ¬g n = f n

Tactic:
apply Ne.symm

Goal state after:
case true
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := ⋯
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ f n ≠ g n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : 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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
d : τ →₀ ℕ
hd : ↑((Finsupp.weight w) d) < ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d
x : σ →₀ ℕ
hfx : (coeff x) f = 0
⊢ (coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) = 0

Tactic:
simp [hfx]

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

Goal state before:
pp: f : ℕ → ℂ
h : f 1 = 1
⊢ f * δ = δ

Tactic:
by
  rw [mul_delta_eq_smul_delta, h, one_smul]

Goal state after: