awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Approximation
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NormedField L
inst_2 : Algebra K L
hd : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h_1 : ¬f.natDegree = 0
c : (i : ℕ) → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L : (a : K) → L) (c i)) < ε
hdeg :
  ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree +
        ∑ i ∈ Finset.Iio f.natDegree,
          HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)).natDegree =
    f.natDegree
n : ℕ
h : f.natDegree < n
⊢ ‖coeff
          (map (algebraMap K L)
            ((C : (a : K) → K[X]) 1 * HPow.hPow (α := K[X]) X f.natDegree +
              ∑ i ∈ Finset.Iio f.natDegree,
                HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (c i) : K[X]) (HPow.hPow (α := K[X]) X i)))
          n -
        f.coeff n‖ <
    ε

Tactic:
simp [not_lt_of_gt h, ne_of_gt h, coeff_eq_zero_of_natDegree_lt h, hε]

Premises used: ne_of_gt, Polynomial.coeff_eq_zero_of_natDegree_lt, not_lt_of_gt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NormedDivisionRing α
a b : α
rw : ‖HMul.hMul (α := α) 1 1‖ = norm.{u_2} (E := α) 1 * 1
rw₁ : norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1
rw₂ rw₃ : norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1
⊢ norm.{u_2} (E := α) 1 * norm.{u_2} (E := α) 1 = norm.{u_2} (E := α) 1 * 1

Tactic:
rw [← norm_mul, mul_one, mul_one]

Premises used: norm_mul, mul_one
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a b : α
⊢ ‖a / b‖ = ‖a‖ / ‖b‖

Tactic:
map_div₀ (normHom : α →*₀ ℝ) a b

Premises used: map_div₀, normHom
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a b : α
⊢ ‖a / b‖₊ = ‖a‖₊ / ‖b‖₊

Tactic:
map_div₀ (nnnormHom : α →*₀ ℝ≥0) a b

Premises used: NNReal.mk, map_div₀, nnnormHom
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a : α
⊢ ‖a⁻¹‖ = ‖a‖⁻¹

Tactic:
map_inv₀ (normHom : α →*₀ ℝ) a

Premises used: map_inv₀, normHom
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a : α
⊢ (↑‖a⁻¹‖₊ : ℝ) = (↑‖a‖₊⁻¹ : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Tactic:
simp [enorm, ENNReal.coe_inv, ha]

Premises used: ENNReal.coe_inv, ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
⊢ ∀ (a : α) (n : ℤ), ‖a ^ n‖ = ‖a‖ ^ n

Tactic:
map_zpow₀ (normHom : α →*₀ ℝ)

Premises used: map_zpow₀, normHom
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
⊢ ∀ (a : α) (n : ℤ), ‖a ^ n‖₊ = ‖a‖₊ ^ n

Tactic:
map_zpow₀ (nnnormHom : α →*₀ ℝ≥0)

Premises used: NNReal.mk, nnnormHom, map_zpow₀
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
rw : ‖z⁻¹ - w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₁ : ‖z⁻¹ * (w - z) * w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₂ : ‖z⁻¹ * (w - z)‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₃ : ‖z⁻¹‖ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₄ : ‖z‖⁻¹ * ‖w - z‖ * ‖w⁻¹‖ = dist z w / (‖z‖ * ‖w‖)
rw₅ : ‖z‖⁻¹ * ‖w - z‖ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₆ : ‖w - z‖ * ‖z‖⁻¹ * ‖w‖⁻¹ = dist z w / (‖z‖ * ‖w‖)
rw₇ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = dist z w / (‖z‖ * ‖w‖)
rw₈ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ / (‖z‖ * ‖w‖)
rw₉ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖ * ‖w‖)⁻¹
rw₁₀ rw₁₁ : ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹) = ‖w - z‖ * (‖z‖⁻¹ * ‖w‖⁻¹)
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹,
    mul_assoc, dist_eq_norm', div_eq_mul_inv, mul_inv]

Premises used: Norm.norm, dist_eq_norm, mul_inv, mul_assoc, dist_eq_norm', norm_mul, div_eq_mul_inv, norm_inv, Inv.inv, inv_sub_inv', mul_comm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)

