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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (¬(W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 ^ 2 + W'.a₄ * 1 ^ 4) = 0 ∧
          2 * b + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 3 = 0 ∧
            W'.a₁ * a * b + 3 * W'.a₃ * b * 1 ^ 2 -
                (2 * W'.a₂ * a ^ 2 * 1 + 4 * W'.a₄ * a * 1 ^ 3 + 6 * W'.a₆ * 1 ^ 5) =
              0) ↔
      ¬(W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
          2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0))

Tactic:
not_iff_not,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
a b : R
⊢ b ^ 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
        (a ^ 3 + W'.toAffine.a₂ * a ^ 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
      0 →
    (W'.a₁ * b * 1 - (3 * a ^ 2 + 2 * W'.a₂ * a * 1 ^ 2 + W'.a₄ * 1 ^ 4) = 0 ∧
        2 * b + W'.a₁ * a * 1 + W'.a₃ * 1 ^ 3 = 0 ∧
          W'.a₁ * a * b + 3 * W'.a₃ * b * 1 ^ 2 - (2 * W'.a₂ * a ^ 2 * 1 + 4 * W'.a₄ * a * 1 ^ 3 + 6 * W'.a₆ * 1 ^ 5) =
            0 ↔
      W'.toAffine.a₁ * b - (3 * a ^ 2 + 2 * W'.toAffine.a₂ * a + W'.toAffine.a₄) = 0 ∧
        2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3

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

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ W.Nonsingular (W.add P Q)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

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

Tactic:
revert hQ

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.NonsingularLift Q → W.addMap ⟦P⟧ Q = Q
Module: Mathlib.Topology.Algebra.UniformFilterBasis

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Tactic:
let := B.uniformSpace
  have := B.isUniformAddGroup
  suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U by
    constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
  rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
  change Tendsto _ _ _ ↔ _
  simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_comm (_ ∈ _) G]

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

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

Tactic:
by_cases hxy : P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3

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

case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ toAffine W (W.add P Q) = toAffine W P + toAffine W Q
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z : R
h : 1 * ↑1 ≤ᵥ 0 * ↑1
⊢ False

Tactic:
simp [not_vle_one_zero] at h

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ : Completion α
a : α
⊢ 0 • ↑a = 0

Tactic:
rw [← coe_smul, ← coe_zero, zero_smul]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝³ : Ring R
inst✝² : ValuativeRel R
Γ₀ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst✝ : v.Compatible
r : R
s : ↥(posSubmonoid R)
hr✝ : ValueGroupWithZero.mk r s ≠ 0
hr' : ValueGroupWithZero.mk r s ≠ 1
hγ : v r ≠ 0
hγ' : v r ≤ v ↑s → v r < v ↑s
hr : v r = 1
⊢ v.IsNontrivial

Tactic:
exact ⟨s, by simp, fun h ↦ by simp [h, hr] at hγ'⟩

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
⊢ Completion.extension (⇑f) 0 = 0

Tactic:
rw [← coe_zero, extension_coe hf, f.map_zero]

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
⊢ CompletableTopField α

Tactic:
refine CompletableTopField.mk (fun F F_cau inf_F => ?_)
  rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢
  have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
    ext; simp only [Function.comp_apply, map_inv₀]
  rw [Filter.map_comm h_comm]
  apply CompletableTopField.nice _ F_cau
  rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

Goal state after:
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
⊢ Subgroup.map (MonoidWithZeroHom.ofClass v).valueGroup.subtype (zpowers (generator' v)) =
    Subgroup.map (MonoidWithZeroHom.ofClass v).valueGroup.subtype ⊤

Tactic:
MonoidHom.map_zpowers,

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ zpowers ((MonoidWithZeroHom.ofClass v).valueGroup.subtype (generator' v)) =
    Subgroup.map (MonoidWithZeroHom.ofClass v).valueGroup.subtype ⊤
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
⊢ x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹

Tactic:
rw [mul_sub_left_distrib, sub_mul, mul_assoc, show y * y⁻¹ = 1 from mul_inv_cancel₀ y_ne,
      show x⁻¹ * x = 1 from inv_mul_cancel₀ x_ne, mul_one, one_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y r s : K
y_ne : y ≠ 0
hr : r ≠ 0
hs : s ≠ 0
h : v (x - y) < min (v s / v r * (v y * v y)) (v y)
hr' : 0 < v r
γ : Γ₀ˣ := Units.mk0 (v s / v r) ⋯
⊢ v (x⁻¹ - y⁻¹) * v r < ↑γ * v r

Tactic:
by gcongr; exact Valuation.inversion_estimate v y_ne h

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

Goal state before:

Tactic:
v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
    _ = v s := div_mul_cancel₀ _ (by simpa)

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
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz' : z < y
hz0 : ⊥ < ↑z
⊢ (↑z).unbot ⋯ < (↑y).unbot ⋯

Tactic:
← WithBot.coe_lt_coe,

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H✝ : DenselyOrdered ↑s
this : (some ⁻¹' s).Subsingleton
x y : ↑s
H : x < y
z : ↑s
hz : x < z
hz' : z < y
hz0 : ⊥ < ↑z
⊢ ↑((↑z).unbot ⋯) < ↑((↑y).unbot ⋯)
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case pos
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : x = 0
⊢ ∃ u, u • x = y

Tactic:
rw [eq_comm] at h
    simp_all

Goal state after:
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 Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
⊢ ∃ γ₀, ∃ M ∈ F, ∀ x ∈ M, ↑γ₀ ≤ v.restrict x

Tactic:
exists γ₀, M, M_in

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
F : Filter K
hF : Cauchy F
h0 : 𝓝 0 ⊓ F = ⊥
U : Set K
U_in : U ∈ 𝓝 0
M : Set K
M_in : M ∈ F
H : U ∩ M = ∅
γ₀ : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
hU : {x | v.restrict x < ↑γ₀} ⊆ U
⊢ ∀ x ∈ M, ↑γ₀ ≤ v.restrict x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this : closure {b ^ n} = closure {b}
⊢ b = |b ^ n|ₘ ∧ 1 < b

Tactic:
have := h.left

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y | y ∈ closure {b ^ n} ∧ 1 < y} b
this✝ : closure {b ^ n} = closure {b}
this : b ∈ {y | y ∈ closure {b ^ n} ∧ 1 < y}
⊢ b = |b ^ n|ₘ ∧ 1 < b
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
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
⊢ (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀

Tactic:
have c : Continuous fun x : hat K => x * x₀⁻¹ := by fun_prop

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀) '' V' ∈ 𝓝 x₀
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K) W_int.Δ = W.Δ

Tactic:
hW_int,

Goal state after:
case h
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
W : WeierstrassCurve K
inst✝ : IsIntegral R W
W_int : WeierstrassCurve R
hW_int : W = W_int⁄K
⊢ (algebraMap R K) W_int.Δ = (W_int⁄K).Δ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
⊢ (monomial m) a * (monomial n) b = (monomial (m + n)) (a * b)

Tactic:
classical
  ext k
  simp only [coeff_mul_monomial, coeff_monomial]
  split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl
  · rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
    exact (h₃ rfl).elim
  · rw [h₃, add_tsub_cancel_right] at h₂
    exact (h₂ rfl).elim
  · exact zero_mul b
  · rw [h₂] at h₁
    exact (h₁ <| le_add_left le_rfl).elim

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

Goal state before:
pp: case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
hm : m < n
⊢ (coeff m) φ = 0

Tactic:
apply h
    simpa only [Finsupp.single_eq_same] using hm

Goal state after:
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 : ℕ
hm : m < 1
⊢ (coeff m) φ = 0

Tactic:
Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
m : ℕ
hm : m < 1
⊢ (coeff 0) φ = 0
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)
h_dvd_x : x ∈ v.asIdeal ^ nmin
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

Tactic:
rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy

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
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
⊢ nmin ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors

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
h_dvd_y : y ∈ v.asIdeal ^ nmin
h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y})
⊢ Irreducible (Associates.mk v.asIdeal)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : ¬r = 0
⊢ v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
rw [v.intValuation_if_neg hr, ← exp_zero, exp_lt_exp,
      neg_lt_zero, ← Int.ofNat_zero, Int.ofNat_lt, zero_lt_iff]
    have h : (Ideal.span {r} : Ideal R) ≠ 0 := by
      rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
      exact hr
    exact Associates.count_ne_zero_iff_dvd h v.irreducible

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = 1

Tactic:
← Int.ofNat_one,

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = ↑1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
s : Finset ι
⊢ (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)

Tactic:
induction s using Finset.induction_on generalizing d with
  | empty =>
    simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
    split_ifs
    · simp only [card_singleton, Nat.cast_one]
    · simp only [card_empty, Nat.cast_zero]
  | insert a s ha ih =>
    rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
    · apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha
    · 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.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ Associates.mk (Ideal.span {d}) ≤ Associates.mk (Ideal.span {n})

Tactic:
← Associates.factors_le,

Goal state after:
case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
hd0 : d ≠ 0
ine : ∀ {r : R}, r ≠ 0 → Ideal.span {r} ≠ ⊥
⊢ (Associates.mk (Ideal.span {d})).factors ≤ (Associates.mk (Ideal.span {n})).factors
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

pp: case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ¬f = 0

Tactic:
· simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
    exact ⟨weight w d, le_rfl, d, h, rfl⟩

Goal state after:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ¬f = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case insert
σ : Type u_1
w : σ → ℕ
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, ↑((weight w) d) < weightedOrder w (g i)) → (coeff d) (f * ∏ i ∈ s, (1 - g i)) = (coeff d) f
h : ↑((weight w) d) < weightedOrder w (g a) ∧ ∀ a ∈ s, ↑((weight w) d) < weightedOrder w (g a)
⊢ (coeff d) (f * ∏ i ∈ insert a s, (1 - g i)) = (coeff d) f

Tactic:
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm,
      coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]

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
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : adicCompletion K v
⊢ embedding ((valuation K v).restrict x) = embedding (Valued.v.restrict x.toCompletion)

Tactic:
embedding_restrict,

Goal state after:
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
x : adicCompletion K v
⊢ (valuation K v) x = embedding (Valued.v.restrict x.toCompletion)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : n < φ.order.toNat
⊢ (coeff n) φ = 0

Tactic:
by_cases h' : φ = 0
  · simp [h']
  · refine coeff_of_lt_order _ ?_
    rwa [← coe_toNat_order h', ENat.natCast_lt_natCast]

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

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

Tactic:
refine le_order _ _ ?_

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
⊢ ∀ (i : ℕ), ↑i < min φ.order ψ.order → (coeff i) (φ + ψ) = 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (coeff j) f = (if n ≤ j then (coeff (j - n)) (mk fun i ↦ (coeff (i + n)) f) else 0) + if j < n then (coeff j) f else 0

Tactic:
simp_rw [← not_le, ite_not, ite_add_ite]

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (coeff j) f = if n ≤ j then (coeff (j - n)) (mk fun i ↦ (coeff (i + n)) f) + 0 else 0 + (coeff j) f
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
⊢ ∀ᶠ (x : ι) in f, (a • m) x ∈ ↑I

Tactic:
filter_upwards [ha I hI] with i ai_mem

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace M
inst✝ : IsLinearTopology R M
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), ↑i ∈ 𝓝 0 → ∀ᶠ (x : ι) in f, m x ∈ ↑i
I : Submodule R M
hI : ↑I ∈ 𝓝 0
i : ι
ai_mem : m i ∈ ↑I
⊢ (a • m) i ∈ ↑I
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]

Goal state after: