awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
h : HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
⊢ HasSum (fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) (HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n))

Tactic:
convert! (summable_sum_mul_range_of_summable_norm' hf h'f hg h'g).hasSum

Premises used: summable_sum_mul_range_of_summable_norm', Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g

Premises used: tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
R : Type u_1
inst : NormedRing R
f g : ℕ → R
hf : Summable (α := ℝ) fun (x : ℕ) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ℕ) ↦ ‖g x‖
h'g : Summable g
⊢ HMul.hMul (α := R) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)

Tactic:
exact tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm' hf h'f hg h'g

Premises used: tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm'
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Summable f

Tactic:
.of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩

Premises used: Iff.mpr, Summable.of_norm, Exists.intro, hasSum_iff_tendsto_nat_of_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
refine_1 : ∀ (i : ℕ), 0 ≤ ‖f i‖
refine_2 : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)
⊢ Summable f

Tactic:
refine .of_norm ⟨r, (hasSum_iff_tendsto_nat_of_nonneg ?_ _).2 ?_⟩
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

Tactic:
fun i ↦ norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

Tactic:
exact fun i ↦ norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.InfiniteSum
Goal:
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, ‖f i‖) atTop (𝓝 r)

Tactic:
simpa only using hr
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
e : ℤˣ
inl : nnnorm (E := ℤ) (↑1 : ℤ) = 1
inr : nnnorm (E := ℤ) (↑(-1) : ℤ) = 1
⊢ ‖(↑e : ℤ)‖₊ = 1

Tactic:
obtain rfl | rfl := units_eq_one_or e

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
⊢ nnnorm (E := ℤ) (↑1 : ℤ) = 1

Tactic:
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]

Premises used: Units.coe_neg_one, nnnorm_one, nnnorm_neg, Units.val_one
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
⊢ nnnorm (E := ℤ) (↑(-1) : ℤ) = 1

Tactic:
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]

Premises used: Units.coe_neg_one, nnnorm_one, nnnorm_neg, Units.val_one
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
e : ℤˣ
rw : (↑‖(↑e : ℤ)‖₊ : ℝ) = 1
rw₁ : (↑1 : ℝ) = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ ‖(↑e : ℤ)‖ = 1

Tactic:
rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]

Premises used: coe_nnnorm, Int.nnnorm_coe_units, NNReal.coe_one
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
n : ℕ
⊢ nnnorm (E := ℤ) (↑n : ℤ) = (↑n : NNReal)

Tactic:
Real.nnnorm_natCast _

Premises used: Real.nnnorm_natCast
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
n : ℕ
⊢ enorm (E := ℤ) (↑n : ℤ) = (↑n : ENNReal)

Tactic:
Real.enorm_natCast _

Premises used: Real.enorm_natCast
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
n : ℤ
rw : (↑(n.toNat + (-n).toNat) : NNReal) = ‖n‖₊
rw₁ : (↑n.natAbs : NNReal) = ‖n‖₊
rw₂ rw₃ : ‖n‖₊ = ‖n‖₊
⊢ HAdd.hAdd (α := NNReal) (↑n.toNat : NNReal) (↑(-n).toNat : NNReal) = ‖n‖₊

Tactic:
rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.natCast_natAbs]

Premises used: NNReal.natCast_natAbs, Nat.cast_add, Int.toNat_add_toNat_neg_eq_natAbs
-- Module: Mathlib.Analysis.Normed.Ring.Int
Goal:
n : ℤ
⊢ HAdd.hAdd (α := ℝ) (↑n.toNat : ℝ) (↑(-n).toNat : ℝ) = ‖n‖

Tactic:
simpa only [NNReal.coe_natCast, NNReal.coe_add] using
    congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)

Premises used: NNReal.coe_add, congrArg, NNReal.coe_natCast, Int.toNat_add_toNat_neg_eq_nnnorm, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
ι : Type u_3
inst : NonUnitalSeminormedRing α
f g : ι → α
l : Filter ι
hf : Tendsto f l (𝓝 0)
hg : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l ((fun (x : α) ↦ ‖x‖) ∘ g)
⊢ Tendsto.{u_3, u_1} (β := α) (fun (x : ι) ↦ f x * g x) l (𝓝 0)

Tactic:
hf.op_zero_isBoundedUnder_le hg (· * ·) norm_mul_le

Premises used: HMul.hMul, Filter.Tendsto.op_zero_isBoundedUnder_le, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
ι : Type u_3
inst : NonUnitalSeminormedRing α
f g : ι → α
l : Filter ι
hf : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l (norm ∘ f)
hg : Tendsto g l (𝓝 0)
⊢ Tendsto.{u_3, u_1} (β := α) (fun (x : ι) ↦ f x * g x) l (𝓝 0)

Tactic:
hg.op_zero_isBoundedUnder_le hf (flip (· * ·)) fun x y =>
    (norm_mul_le y x).trans_eq (mul_comm _ _)

Premises used: Norm.norm, HMul.hMul, LE.le.trans_eq, Filter.Tendsto.op_zero_isBoundedUnder_le, flip, mul_comm, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : SeminormedRing 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ
⊢ Isometry.{u_4, u_5} (α := 𝕜₁) (β := 𝕜₂) (⇑σ : (a : 𝕜₁) → 𝕜₂)

Tactic:
AddMonoidHomClass.isometry_of_norm _ fun _ => RingHomIsometric.norm_map

Premises used: AddMonoidHomClass.isometry_of_norm, RingHomIsometric.norm_map
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst : SeminormedRing 𝕜₁
inst_1 : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomIsometric σ
x : 𝕜₂
rw : norm.{u_5} (E := 𝕜₂) ((σ : (a : 𝕜₁) → 𝕜₂) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) : 𝕜₂) = ‖x‖
rw₁ rw₂ : ‖x‖ = ‖x‖
⊢ norm.{u_4} (E := 𝕜₁) ((σ' : (a : 𝕜₂) → 𝕜₁) x : 𝕜₁) = ‖x‖

Tactic:
rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]

Premises used: RingHomInvPair.comp_apply_eq₂, RingHomIsometric.norm_map
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
m : ℕ
hm : m ≠ 0
⊢ Tendsto (fun (x : α) ↦ x ^ m) (cobounded α) (cobounded α)

Tactic:
simpa [← tendsto_norm_atTop_iff_cobounded] using
    (tendsto_pow_atTop hm).comp (tendsto_norm_cobounded_atTop (E := α))

Premises used: tendsto_norm_cobounded_atTop, tendsto_norm_atTop_iff_cobounded, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 - x.1) * x.2‖
rw₁ : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - e.1 * x.2 + (e.1 * x.2 - x.1 * x.2)‖
rw₂ rw₃ : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * e.2 - x.1 * x.2‖
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖

Tactic:
rw [mul_sub, sub_mul, sub_add_sub_cancel]

Premises used: sub_add_sub_cancel, mul_sub, sub_mul
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖

Tactic:
norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)

Premises used: norm_add_le_of_le, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x e : α × α
rw : ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖

Tactic:
calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)

Premises used: HSub.hSub, Prod.fst, norm_add_le_of_le, Prod.snd
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
⊢ ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖

Tactic:
have : ∀ e : α × α,
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
          intro e
          calc
            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
              rw [mul_sub, sub_mul, sub_add_sub_cancel]
            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 * e.2 - (fun (p : α × α) ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
squeeze_zero (fun e => norm_nonneg _) this ?_

Premises used: squeeze_zero, HMul.hMul, HSub.hSub, Prod.fst, Prod.snd, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
refine : Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1‖ * ‖t.2 - x.2‖ + ‖t.1 - x.1‖ * ‖x.2‖) (𝓝 x) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (e : α × α) ↦ ‖e.1 * e.2 - (fun (p : α × α) ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
refine squeeze_zero (fun e => norm_nonneg _) this ?_

Premises used: squeeze_zero, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (fun (x_1 : α × α) ↦ ‖x_1.1‖ * ‖x_1.2 - x.2‖ + ‖x_1.1 - x.1‖ * ‖x.2‖) (𝓝 x)
    (𝓝 (‖x.1‖ * ‖x.2 - x.2‖ + ‖x.1 - x.1‖ * ‖x.2‖))

Tactic:
((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)

Premises used: tendsto_const_nhds, continuous_snd, continuous_fst, Filter.Tendsto.norm, Continuous.tendsto, Filter.Tendsto.mul, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
h : 0 = ‖x.1‖ * ‖x.2 - x.2‖ + ‖x.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (β := ℝ) (fun (t : α × α) ↦ ‖t.1‖ * ‖t.2 - x.2‖ + ‖t.1 - x.1‖ * ‖x.2‖) (𝓝 x) (𝓝 0)

Tactic:
convert!
          ((continuous_fst.tendsto x).norm.mul
                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)

Premises used: tendsto_const_nhds, continuous_snd, continuous_fst, Filter.Tendsto.norm, Continuous.tendsto, Filter.Tendsto.mul, Filter.Tendsto.add, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ 0 = ‖x.1‖ * ‖x.2 - x.2‖ + ‖x.1 - x.1‖ * ‖x.2‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
⊢ Isometry (Prod.map toReal toReal)

Tactic:
have : Isometry (Prod.map ((↑) : ℝ≥0 → ℝ) ((↑) : ℝ≥0 → ℝ)) :=
    NNReal.isometry_coe.prodMap NNReal.isometry_coe
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
this : Isometry (Prod.map toReal toReal)
⊢ LipschitzWith (β := ℝ) (HMul.hMul (α := ℝ≥0) 1 1 + HMul.hMul (α := ℝ≥0) 1 1) fun (x : ℝ≥0 × ℝ≥0) ↦
    max ((Prod.fst ∘ Prod.map toReal toReal) x - (Prod.snd ∘ Prod.map toReal toReal) x) 0

Tactic:
(((LipschitzWith.prod_fst.comp this.lipschitz).sub
          (LipschitzWith.prod_snd.comp this.lipschitz)).max_const
      0)

Premises used: LipschitzWith.max_const, LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzWith.sub, Isometry.lipschitz, LipschitzWith.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
this : Isometry (Prod.map toReal toReal)
h : 2 = HMul.hMul (α := ℝ≥0) 1 1 + HMul.hMul (α := ℝ≥0) 1 1
⊢ LipschitzWith (α := ℝ≥0 × ℝ≥0) 2 (toReal ∘ fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 - p.2)

Tactic:
convert!
    (((LipschitzWith.prod_fst.comp this.lipschitz).sub
          (LipschitzWith.prod_snd.comp this.lipschitz)).max_const
      0)

Premises used: LipschitzWith.max_const, LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzWith.sub, Isometry.lipschitz, LipschitzWith.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
this : Isometry (Prod.map toReal toReal)
⊢ 2 = HMul.hMul (α := ℝ≥0) 1 1 + HMul.hMul (α := ℝ≥0) 1 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m n : ℤ
⊢ ‖m * n‖ ≤ ‖m‖ * ‖n‖

Tactic:
simp only [norm, Int.cast_mul, abs_mul, le_rfl]

Premises used: Norm.norm, le_rfl, abs_mul, Int.cast_mul
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ norm (E := ℤ) 1 = 1

Tactic:
simp [← Int.norm_cast_real]

Premises used: Int.norm_cast_real
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
a b : ℤ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp [← Int.norm_cast_real, abs_mul]

Premises used: abs_mul, Int.norm_cast_real
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a : α
ha : a ≠ 0
x x_1 : α
⊢ dist x x_1 ≤ (↑‖a‖₊⁻¹ : ℝ) * dist (a * x) (a * x_1)

Tactic:
simp [dist_eq_norm, ← mul_sub, ha]

Premises used: dist_eq_norm, mul_sub
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a : α
ha : a ≠ 0
x x_1 : α
⊢ dist x x_1 ≤ (↑‖a‖₊⁻¹ : ℝ) * dist (x * a) (x_1 * a)

Tactic:
simp [dist_eq_norm, ← sub_mul, mul_comm, ha]

Premises used: dist_eq_norm, sub_mul, mul_comm
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a_1 a : α
ha : a ≠ 0
x y : α
⊢ edist (a * x) (a * y) = (↑‖a‖₊ : ENNReal) * edist x y

Tactic:
simp [edist_nndist, nndist_eq_nnnorm, ← mul_sub]

Premises used: mul_sub, nndist_eq_nnnorm, edist_nndist
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a_1 a : α
ha : a ≠ 0
x y : α
⊢ edist (x * a) (y * a) = (↑‖a‖₊ : ENNReal) * edist x y

Tactic:
simp [edist_nndist, nndist_eq_nnnorm, ← sub_mul, ← mul_comm (‖a‖₊)]

Premises used: NNNorm.nnnorm, sub_mul, mul_comm, nndist_eq_nnnorm, edist_nndist
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a : α
ha : a ≠ 0
⊢ comap (fun (x : α) ↦ a * x) (cobounded α) = cobounded α

Tactic:
Dilation.comap_cobounded (Dilation.mulLeft a ha)

Premises used: Dilation.comap_cobounded, Dilation.mulLeft
-- Module: Mathlib.Analysis.Normed.Ring.Lemmas
Goal:
α : Type u_1
inst : NonUnitalNormedRing α
inst_1 : NormMulClass α
a : α
ha : a ≠ 0
⊢ comap (fun (x : α) ↦ x * a) (cobounded α) = cobounded α

Tactic:
Dilation.comap_cobounded (Dilation.mulRight a ha)

Premises used: Dilation.mulRight, Dilation.comap_cobounded
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
x : R
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
simpa only [le_max_iff, norm_one] using norm_add_le_max x 1

Premises used: NormOneClass.norm_one, IsUltrametricDist.norm_add_le_max, OfNat.ofNat, le_max_iff
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
x : R
⊢ ‖x + 1‖₊ ≤ max ‖x‖₊ 1

Tactic:
norm_add_one_le_max_norm_one _

Premises used: IsUltrametricDist.norm_add_one_le_max_norm_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
⊢ nnnorm.{u_1} (E := R) (↑0 : R) ≤ 1

Tactic:
simp only [Nat.cast_zero, nnnorm_zero, zero_le]

Premises used: zero_le, nnnorm_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
n : ℕ
hn : nnnorm.{u_1} (E := R) (↑n : R) ≤ 1
⊢ nnnorm.{u_1} (E := R) (↑(n + 1) : R) ≤ 1

Tactic:
simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)

Premises used: IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, Nat.cast, max_eq_right, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
n : ℕ
zero : nnnorm.{u_1} (E := R) (↑0 : R) ≤ 1
succ : ∀ (n : ℕ) (hn : nnnorm.{u_1} (E := R) (↑n : R) ≤ 1), nnnorm.{u_1} (E := R) (↑(n + 1) : R) ≤ 1
⊢ nnnorm.{u_1} (E := R) (↑n : R) ≤ 1

Tactic:
induction n with
  | zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
  | succ n hn => simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)