Tactic:
NNReal.eq <| dist_inv_inv₀ hz hw

Premises used: dist_inv_inv₀, NNReal.eq
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Tactic:
simpa using norm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

Premises used: Units.mk0, norm_commutator_units_sub_one_le
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

Tactic:
simpa using nnnorm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

Premises used: Units.mk0, nnnorm_commutator_units_sub_one_le
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
mp : ‖x‖ = 1 → x ≠ 0
mpr : x ≠ 0 → ‖x‖ = 1
⊢ ‖x‖ = 1 ↔ x ≠ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : ‖x‖ = 1
mp : ∀ (hx : x = 0), ‖x‖ ≠ 1
⊢ x ≠ 0

Tactic:
contrapose! hx
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x = 0
⊢ ‖x‖ ≠ 1

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}

Tactic:
have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}
⊢ ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0

Tactic:
simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this

Premises used: dist_eq_norm, sub_zero, Metric.isOpen_singleton_iff
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
this : ∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0
mpr : ∀ (ε : ℝ) (εpos : ε > 0) (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0), ‖x‖ = 1
⊢ ‖x‖ = 1

Tactic:
obtain ⟨ε, εpos, h'⟩ := this
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
mpr :
  ∀
    (H :
      ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
        (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1)
    (h : 1 ≤ ‖x‖), ‖x‖ = 1
wlog! :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
⊢ ‖x‖ = 1

Tactic:
wlog! h : ‖x‖ < 1 generalizing 𝕜 with H
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h : 1 ≤ ‖x‖
mpr : ∀ (h : 1 = ‖x‖), ‖x‖ = 1
mpr₁ : ∀ (h : 1 < ‖x‖), ‖x‖ = 1
⊢ ‖x‖ = 1

Tactic:
rcases h.eq_or_lt with h | h

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : 1 = ‖x‖
mpr mpr₁ : ‖x‖ = ‖x‖
⊢ ‖x‖ = 1

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : 1 < ‖x‖
⊢ ‖x⁻¹‖ < 1

Tactic:
replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : ‖x⁻¹‖ < 1
mpr : ‖x⁻¹‖ = 1
⊢ ‖x‖ = 1

Tactic:
rw [← inv_inj, inv_one, ← norm_inv]

Premises used: inv_one, norm_inv, inv_inj
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : ‖x⁻¹‖ < 1
⊢ x⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜} (hx : x ≠ 0)
    (h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0) (h : ‖x‖ < 1), ‖x‖ = 1
h_1 : 1 ≤ ‖x‖
h : ‖x⁻¹‖ < 1
⊢ ‖x⁻¹‖ = 1

Tactic:
exact H (by simpa) h' h
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
⊢ ∃ (k : ℕ), ‖x‖ ^ k < ε

Tactic:
exists_pow_lt_of_lt_one εpos h

Premises used: exists_pow_lt_of_lt_one
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
obtain : ∀ (k : ℕ) (hk : ‖x‖ ^ k < ε), ‖x‖ = 1
⊢ ‖x‖ = 1

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h

Premises used: exists_pow_lt_of_lt_one
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x‖ ^ k < ε
⊢ ‖x ^ k‖ < ε

Tactic:
rw [← norm_pow] at hk

Premises used: norm_pow
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x ^ k‖ < ε
⊢ x ^ k = 0

Tactic:
specialize h' _ hk
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜_1 : Type u_5
inst : NormedDivisionRing 𝕜_1
ε : ℝ
εpos : ε > 0
𝕜 : Type u_5
inst_1 : NormedDivisionRing 𝕜
inst_2 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
h : ‖x‖ < 1
k : ℕ
hk : ‖x ^ k‖ < ε
h' : x ^ k = 0
⊢ ‖x‖ = 1

Tactic:
simp [hx] at h'
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
inl : norm.{u_5} (E := 𝕜) 0 ≤ 1
inr : ∀ (hx : x ≠ 0), ‖x‖ ≤ 1
⊢ ‖x‖ ≤ 1

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
⊢ norm.{u_5} (E := 𝕜) 0 ≤ 1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
⊢ ‖x‖ ≤ 1

