awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ ‖(b :: l).prod‖ ≤ (map norm (b :: l)).prod

Tactic:
exact List.norm_prod_le' (List.cons_ne_nil b l)

Premises used: List.cons_ne_nil
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
l : List α
hl : l ≠ []
⊢ (map norm l).prod = (↑(map nnnorm l).prod : ℝ)

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

Premises used: List.map_map, NNReal.coe_list_prod
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
⊢ norm.{u_2} (E := α) (prod []) ≤ (map.{u_2, 0} (α := α) norm []).prod

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
l : List α
⊢ (map norm l).prod = (↑(map nnnorm l).prod : ℝ)

Tactic:
simp [NNReal.coe_list_prod, List.map_map]

Premises used: List.map_map, NNReal.coe_list_prod
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
mk :
  ∀ (val : Multiset ι) (l : List ι) (hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l))
    (hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty),
    norm.{u_5} (E := α)
        (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
      ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖
⊢ norm.{u_5} (E := α) (∏ i ∈ s, f i) ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
f : ι → α
val : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty
⊢ List.map f l ≠ []

Tactic:
simpa using hs
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
f : ι → α
val : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty
⊢ List.map f l ≠ []

Tactic:
have : l.map f ≠ [] := by simpa using hs
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
f : ι → α
val : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
hs : { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }.Nonempty
this : List.map f l ≠ []
⊢ norm.{u_5} (E := α)
      (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖

Tactic:
simpa using List.norm_prod_le' this

Premises used: List.norm_prod_le'
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ Eq (α := ℝ) (∏ i ∈ s, ‖f i‖) (↑(∏ i ∈ s, ‖f i‖₊) : ℝ)

Tactic:
simp [NNReal.coe_prod]

Premises used: NNReal.coe_prod
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
inst_1 : NormOneClass α
s : Finset ι
f : ι → α
mk :
  ∀ (val : Multiset ι) (l : List ι) (hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)),
    norm.{u_5} (E := α)
        (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
      ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖
⊢ norm.{u_5} (E := α) (∏ i ∈ s, f i) ≤ ∏ i ∈ s, ‖f i‖

Tactic:
rcases s with ⟨⟨l⟩, hl⟩
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
inst_1 : NormOneClass α
f : ι → α
val : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l)
⊢ norm.{u_5} (E := α)
      (∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, f i) ≤
    ∏ i ∈ { val := Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) l, nodup := hl : Finset ι }, ‖f i‖

Tactic:
simpa using (l.map f).norm_prod_le

Premises used: List.norm_prod_le, List.map
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
ι : Type u_4
α : Type u_5
inst : NormedCommRing α
inst_1 : NormOneClass α
s : Finset ι
f : ι → α
⊢ Eq (α := ℝ) (∏ i ∈ s, ‖f i‖) (↑(∏ i ∈ s, ‖f i‖₊) : ℝ)

Tactic:
simp [NNReal.coe_prod]

Premises used: NNReal.coe_prod
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
inl : ∀ (hz : z = (↑z.natAbs : ℤ)), norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
inr : ∀ (hz : z = -(↑z.natAbs : ℤ)), norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)

Tactic:
rcases z.natAbs_eq with hz | hz

Premises used: Int.natAbs_eq
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = (↑z.natAbs : ℤ)
inl : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
inl₁ inl₂ : norm.{u_2} (E := α) (↑z : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)

Tactic:
rw [← Int.cast_natCast, ← hz]

Premises used: Int.cast_natCast
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
hz : z = -(↑z.natAbs : ℤ)
inr : norm.{u_2} (E := α) (↑(↑z.natAbs : ℤ) : α) = norm.{u_2} (E := α) (↑z : α)
inr₁ : norm.{u_2} (E := α) (-(↑(↑z.natAbs : ℤ) : α)) = norm.{u_2} (E := α) (↑z : α)
inr₂ : norm.{u_2} (E := α) (↑(-(↑z.natAbs : ℤ)) : α) = norm.{u_2} (E := α) (↑z : α)
inr₃ inr₄ : norm.{u_2} (E := α) (↑z : α) = norm.{u_2} (E := α) (↑z : α)
⊢ norm.{u_2} (E := α) (↑z.natAbs : α) = norm.{u_2} (E := α) (↑z : α)