Premises used: zero_le, IsUltrametricDist.nnnorm_add_one_le_max_nnnorm_one, Nat.cast, max_eq_right, Nat.cast_add, nnnorm_zero, Nat.cast_zero, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
n : ℕ
⊢ norm.{u_1} (E := R) (↑n : R) ≤ 1

Tactic:
nnnorm_natCast_le_one R n

Premises used: IsUltrametricDist.nnnorm_natCast_le_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
z : ℤ
ofNat : ∀ (a : ℕ), nnnorm.{u_1} (E := R) (↑(Int.ofNat a) : R) ≤ 1
negSucc : ∀ (a : ℕ), nnnorm.{u_1} (E := R) (↑(Int.negSucc a) : R) ≤ 1
⊢ nnnorm.{u_1} (E := R) (↑z : R) ≤ 1

Tactic:
cases z
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
a : ℕ
⊢ nnnorm.{u_1} (E := R) (↑(Int.ofNat a) : R) ≤ 1

Tactic:
simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

Premises used: Int.cast_natCast, Int.ofNat_eq_natCast, Int.cast_negSucc, nnnorm_neg, IsUltrametricDist.nnnorm_natCast_le_one, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
a : ℕ
⊢ nnnorm.{u_1} (E := R) (↑(Int.negSucc a) : R) ≤ 1