Tactic:
simp [norm_eq_one_iff_ne_zero_of_discrete.mpr hx]

Premises used: Iff.mpr, NormedDivisionRing.norm_eq_one_iff_ne_zero_of_discrete
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
h : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 1) x ↔ Membership.mem (γ := Set 𝕜) Set.univ x
⊢ Eq.{u_5 + 1} (α := Set 𝕜) (Metric.closedBall 0 1) Set.univ

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
𝕜 : Type u_5
inst : NormedDivisionRing 𝕜
inst_1 : DiscreteTopology 𝕜
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Metric.closedBall 0 1) x ↔ Membership.mem (γ := Set 𝕜) Set.univ x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 1 < ‖x‖

Tactic:
‹NontriviallyNormedField α›.non_trivial

Premises used: NontriviallyNormedField.non_trivial
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 1 < ‖x‖₊

Tactic:
exists_one_lt_norm α

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 1 < ‖x‖ₑ

Tactic:
exists_one_lt_nnnorm α |>.imp fun _ => ENNReal.coe_lt_coe.mpr

Premises used: Iff.mpr, ENNReal.coe_lt_coe, Exists.imp, NormedField.exists_one_lt_nnnorm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
rwa rwa₁ rwa₂ rwa₃ : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖

Tactic:
rwa [norm_pow]

Premises used: norm_pow
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0
⊢ ∃ (x : α), r < ‖x‖₊

Tactic:
exists_lt_norm α r

Premises used: NormedField.exists_lt_norm, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0∞
hr : r ≠ ∞
⊢ r ≠ ∞

Tactic:
hr
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0∞
hr : r ≠ ∞
lift : ∀ (r : ℝ≥0), ∃ (x : α), (↑r : ℝ≥0∞) < ‖x‖ₑ
⊢ ∃ (x : α), r < ‖x‖ₑ

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0
⊢ ∃ (x : α), (↑r : ℝ≥0∞) < ‖x‖ₑ

Tactic:
mod_cast exists_lt_nnnorm α r

Premises used: congrArg, cast, Exists, funext, Eq.symm, coe_lt_enorm._simp_1, NormedField.exists_lt_nnnorm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0
⊢ ∃ (x : α), (↑r : ℝ≥0∞) < ‖x‖ₑ

Tactic:
exact mod_cast exists_lt_nnnorm α r

Premises used: NormedField.exists_lt_nnnorm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
rwa : ‖w⁻¹‖ ∈ Set.Ioo 0 r
rwa₁ : ‖w‖⁻¹ ∈ Set.Ioo 0 r
rwa₂ : ‖w‖ ∈ (Set.Ioo 0 r)⁻¹
rwa₃ rwa₄ rwa₅ rwa₆ : ‖w‖ ∈ Set.Ioi r⁻¹
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]

Premises used: Set.mem_Ioo, norm_inv, Set.inv_Ioo_0_left, Set.mem_inv
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0
hr : 0 < r
⊢ ∃ (x : α), 0 < ‖x‖₊ ∧ ‖x‖₊ < r

Tactic:
exists_norm_lt α hr

Premises used: NormedField.exists_norm_lt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
r : ℝ≥0∞
hr : 0 < r
⊢ ∃ (x : α), 0 < ‖x‖ₑ ∧ ‖x‖ₑ < r

Tactic:
match r with
  | ∞ => exists_one_lt_enorm α |>.imp fun _ hx => ⟨zero_le_one.trans_lt hx, ENNReal.coe_lt_top⟩
  | (r : ℝ≥0) => exists_nnnorm_lt α (ENNReal.coe_pos.mp hr) |>.imp fun _ =>
    And.imp ENNReal.coe_pos.mpr ENNReal.coe_lt_coe.mpr

Premises used: Iff.mpr, And.imp, NormedField.exists_one_lt_enorm, NormedField.exists_nnnorm_lt, Exists, ENNReal.coe_lt_coe, Exists.imp, zero_le_one, ENNReal.coe_pos, And, ENorm.enorm, And.intro, LT.lt, Iff.mp, OfNat.ofNat, LE.le.trans_lt, _private.0.NormedField.exists_enorm_lt.match_1, ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 0 < ‖x‖ ∧ ‖x‖ < 1