Tactic:
rw [← Int.cast_natCast, ← norm_neg, ← Int.cast_neg, ← hz]

Premises used: Int.cast_neg, Int.cast_natCast, norm_neg
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
⊢ nnnorm.{u_2} (E := α) (↑z.natAbs : α) = nnnorm.{u_2} (E := α) (↑z : α)

Tactic:
simp [← NNReal.coe_inj, -Nat.cast_natAbs, norm_natAbs]

Premises used: Nat.cast_natAbs, norm_natAbs, NNReal.coe_inj
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
⊢ norm.{u_2} (E := α) (↑|z| : α) = norm.{u_2} (E := α) (↑z : α)

Tactic:
simp [← norm_natAbs]

Premises used: norm_natAbs
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
z : ℤ
⊢ nnnorm.{u_2} (E := α) (↑|z| : α) = nnnorm.{u_2} (E := α) (↑z : α)

Tactic:
simp [← nnnorm_natAbs]

Premises used: nnnorm_natAbs
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a : α
h : LT.lt (α := ℕ) 0 1
⊢ ‖HPow.hPow (β := ℕ) a 1‖₊ ≤ HPow.hPow (β := ℕ) ‖a‖₊ 1

Tactic:
simp only [pow_one, le_rfl]

Premises used: le_rfl, pow_one
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a : α
n : ℕ
h : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)