Tactic:
simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

Premises used: Int.cast_natCast, Int.ofNat_eq_natCast, Int.cast_negSucc, nnnorm_neg, IsUltrametricDist.nnnorm_natCast_le_one, Nat.cast_one
-- Module: Mathlib.Analysis.Normed.Ring.Ultra
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
z : ℤ
⊢ norm.{u_1} (E := R) (↑z : R) ≤ 1

Tactic:
nnnorm_intCast_le_one _ z

Premises used: IsUltrametricDist.nnnorm_intCast_le_one
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ Nontrivial R

Tactic:
nontriviality R using zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
⊢ 0 < ‖(↑x⁻¹ : R)‖

Tactic:
have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
rw rw₁ : ‖(↑x⁻¹ : R) * t‖ = ‖(↑x⁻¹ : R) * t‖
⊢ ‖-((↑x⁻¹ : R) * t)‖ = ‖(↑x⁻¹ : R) * t‖

Tactic:
rw [norm_neg]

Premises used: norm_neg
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
⊢ ‖(↑x⁻¹ : R) * t‖ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖

Tactic:
norm_mul_le (x⁻¹).1 _

Premises used: Units.val, Inv.inv, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
nlinarith nlinarith₁ : ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ → HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₂ :
  ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ →
    1 * ‖(↑x⁻¹ : R)‖ * (1 * ‖(↑x⁻¹ : R)‖⁻¹) - 1 * ‖(↑x⁻¹ : R)‖ * (1 * ‖t‖) +
        (0 - (1 * ‖t‖ - 1 * ‖(↑x⁻¹ : R)‖⁻¹) * (HMul.hMul (α := ℝ) 1 0 - 1 * ‖(↑x⁻¹ : R)‖)) =
      0
⊢ ‖(↑x⁻¹ : R)‖ * ‖t‖ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹

Tactic:
nlinarith only [h, hpos]
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
⊢ ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ = 1

Tactic:
mul_inv_cancel₀ (ne_of_gt hpos)

Premises used: mul_inv_cancel₀, ne_of_gt
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
by : ‖-((↑x⁻¹ : R) * t)‖ = ‖(↑x⁻¹ : R) * t‖
by₁ : ‖(↑x⁻¹ : R)‖ * ‖t‖ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹
⊢ ‖-((↑x⁻¹ : R) * t)‖ < 1

Tactic:
calc
        ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖ := by rw [norm_neg]
        _ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ := norm_mul_le (x⁻¹).1 _
        _ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
        _ = 1 := mul_inv_cancel₀ (ne_of_gt hpos)

Premises used: Units.val, HMul.hMul, mul_inv_cancel₀, ne_of_gt, Inv.inv, norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ (↑x : R) + t = (↑(x * oneSub (-((↑x⁻¹ : R) * t)) ⋯) : R)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
y : R
h : ‖y - (↑x : R)‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ y = (↑(x.add (y - (↑x : R)) h) : R)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
rw : ∀ (x : R), Membership.mem (γ := Set R) {x : R | IsUnit x} x → ∃ ε > 0, Metric.ball x ε ⊆ {x : R | IsUnit x}
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : R | IsUnit x}

Tactic:
rw [Metric.isOpen_iff]

Premises used: Metric.isOpen_iff
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
⊢ ∃ ε > 0, Metric.ball (↑x : R) ε ⊆ {x : R | IsUnit x}

Tactic:
⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩

Premises used: Iff.mpr, Norm.norm, Units.val, inv_pos, Inv.inv, And.intro, Exists.intro, Units.norm_pos