mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∃ x, x ∈ U ∩ Set.range ⇑tensorHom

Tactic:
simpa using

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∃ y, tensorHom y ∈ U
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J

Tactic:
simpa using

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∀ (a : X) (b : Y), (f (a, b), ∑ x, (g x) a * (h x) b) ∈ J
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
hnorm : Tendsto (fun i ↦ ‖(Polynomial.aeval (↑ncs i)) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e ↦ ‖(Polynomial.aeval (↑ncs e)) F - 0‖) atTop (𝓝 0)

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
hnorm : Tendsto (fun i ↦ ‖(Polynomial.aeval (↑ncs i)) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e ↦ ‖(Polynomial.aeval (↑ncs e)) F‖) atTop (𝓝 0)
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
⊢ (Polynomial.aeval a) (Polynomial.derivative F) = -q * h

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
⊢ (Polynomial.aeval a) (Polynomial.derivative F) = -(q * h)
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
⊢ T_gen p F a = ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
by
  simp [T_gen]

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
⊢ ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
⊢ ‖(Polynomial.aeval z) (Polynomial.derivative F)‖ *
      (‖(Polynomial.aeval z) F‖ / ‖(Polynomial.aeval z) (Polynomial.derivative F)‖) ≤
    1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False

Tactic:
simpa using

Goal state after:
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
⊢ ↑(-((Polynomial.aeval z) (Polynomial.derivative F) *
          ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩)) =
    ↑(-⟨↑((Polynomial.aeval z) (Polynomial.derivative F)) *
            (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))),
          this⟩)

Tactic:
by simp only [PadicInt.coe_neg, PadicInt.coe_mul]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = (a.x ^ 2 - 1) * a₁.x

Tactic:
rw [← a.prop_y]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = d * a.y ^ 2 * a₁.x
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this✝ :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
this : (Polynomial.aeval z) (Polynomial.derivative F) * -z1 = -(Polynomial.aeval z) F
⊢ (Polynomial.aeval z') F = q * z1 ^ 2

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this✝ :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
this : (Polynomial.aeval z) (Polynomial.derivative F) * -z1 = -(Polynomial.aeval z) F
⊢ (Polynomial.aeval (z + -z1)) F = q * z1 ^ 2
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : (fun x ↦ 2 ^ x) 1 ≤ (fun x ↦ 2 ^ x) (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : (fun x ↦ 2 ^ x) 1 ≤ (fun x ↦ 2 ^ x) (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
⊢ v.IsEquiv (inftyValuation K)

Tactic:
by
  refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_
  rcases eq_or_ne f 0 with rfl | hf
  · simp
  · have hlt' : 1 < inftyValuation K X := by simp [← exp_zero]
    rw [valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt hf,
      valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X hlt' hf]
    grind [one_le_zpow_iff_right₀]

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ ∀ ⦃a : ℤ⦄, a ∈ {x | ∃ k, beattySeq r k = x} → a ∉ {x | ∃ k, beattySeq' s k = x}

Tactic:
intro j ⟨k, h₁⟩ ⟨m, h₂⟩

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : beattySeq r k = j
m : ℤ
h₂ : beattySeq' s m = j
⊢ False
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < ↑b.natDegree
⊢ a.natDegree < a.natDegree + b.natDegree

Tactic:
simpa using

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < ↑b.natDegree
⊢ 0 < b.natDegree
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simpa using

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k, beattySeq' r k = x}ᶜ = {x | ∃ k, beattySeq s k = x}

Tactic:
rw [← compl_beattySeq hrs.symm, compl_compl]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case h_ne
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ d.primeFactors.Nonempty

Tactic:
simp only [nonempty_primeFactors, show 1 < d by lia]

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case right
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := ⋯
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1

Tactic:
simpa using

Goal state after:
case right
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ↑π * v ↑(q / π) < 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ v ↑πᵥ ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ ¬πᵥ = 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
⊢ v ↑πᵥ ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
⊢ ¬πᵥ = 0
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
d e : ℕ
hd : (d, e) ∈ l.divisorsAntidiagonal
⊢ d * e = l ∧ ?m.92

Tactic:
simpa using

Goal state after:
s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
d e : ℕ
hd : (d, e) ∈ l.divisorsAntidiagonal
⊢ d * e = l ∧ ?m.92
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
⊢ d.Coprime e ∧ ?m.123

Tactic:
simpa using

Goal state after:
s : BoundingSieve
d e : ℕ
hl : Squarefree (d * e)
hnu_nonzero : s.nu (d * e) ≠ 0
hd : (d, e) ∈ (d * e).divisorsAntidiagonal
⊢ d.Coprime e ∧ ?m.123
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).re - ↑(round (toComplex x / toComplex y).re)| ≤ 2⁻¹

Tactic:
simpa using

Goal state after:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).re - ↑(round (toComplex x / toComplex y).re)| ≤ 2⁻¹
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).im - ↑(round (toComplex x / toComplex y).im)| ≤ 2⁻¹

Tactic:
simpa using

Goal state after:
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).im - ↑(round (toComplex x / toComplex y).im)| ≤ 2⁻¹
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case h
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
simpa using

Goal state after:
case h
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
⊢ ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
⊢ ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ (norm a).natAbs * (norm b).natAbs = p ^ 2

Tactic:
by
        rw [← Int.natCast_inj, Int.natCast_pow, sq, ← @norm_natCast (-1), hpab]; simp

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : (norm a).natAbs = p
⊢ a.re.natAbs ^ 2 + a.im.natAbs ^ 2 = p

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : (norm a).natAbs = p
⊢ a.re.natAbs * a.re.natAbs + a.im.natAbs * a.im.natAbs = p
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
simpa using

Goal state after:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hq : q ∈ b.primeFactors
hq4 : q % 4 = 3
this✝¹ : Fact (Prime q)
this✝ : n ≠ 0 → b.primeFactors ⊆ n.primeFactors
this : b.factorization q = 1
⊢ False

Tactic:
grind [factorization_def, prime_of_mem_primeFactors, padicValNat.mul, padicValNat.pow]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * 0
⊢ f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * 0
⊢ f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0