Tactic:
simpa only [pow_succ' _ (n + 1)] using
      le_trans (nnnorm_mul_le _ _) (mul_le_mul_right (nnnorm_pow_le' a n.succ_pos) _)

Premises used: nnnorm_mul_le, mul_le_mul_right, HAdd.hAdd, Nat.succ_pos, OfNat.ofNat, pow_succ', le_trans
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n

Tactic:
simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)

Premises used: nnnorm_pow_le', NNReal.coe_mono, coe_nnnorm, NNReal.coe_pow
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a : α
⊢ ∀ᶠ (n : ℕ) in atTop, ‖a ^ n‖ ≤ ‖a‖ ^ n

Tactic:
eventually_atTop.mpr ⟨1, fun _b h => norm_pow_le' a (Nat.succ_le_iff.mp h)⟩

Premises used: Iff.mpr, Exists.intro, Iff.mp, norm_pow_le', Filter.eventually_atTop, OfNat.ofNat, Nat.succ_le_iff
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Tactic:
simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)

Premises used: HMul.hMul, mul_one_sub, norm_sub_le_norm_sub_add_norm_sub
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
bc : ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖
⊢ ‖c - a‖ + ‖a * (1 - b)‖ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖

Tactic:
norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖a * (1 - b)‖ ≤ ‖a‖ * ‖1 - b‖

Tactic:
exact norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
bc : 0 ≤ ‖1 - b‖
⊢ ‖c - a‖ + ‖a‖ * ‖1 - b‖ ≤ ‖c - a‖ + 1 * ‖1 - b‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a‖ + 1 * ‖1 - b‖ = ‖c - a‖ + ‖1 - b‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
rw : ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖
⊢ ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Tactic:
norm_sub_mul_le (α := αᵐᵒᵖ) hb

Premises used: MulOpposite.unop, norm_sub_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
hb : ‖b‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - b‖ + ‖1 - a‖

Tactic:
exact norm_sub_mul_le (α := αᵐᵒᵖ) hb

Premises used: norm_sub_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
ha : ‖a‖₊ ≤ 1
⊢ ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊

Tactic:
norm_sub_mul_le ha

Premises used: norm_sub_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b c : α
hb : ‖b‖₊ ≤ 1
⊢ ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊

Tactic:
norm_sub_mul_le' hb

Premises used: norm_sub_mul_le'
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖(↑(a * b * a⁻¹ * b⁻¹) : α) - 1‖ = ‖((↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)) * (↑a⁻¹ : α) * (↑b⁻¹ : α)‖

Tactic:
simp [sub_mul, *]

Premises used: sub_mul
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
simp_rw :
  ‖(↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
    ‖(↑a : α) * (↑b : α) - (↑a : α) - ((↑b : α) - 1) - ((↑b : α) * (↑a : α) - (↑b : α) - ((↑a : α) - 1))‖ *
        ‖(↑a⁻¹ : α)‖ *
      ‖(↑b⁻¹ : α)‖
⊢ ‖(↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
    ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖

Tactic:
simp_rw [sub_one_mul, mul_sub_one]

Premises used: mul_sub_one, sub_one_mul
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖(↑a : α) * (↑b : α) - (↑b : α) * (↑a : α)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
    ‖(↑a : α) * (↑b : α) - (↑a : α) - ((↑b : α) - 1) - ((↑b : α) * (↑a : α) - (↑b : α) - ((↑a : α) - 1))‖ *
        ‖(↑a⁻¹ : α)‖ *
      ‖(↑b⁻¹ : α)‖

Tactic:
abel_nf
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
hbc :
  ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤
    ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ ≤
    (‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤
    ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖

Tactic:
norm_sub_le ..

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1) - ((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤
    ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖

Tactic:
exact norm_sub_le ..

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
hbc : ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ ≤ ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖
hbc₁ : ‖((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤ ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖
⊢ (‖((↑a : α) - 1) * ((↑b : α) - 1)‖ + ‖((↑b : α) - 1) * ((↑a : α) - 1)‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ ≤
    (‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖ + ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ ≤ ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖

Tactic:
norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑a : α) - 1) * ((↑b : α) - 1)‖ ≤ ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖

Tactic:
exact norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤ ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖

Tactic:
norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖((↑b : α) - 1) * ((↑a : α) - 1)‖ ≤ ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖

Tactic:
exact norm_mul_le ..

Premises used: norm_mul_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ (‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖ + ‖(↑b : α) - 1‖ * ‖(↑a : α) - 1‖) * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ =
    2 * ‖(↑a⁻¹ : α)‖ * ‖(↑b⁻¹ : α)‖ * ‖(↑a : α) - 1‖ * ‖(↑b : α) - 1‖

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
a b : αˣ
⊢ ‖(↑(a * b * a⁻¹ * b⁻¹) : α) - 1‖₊ ≤ 2 * ‖(↑a⁻¹ : α)‖₊ * ‖(↑b⁻¹ : α)‖₊ * ‖(↑a : α) - 1‖₊ * ‖(↑b : α) - 1‖₊

Tactic:
simpa using norm_commutator_units_sub_one_le a b

Premises used: norm_commutator_units_sub_one_le
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NormedRing α
inst_1 : Nontrivial α
x : αˣ
⊢ 0 < ‖(↑x : α)‖

Tactic:
norm_pos_iff.mpr (Units.ne_zero x)

Premises used: Iff.mpr, norm_pos_iff, Units.ne_zero
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NormedRing α
inst_1 : Nontrivial α
x : αˣ
⊢ 0 < ‖(↑x : α)‖₊

Tactic:
x.norm_pos

Premises used: Units.norm_pos
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
f : S → ℝ
hf_pm : IsPowMul f
x : ↥A
n : ℕ
hn : 1 ≤ n
⊢ (fun (x : ↥A) ↦ f (↑x : S)) (x ^ n) = HPow.hPow (α := ℝ) ((fun (x : ↥A) ↦ f (↑x : S)) x) n

Tactic:
simpa using hf_pm (↑x) hn

Premises used: Subtype.val
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
x : ℝ≥0
rw : |(↑x : ℝ)| = (↑x : ℝ)
rw₁ rw₂ : (↑x : ℝ) = (↑x : ℝ)
⊢ ‖(↑x : ℝ)‖ = (↑x : ℝ)

Tactic:
rw [Real.norm_eq_abs, x.abs_eq]

Premises used: NNReal.abs_eq, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
x : ℝ≥0
a : (↑‖(↑x : ℝ)‖₊ : ℝ) = (↑x : ℝ)
⊢ ‖(↑x : ℝ)‖₊ = x

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
x : ℝ≥0
⊢ (↑‖(↑x : ℝ)‖₊ : ℝ) = (↑x : ℝ)

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
x : ℝ≥0
⊢ ‖(↑x : ℝ)‖ₑ = (↑x : ENNReal)

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
β : Type u_5
inst_3 : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ (ia : α), True ∧ ∀ x ∈ Set.Ici ia, f x ∈ Metric.ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (N : α), ∀ (n : α), N ≤ n → ‖f n - b‖ < ε

Tactic:
simp [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : Nonempty α
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
inst_3 : NoMaxOrder α
β : Type u_5
inst_4 : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ (ia : α), True ∧ ∀ x ∈ Set.Ioi ia, f x ∈ Metric.ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (N : α), ∀ (n : α), N < n → ‖f n - b‖ < ε

Tactic:
simp [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R₁ : Type u_5
R₂ : Type u_6
inst : SeminormedRing R₁
inst_1 : SeminormedRing R₂
σ : R₁ →+* R₂
inst_2 : RingHomIsometric σ
x : R₁
⊢ nnnorm.{u_6} (E := R₂) ((σ : (a : R₁) → R₂) x : R₂) = ‖x‖₊

Tactic:
NNReal.eq norm_map

Premises used: NNReal.eq, RingHomIsometric.norm_map
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
R₁ : Type u_5
R₂ : Type u_6
inst : SeminormedRing R₁
inst_1 : SeminormedRing R₂
σ : R₁ →+* R₂
inst_2 : RingHomIsometric σ
x : R₁
⊢ enorm.{u_6} (E := R₂) ((σ : (a : R₁) → R₂) x : R₂) = ‖x‖ₑ

Tactic:
congrArg ENNReal.ofNNReal <| nnnorm_map σ x

Premises used: ENNReal.ofNNReal, congrArg, RingHomIsometric.nnnorm_map
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
inst : SeminormedRing R₁
⊢ RingHomIsometric (RingHom.id R₁)

Tactic:
⟨rfl⟩

Premises used: RingHomIsometric.mk, rfl
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : Norm α
inst_1 : Mul α
inst_2 : NormMulClass α
a b : α
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
NormMulClass.norm_mul a b

Premises used: NormMulClass.norm_mul
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedAddCommGroup α
inst_1 : Mul α
inst_2 : NormMulClass α
a b : α
⊢ ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊

Tactic:
NNReal.eq <| norm_mul a b

Premises used: NNReal.eq, norm_mul
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedAddCommGroup α
inst_1 : Mul α
inst_2 : NormMulClass α
a b : α
⊢ ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
a : α
⊢ ∀ (n : ℕ), ‖a ^ n‖ = ‖a‖ ^ n

Tactic:
(normHom.toMonoidHom : α →* ℝ).map_pow a

Premises used: MonoidWithZeroHom.toMonoidHom, normHom, MonoidHom.map_pow
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
a : α
n : ℕ
⊢ ‖a ^ n‖₊ = ‖a‖₊ ^ n

Tactic:
(nnnormHom.toMonoidHom : α →* ℝ≥0).map_pow a n

Premises used: NNReal.mk, MonoidWithZeroHom.toMonoidHom, nnnormHom, MonoidHom.map_pow
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
a : α
n : ℕ
⊢ ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
l : List α
⊢ ‖l.prod‖ = (map norm l).prod

Tactic:
map_list_prod (normHom.toMonoidHom : α →* ℝ) _

Premises used: map_list_prod, MonoidWithZeroHom.toMonoidHom, normHom
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : SeminormedRing α
inst_1 : NormOneClass α
inst_2 : NormMulClass α
l : List α
⊢ ‖l.prod‖₊ = (map nnnorm l).prod

Tactic:
map_list_prod (nnnormHom.toMonoidHom : α →* ℝ≥0) _

Premises used: NNReal.mk, map_list_prod, MonoidWithZeroHom.toMonoidHom, nnnormHom
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedCommRing α
inst_1 : NormMulClass α
inst_2 : NormOneClass α
s : Finset β
f : β → α
⊢ norm.{u_2} (E := α) (∏ b ∈ s, f b) = ∏ b ∈ s, ‖f b‖

Tactic:
map_prod normHom.toMonoidHom f s

Premises used: map_prod, MonoidWithZeroHom.toMonoidHom, normHom
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedCommRing α
inst_1 : NormMulClass α
inst_2 : NormOneClass α
s : Finset β
f : β → α
⊢ nnnorm.{u_2} (E := α) (∏ b ∈ s, f b) = ∏ b ∈ s, ‖f b‖₊

Tactic:
map_prod nnnormHom.toMonoidHom f s

Premises used: NNReal.mk, map_prod, MonoidWithZeroHom.toMonoidHom, nnnormHom
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NormedAddCommGroup α
inst_1 : MulOneClass α
inst_2 : NormMulClass α
inst_3 : Nontrivial α
obtain : ∀ (u : α) (hu : u ≠ 0), norm.{u_2} (E := α) 1 = 1
⊢ norm.{u_2} (E := α) 1 = 1

Tactic:
obtain ⟨u, hu⟩ := exists_ne (0 : α)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
α : Type u_2
inst : NormedAddCommGroup α
inst_1 : MulOneClass α
inst_2 : NormMulClass α
inst_3 : Nontrivial α
u : α
hu : u ≠ 0
⊢ norm.{u_2} (E := α) 1 = 1

Tactic:
simpa [mul_eq_left₀ (norm_ne_zero_iff.mpr hu)] using (norm_mul u 1).symm

Premises used: Iff.mpr, mul_eq_left₀, norm_mul, norm_ne_zero_iff, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : NormedRing α
inst_1 : NormMulClass α
a b : α
h : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
simpa only [← norm_eq_zero (E := α), norm_mul, mul_eq_zero] using h

Premises used: norm_eq_zero, norm_mul, mul_eq_zero
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
F : Type u_8
R : Type u_9
S : Type u_10
inst : Ring R
inst_1 : SeminormedRing S
inst_2 : NormOneClass S
inst_3 : FunLike F R S
inst_4 : RingHomClass F R S
f : F
⊢ NormOneClass R

Tactic:
let _ : SeminormedRing R := SeminormedRing.induced R S f
  { norm_one := (congr_arg norm (map_one f)).trans norm_one }

Premises used: Norm.norm, NormOneClass.mk, NormOneClass.norm_one, congr_arg, map_one, SeminormedRing.induced, Eq.trans
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
F : Type u_8
R : Type u_9
S : Type u_10
inst : Ring R
inst_1 : SeminormedRing S
inst_2 : NormMulClass S
inst_3 : FunLike F R S
inst_4 : RingHomClass F R S
f : F
⊢ NormMulClass R

Tactic:
let _ : SeminormedRing R := SeminormedRing.induced R S f
  { norm_mul x y := (congr_arg norm (map_mul f x y)).trans <| norm_mul _ _ }

Premises used: Norm.norm, NormMulClass.mk, norm_mul, congr_arg, map_mul, SeminormedRing.induced, DFunLike.coe, Eq.trans
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
S : Type u_5
R : Type u_6
inst : SetLike S R
inst_1 : SeminormedRing R
inst_2 : NormOneClass R
inst_3 : SubringClass S R
s : S
⊢ NormOneClass.{u_6} ↥s

Tactic:
.induced s R <| SubringClass.subtype _

Premises used: SubringClass.subtype, Membership.mem, Subtype, NormOneClass.induced
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
S : Type u_5
R : Type u_6
inst : SetLike S R
inst_1 : SeminormedRing R
inst_2 : NormMulClass R
inst_3 : SubringClass S R
s : S
⊢ NormMulClass.{u_6} ↥s

Tactic:
.induced s R <| SubringClass.subtype _

Premises used: SubringClass.subtype, Membership.mem, Subtype, NormMulClass.induced
-- Module: Mathlib.Analysis.Normed.Ring.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
R : Type u_5
inst : Ring R
v : AbsoluteValue R ℝ
x : R
⊢ Eq (α := ℝ) ((v : (a : R) → ℝ) (-x + x) : ℝ) (0 : ℝ)

Tactic:
simp