Tactic:
exists_norm_lt α one_pos

Premises used: NormedField.exists_norm_lt, one_pos
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 0 < ‖x‖₊ ∧ ‖x‖₊ < 1

Tactic:
exists_norm_lt_one _

Premises used: NormedField.exists_norm_lt_one
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ ∃ (x : α), 0 < ‖x‖ₑ ∧ ‖x‖ₑ < 1

Tactic:
exists_enorm_lt _ one_pos

Premises used: NormedField.exists_enorm_lt, one_pos
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
rw : ∀ ε > 0, ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
⊢ (𝓝[≠] x).NeBot

Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]

Premises used: Metric.mem_closure_iff, mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
rcases : ∀ (b : α) (hb0 : 0 < ‖b‖) (hbε : ‖b‖ < ε), ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε
⊢ ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε

Tactic:
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩

Premises used: NormedField.exists_norm_lt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε

Tactic:
⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩

Premises used: norm_pos_iff, mt, Set.mem_singleton_iff, add_eq_left, HAdd.hAdd, And.intro, Exists.intro, Iff.mp, Iff.trans
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
refine : dist x (x + b) < ε
⊢ ∃ (b : α), Membership.mem (γ := Set α) {x}ᶜ b ∧ dist x b < ε

Tactic:
refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
rwa : dist (x + b) x < ε
rwa₁ : ‖x + b - x‖ < ε
rwa₂ rwa₃ rwa₄ rwa₅ : ‖b‖ < ε
⊢ dist x (x + b) < ε

Tactic:
rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]

Premises used: dist_eq_norm, add_sub_cancel_left, dist_comm
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : NontriviallyNormedField α
⊢ NeBot.{u_2} (α := α) (𝓝[{x : α | IsUnit x}] 0)

Tactic:
simpa only [isUnit_iff_ne_zero] using nhdsNE_neBot (0 : α)

Premises used: NormedField.nhdsNE_neBot, isUnit_iff_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : DenselyNormedField α
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
h : r₁ < r₂
⊢ ∃ (x : α), r₁ < ‖x‖ ∧ ‖x‖ < r₂

Tactic:
DenselyNormedField.lt_norm_lt r₁ r₂ h₀ h

Premises used: DenselyNormedField.lt_norm_lt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
α : Type u_2
inst : DenselyNormedField α
r₁ r₂ : ℝ≥0
h : r₁ < r₂
⊢ ∃ (x : α), r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂

Tactic:
mod_cast exists_lt_norm_lt α r₁.prop h

Premises used: NNNorm.nnnorm, cast, Exists, And, Subtype.prop, LT.lt, Eq.refl, NormedField.exists_lt_norm_lt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯)
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯)
let :
  ∀ (z : α)
    (h : ‖x‖ < ‖z‖ ∧ ‖z‖ < (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯) : ℝ)),
    ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
      Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯ < a ∧
        a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯

Tactic:
let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯)
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯)
z : α
h : ‖x‖ < ‖z‖ ∧ ‖z‖ < (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯) : ℝ)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯

Tactic:
⟨⟨‖z‖, z, rfl⟩, h⟩

Premises used: Norm.norm, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯)
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯)
z : α
h : ‖x‖ < ‖z‖ ∧ ‖z‖ < (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯) : ℝ)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) norm) : Type)),
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖x‖ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) norm) ‖y‖ ⋯

Tactic:
exact ⟨⟨‖z‖, z, rfl⟩, h⟩
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type))
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯)
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯)
let :
  ∀ (z : α)
    (h :
      (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯) : ℝ≥0) < ‖z‖₊ ∧
        ‖z‖₊ < (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯) : ℝ≥0)),
    ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
      Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯ < a ∧
        a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
    Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯

Tactic:
let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type))
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯)
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯)
z : α
h :
  (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯) : ℝ≥0) < ‖z‖₊ ∧
    ‖z‖₊ < (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯) : ℝ≥0)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
    Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯

Tactic:
⟨⟨‖z‖₊, z, rfl⟩, h⟩

Premises used: NNNorm.nnnorm, Subtype.mk, Exists.intro, rfl