awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
hp : Continuous (Y := ℝ) fun (x : Completion E × Completion E) ↦ ‖-x.1 + x.2‖
⊢ IsClosed.{u_1} (X := Completion E × Completion E) {x : Completion E × Completion E | dist x.1 x.2 = ‖-x.1 + x.2‖}

Tactic:
refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_

Premises used: UniformSpace.Completion.uniformContinuous_extension₂, UniformContinuous.continuous, isClosed_eq
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
⊢ Continuous (Y := ℝ) fun (x : Completion E × Completion E) ↦ ‖-x.1 + x.2‖

Tactic:
Continuous.comp Completion.continuous_extension (continuous_neg.fst.add continuous_snd)

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, continuous_snd, UniformSpace.Completion.continuous_extension, Continuous.fst, Continuous.add
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
⊢ Continuous (Y := ℝ) fun (x : Completion E × Completion E) ↦ ‖-x.1 + x.2‖

Tactic:
exact Continuous.comp Completion.continuous_extension (continuous_neg.fst.add continuous_snd)

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, continuous_snd, UniformSpace.Completion.continuous_extension, Continuous.fst, Continuous.add
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
a b : E
ih :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (↑(-a) : Completion E) (↑b : Completion E)‖
ih₁ :
  dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = norm (E := Completion E) (↑(-a + b) : Completion E)
ih₂ : dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) = ‖-a + b‖
ih₃ : dist a b = ‖-a + b‖
ih₄ ih₅ : ‖-a + b‖ = ‖-a + b‖
⊢ dist (α := Completion E) (↑a : Completion E) (↑b : Completion E) =
    ‖HAdd.hAdd (α := Completion E) (-(↑a : Completion E)) (↑b : Completion E)‖

Tactic:
rw [← Completion.coe_neg, ← Completion.coe_add, norm_coe, Completion.dist_eq,
        dist_eq_norm_neg_add]

Premises used: UniformSpace.Completion.dist_eq, dist_eq_norm_neg_add, UniformSpace.Completion.norm_coe, UniformSpace.Completion.coe_neg, UniformSpace.Completion.coe_add
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
x : E
⊢ nnnorm (E := Completion E) (↑x : Completion E) = ‖x‖₊

Tactic:
simp [nnnorm]

Premises used: NNNorm.nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Completion
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
x : E
⊢ enorm (E := Completion E) (↑x : Completion E) = ‖x‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
x : PUnit.{u_5 + 1}
⊢ ‖x‖ = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : ULift.{u_5, u_2} E
⊢ ‖x‖ = ‖x.down‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : E
⊢ ‖{ down := x : ULift.{u_5, u_2} E }‖ = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : ULift.{u_5, u_2} E
⊢ ‖x.down‖ = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : ULift.{u_5, u_2} E
⊢ ‖x‖₊ = ‖x.down‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : E
⊢ ‖{ down := x : ULift.{u_5, u_2} E }‖₊ = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : ULift.{u_5, u_2} E
⊢ ‖x.down‖₊ = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : Additive E
⊢ norm (E := E) ((toMul : (a : Additive E) → E) x : E) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : E
⊢ norm (E := Additive E) ((ofMul : (a : E) → Additive E) x : Additive E) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : Multiplicative E
⊢ norm (E := E) ((toAdd : (a : Multiplicative E) → E) x : E) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : E
⊢ norm (E := Multiplicative E) ((ofAdd : (a : E) → Multiplicative E) x : Multiplicative E) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : Additive E
⊢ nnnorm (E := E) ((toMul : (a : Additive E) → E) x : E) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : E
⊢ nnnorm (E := Additive E) ((ofMul : (a : E) → Additive E) x : Additive E) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : Multiplicative E
⊢ nnnorm (E := E) ((toAdd : (a : Multiplicative E) → E) x : E) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : E
⊢ nnnorm (E := Multiplicative E) ((ofAdd : (a : E) → Multiplicative E) x : Multiplicative E) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : E
⊢ norm (E := Eᵒᵈ) ((toDual : (a : E) → Eᵒᵈ) x : Eᵒᵈ) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : Norm E
x : Eᵒᵈ
⊢ norm (E := E) ((ofDual : (a : Eᵒᵈ) → E) x : E) = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : E
⊢ nnnorm (E := Eᵒᵈ) ((toDual : (a : E) → Eᵒᵈ) x : Eᵒᵈ) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : NNNorm E
x : Eᵒᵈ
⊢ nnnorm (E := E) ((ofDual : (a : Eᵒᵈ) → E) x : E) = ‖x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : Norm F
x : E × F
⊢ ‖x‖ = max ‖x.1‖ ‖x.2‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : Norm F
x : E
y : F
⊢ ‖(x, y)‖ = max ‖x‖ ‖y‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : Norm F
x : E × F
⊢ ‖x.1‖ ≤ ‖x‖

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : Norm F
x : E × F
⊢ ‖x.2‖ ≤ ‖x‖

Tactic:
le_max_right _ _

Premises used: le_max_right
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : Norm E
inst_1 : Norm F
x : E × F
r : ℝ
⊢ ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r

Tactic:
max_le_iff

Premises used: max_le_iff
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
G : ι → Type u_4
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x y : E × F
⊢ dist x y = ‖x⁻¹ * y‖

Tactic:
simp [Prod.norm_def, Prod.dist_eq, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Prod.dist_eq, Prod.norm_def
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E × F
⊢ ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, NNReal.mk, rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
x : E
y : F
⊢ ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊

Tactic:
rfl

Premises used: Set.Ici, Set.Mem, setOf, NNReal.mk, rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
⊢ ‖f‖ = (↑(Finset.sup Finset.univ fun (b : ι) ↦ ‖f b‖₊) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
⊢ ‖f‖₊ = Finset.sup Finset.univ fun (b : ι) ↦ ‖f b‖₊

Tactic:
Subtype.eta _ _

Premises used: NNReal.mk, NNReal, Subtype.eta, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
x : (i : ι) → G i
r : ℝ
hr : 0 ≤ r
⊢ ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

Tactic:
simp only [← dist_one_right, dist_pi_le_iff hr, Pi.one_apply]

Premises used: Pi.one_apply, dist_pi_le_iff, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
x : (i : ι) → G i
r : ℝ≥0
⊢ ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

Tactic:
pi_norm_le_iff_of_nonneg' r.coe_nonneg

Premises used: pi_norm_le_iff_of_nonneg', NNReal.coe_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
pos : ∀ (hr : 0 ≤ r), ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
neg : ∀ (hr : ¬0 ≤ r), ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
by_cases hr : 0 ≤ r
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
pi_norm_le_iff_of_nonneg' hr

Premises used: pi_norm_le_iff_of_nonneg'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
hr : 0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
exact pi_norm_le_iff_of_nonneg' hr

Premises used: pi_norm_le_iff_of_nonneg'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
        hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

Premises used: norm_nonneg', iff_of_false, Classical.arbitrary, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst_2 : Nonempty ι
hr : ¬0 ≤ r
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
exact
      iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
        hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

Premises used: norm_nonneg', iff_of_false, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
x : (i : ι) → G i
r : ℝ
hr : 0 < r
⊢ ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

Tactic:
simp only [← dist_one_right, dist_pi_lt_iff hr, Pi.one_apply]

Premises used: Pi.one_apply, dist_pi_lt_iff, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
x : (i : ι) → G i
r : ℝ≥0
hr : 0 < r
⊢ ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

Tactic:
pi_norm_lt_iff' hr

Premises used: pi_norm_lt_iff'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
i : ι
⊢ ‖f i‖ ≤ ‖f‖

Tactic:
(pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).1 le_rfl i

Premises used: le_rfl, norm_nonneg', pi_norm_le_iff_of_nonneg', Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
i : ι
⊢ ‖f i‖₊ ≤ ‖f‖₊

Tactic:
norm_le_pi_norm' _ i

Premises used: norm_le_pi_norm'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : SeminormedGroup E
a : E
⊢ (norm (E := ι → E) fun (x : ι) ↦ a) ≤ ‖a‖

Tactic:
(pi_norm_le_iff_of_nonneg' <| norm_nonneg' _).2 fun _ => le_rfl

Premises used: Iff.mpr, le_rfl, norm_nonneg', pi_norm_le_iff_of_nonneg'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : SeminormedGroup E
a : E
⊢ (nnnorm (E := ι → E) fun (x : ι) ↦ a) ≤ ‖a‖₊

Tactic:
pi_norm_const_le' _

Premises used: pi_norm_const_le'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : SeminormedGroup E
inst_2 : Nonempty ι
a : E
⊢ (norm (E := (_i : ι) → E) fun (_i : ι) ↦ a) = ‖a‖

Tactic:
simpa only [← dist_one_right] using dist_pi_const a 1

Premises used: dist_pi_const, OfNat.ofNat, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : SeminormedGroup E
inst_2 : Nonempty ι
a : E
⊢ (nnnorm (E := (_i : ι) → E) fun (_i : ι) ↦ a) = ‖a‖₊

Tactic:
NNReal.eq <| pi_norm_const' a

Premises used: NNReal.eq, pi_norm_const'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
⊢ ∑ i : ι, ‖f i‖ ≤ Fintype.card ι • ‖f‖

Tactic:
Finset.sum_le_card_nsmul _ _ _ fun i _hi => norm_le_pi_norm' _ i

Premises used: Fintype.card, Finset.sum_le_card_nsmul, norm_le_pi_norm'
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
⊢ ∑ i : ι, ‖f i‖₊ ≤ Fintype.card ι • ‖f‖₊

Tactic:
(NNReal.coe_sum ..).trans_le <| Pi.sum_norm_apply_le_norm' _

Premises used: Pi.sum_norm_apply_le_norm', Eq.trans_le, NNReal.coe_sum, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b

Tactic:
Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b

Premises used: NNNorm.nnnorm, Pi.apply_single
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
refine : ∀ (i : ι), Eq (α := ℝ≥0) ((fun (i : ι) (x : G i) ↦ ‖x‖₊) i 0) 0
⊢ ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b

Tactic:
refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b

Premises used: NNNorm.nnnorm, Pi.apply_single
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
b : ι
⊢ ∀ (i : ι), Eq (α := ℝ≥0) ((fun (i : ι) (x : G i) ↦ ‖x‖₊) i 0) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ∀ (b : ι), ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b

Tactic:
have H : ∀ b, ‖single i y b‖₊ = single (M := fun _ ↦ ℝ≥0) i ‖y‖₊ b := by
    intro b
    refine Pi.apply_single (fun i (x : G i) ↦ ‖x‖₊) ?_ i y b
    simp
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
H : ∀ (b : ι), ‖single (M := G) i y b‖₊ = single (M := fun (x : ι) ↦ ℝ≥0) i ‖y‖₊ b
⊢ ‖single (M := G) i y‖₊ = ‖y‖₊

Tactic:
simp [Pi.nnnorm_def, H, Pi.single_apply, Finset.sup_ite, Finset.filter_eq']

Premises used: Pi.single_apply, Finset.filter_eq', Pi.nnnorm_def, Finset.sup_ite
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ‖single (M := G) i y‖ₑ = ‖y‖ₑ

Tactic:
simp [enorm, Pi.nnnorm_single]

Premises used: Pi.nnnorm_single, ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
ι : Type u_1
G : ι → Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → NormedAddCommGroup (G i)
i : ι
y : G i
⊢ ‖single (M := G) i y‖ = ‖y‖

Tactic:
congr_arg Subtype.val <| Pi.nnnorm_single y

Premises used: Pi.nnnorm_single, congr_arg, Subtype.val
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : SeminormedAddGroup E
a : E
⊢ ‖op a‖ = ‖a‖

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : SeminormedAddGroup E
a : Eᵐᵒᵖ
⊢ ‖unop a‖ = ‖a‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : SeminormedAddGroup E
a : E
⊢ ‖op a‖₊ = ‖a‖₊

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Analysis.Normed.Group.Constructions
Goal:
E : Type u_2
inst : SeminormedAddGroup E
a : Eᵐᵒᵖ
⊢ ‖unop a‖₊ = ‖a‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
⊢ Continuous[inst, _] fun (a : E) ↦ ‖a‖ₑ

Tactic:
ContinuousENorm.continuous_enorm

Premises used: ContinuousENorm.continuous_enorm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
X : Type u_8
inst_2 : TopologicalSpace X
f : X → E
⊢ Continuous[inst_2, inst] f → Continuous[inst_2, _] fun (x : X) ↦ ‖f x‖ₑ

Tactic:
continuous_enorm.comp

Premises used: Continuous.comp, continuous_enorm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
X : Type u_8
inst_2 : TopologicalSpace X
f : X → E
a : X
h : ContinuousAt f a
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) a

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
X : Type u_8
inst_2 : TopologicalSpace X
f : X → E
s : Set X
a : X
h : ContinuousWithinAt f s a
x : X
h_1 : x ∈ s
⊢ Membership.mem (γ := Set E) Set.univ (f x)

Tactic:
trivial
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
X : Type u_8
inst_2 : TopologicalSpace X
f : X → E
s : Set X
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : X) ↦ ‖f x‖ₑ) s

Tactic:
(ContinuousENorm.continuous_enorm.continuousOn).comp (t := Set.univ) h <| Set.mapsTo_univ _ _

Premises used: Continuous.continuousOn, Set.mapsTo_univ, ContinuousENorm.continuous_enorm, ContinuousOn.comp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (β := ℝ) (fun (e : α) ↦ ‖(f e)⁻¹ * b‖) a (𝓝 0)

Tactic:
simp only [← dist_eq_norm_inv_mul, ← tendsto_iff_dist_tendsto_zero]

Premises used: dist_eq_norm_inv_mul, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (β := ℝ) (fun (e : α) ↦ ‖(f e)⁻¹ * 1‖) a (𝓝 0) ↔ Tendsto (β := ℝ) (fun (x : α) ↦ ‖f x‖) a (𝓝 0)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
⊢ Eq.{u_4 + 1} (α := Filter E) (comap norm (𝓝 0)) (𝓝 1)

Tactic:
simpa only [dist_one_right] using nhds_comap_dist (1 : E)

Premises used: nhds_comap_dist, OfNat.ofNat, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
f : α → E
a : α → ℝ
t₀ : Filter α
h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n
h' : Tendsto a t₀ (𝓝 0)
⊢ Tendsto f t₀ (𝓝 1)

Tactic:
tendsto_one_iff_norm_tendsto_zero.2 <|
    squeeze_zero' (Eventually.of_forall fun _n => norm_nonneg' _) h h'

Premises used: Iff.mpr, norm_nonneg', Filter.Eventually.of_forall, tendsto_one_iff_norm_tendsto_zero, squeeze_zero'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
f : α → E
a : α → ℝ
t₀ : Filter α
h : ∀ (n : α), ‖f n‖ ≤ a n
⊢ Tendsto a t₀ (𝓝 0) → Tendsto f t₀ (𝓝 1)

Tactic:
squeeze_one_norm' <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, squeeze_one_norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
⊢ Tendsto (β := ℝ) (fun (a : E) ↦ ‖a⁻¹ * x‖) (𝓝 x) (𝓝 0)

Tactic:
simpa [dist_eq_norm_inv_mul] using
    tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

Premises used: Filter.tendsto_id, tendsto_const_nhds, dist_eq_norm_inv_mul, Filter.Tendsto.dist
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, Membership.mem (γ := Set ℝ) (Set.Ici 0) ‖n⁻¹ * x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
⊢ Tendsto (fun (a : E) ↦ ‖a‖) (𝓝 x) (𝓝 ‖x‖)

Tactic:
simpa using tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (1 : E)) _ _)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.dist
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
⊢ Tendsto (β := ℝ) (fun (a : E) ↦ ‖a‖) (𝓝 1) (𝓝 0)

Tactic:
simpa using tendsto_norm_inv_mul_self (1 : E)

Premises used: tendsto_norm_inv_mul_self, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (a : E) ↦ ‖a‖

Tactic:
simpa using continuous_id.dist (continuous_const : Continuous fun _a => (1 : E))

Premises used: continuous_const, Continuous.dist, continuous_id
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (a : E) ↦ ‖a‖₊

Tactic:
continuous_norm'.subtype_mk _

Premises used: NNReal.mk, NNReal, Continuous.subtype_mk, continuous_norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F_1 : Type u_5
G : Type u_6
F : Type u_7
inst : NormedGroup F
⊢ enorm.{u_7} (E := F) 1 = 0

Tactic:
simp [enorm_eq_nnnorm]

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F_1 : Type u_5
G : Type u_6
F : Type u_7
inst : NormedGroup F
⊢ ∀ (x y : F), ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

Tactic:
simp [enorm_eq_nnnorm, ← coe_add, nnnorm_mul_le']

Premises used: nnnorm_mul_le', ENNReal.coe_add, enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
E : Type u_4
F_1 : Type u_5
G : Type u_6
F : Type u_7
inst : NormedGroup F
⊢ ∀ (x : F), ‖x‖ₑ = 0 ↔ x = 1

Tactic:
simp [enorm_eq_nnnorm]

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
u v : E
h : Inseparable u v
⊢ ‖u‖ = ‖v‖

Tactic:
h.map continuous_norm' |>.eq

Premises used: Inseparable.eq, continuous_norm', Inseparable.map
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
u v : E
h : Inseparable u v
⊢ ‖u‖₊ = ‖v‖₊

Tactic:
h.map continuous_nnnorm' |>.eq

Premises used: Inseparable.eq, continuous_nnnorm', Inseparable.map
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_7
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
u v : E
h : Inseparable u v
⊢ ‖u‖ₑ = ‖v‖ₑ

Tactic:
h.map continuous_enorm |>.eq

Premises used: Inseparable.eq, continuous_enorm, Inseparable.map