awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Premises used: norm_nonneg', le_ciSup_of_le, Nonempty.some
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Premises used: norm_nonneg', le_ciSup_of_le, Nonempty.some
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
h_bd : ¬BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
neg neg₁ : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
rw [Real.iSup_of_not_bddAbove h_bd]

Premises used: Real.iSup_of_not_bddAbove
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)

Tactic:
have h_bd : BddAbove (Set.range fun i ↦ ‖f i‖) :=
    h.tendsto_cofinite_one.norm'.bddAbove_range_of_cofinite
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)

Premises used: Filter.Tendsto.norm', Multipliable.hasProd, le_of_tendsto', IsUltrametricDist.norm_prod_le_of_forall_le_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
pos : ∀ (s : Finset ι), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
pos₁ : ∀ (s : Finset ι), ∀ i ∈ s, ‖f i‖ ≤ ⨆ (i : ι), ‖f i‖
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)

Premises used: Filter.Tendsto.norm', Multipliable.hasProd, le_of_tendsto', IsUltrametricDist.norm_prod_le_of_forall_le_of_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
s : Finset ι
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Premises used: norm_nonneg', le_ciSup_of_le, Nonempty.some
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
s : Finset ι
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
exact le_ciSup_of_le h_bd hι.some (norm_nonneg' _)

Premises used: norm_nonneg', le_ciSup_of_le, Nonempty.some
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
s : Finset ι
⊢ ∀ i ∈ s, ‖f i‖ ≤ ⨆ (i : ι), ‖f i‖

Tactic:
fun i _ ↦ le_ciSup h_bd i

Premises used: le_ciSup
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)
s : Finset ι
⊢ ∀ i ∈ s, ‖f i‖ ≤ ⨆ (i : ι), ‖f i‖

Tactic:
exact fun i _ ↦ le_ciSup h_bd i

Premises used: le_ciSup
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
⊢ nnnorm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, coe_nnnorm', coe_iSup] using norm_tprod_le f

Premises used: NNReal.coe_iSup, coe_nnnorm', IsUltrametricDist.norm_tprod_le, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
inst_2 : Nonempty ι
f : ι → M
C : ℝ
h : ∀ (i : ι), ‖f i‖ ≤ C
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
(norm_tprod_le f).trans (ciSup_le h)

Premises used: IsUltrametricDist.norm_tprod_le, LE.le.trans, ciSup_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
inl : IsEmpty ι → norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
inr : Nonempty ι → norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
rcases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h_1 : IsEmpty ι
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
simpa only [tprod_empty, norm_one'] using hC

Premises used: norm_one', tprod_empty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h_1 : Nonempty ι
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
norm_tprod_le_of_forall_le h

Premises used: IsUltrametricDist.norm_tprod_le_of_forall_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
C : ℝ
hC : 0 ≤ C
h : ∀ (i : ι), ‖f i‖ ≤ C
h_1 : Nonempty ι
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
exact norm_tprod_le_of_forall_le h

Premises used: IsUltrametricDist.norm_tprod_le_of_forall_le
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
C : ℝ≥0
h : ∀ (i : ι), ‖f i‖₊ ≤ C
⊢ nnnorm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C

Tactic:
(nnnorm_tprod_le f).trans (ciSup_le' h)

Premises used: ciSup_le', IsUltrametricDist.nnnorm_tprod_le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) = Finset.sup ∅ fun (i : ι) ↦ ‖f i‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
cons :
  ∀ (ha : a ∉ ∅)
    (IH :
      ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
        nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) = Finset.sup ∅ fun (i : ι) ↦ ‖f i‖₊)
    (hs : (↑(Finset.cons a ∅ ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a ∅ ha, f i) = (Finset.cons a ∅ ha).sup fun (i : ι) ↦ ‖f i‖₊
cons₁ :
  ∀ (hs' : s.Nonempty),
    nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs'

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
ha : a ∉ ∅
IH :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) = Finset.sup ∅ fun (i : ι) ↦ ‖f i‖₊
hs : (↑(Finset.cons a ∅ ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a ∅ ha, f i) = (Finset.cons a ∅ ha).sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
⊢ (↑s : Set ι) ⊆ (↑(Finset.cons a s ha) : Set ι)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
specialize IH (hs.mono (by simp))

Premises used: Set.Pairwise.mono
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
⊢ ∃ j ∈ s, nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊

Tactic:
simpa [IH] using s.exists_mem_eq_sup hs' _

Premises used: Finset.exists_mem_eq_sup
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
cons :
  ∀ (j : ι) (hj : j ∈ s) (hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
obtain ⟨j, hj, hj'⟩ : ∃ j ∈ s, ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊ := by
      simpa [IH] using s.exists_mem_eq_sup hs' _
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
this : ‖f a‖₊ ≠ nnnorm.{u_1} (E := M) (∏ x ∈ s, f x)
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]

Premises used: IsUltrametricDist.nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
cons : ‖f a‖₊ ≠ nnnorm.{u_1} (E := M) (∏ x ∈ s, f x)
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
suffices ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊ by simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
cons : ‖f a‖₊ ≠ ‖f j‖₊
⊢ ‖f a‖₊ ≠ nnnorm.{u_1} (E := M) (∏ x ∈ s, f x)

Tactic:
rw [hj']
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
cons : a ∈ (↑(Finset.cons a s ha) : Set ι)
cons₁ : j ∈ (↑(Finset.cons a s ha) : Set ι)
cons₂ : a ≠ j
⊢ ‖f a‖₊ ≠ ‖f j‖₊

Tactic:
apply hs
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
⊢ a ∈ (↑(Finset.cons a s ha) : Set ι)

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
⊢ j ∈ (↑(Finset.cons a s ha) : Set ι)

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
IH : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
j : ι
hj : j ∈ s
hj' : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = ‖f j‖₊
⊢ a ≠ j

Tactic:
grind
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) = Finset.sup ∅ fun (i : ι) ↦ ‖f i‖₊
cons :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (IH :
      ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
        nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊)
    (hs : (↑(Finset.cons a s ha) : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊),
    nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊

Tactic:
induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | hs'
    · simp
    specialize IH (hs.mono (by simp))
    obtain ⟨j, hj, hj'⟩ : ∃ j ∈ s, ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊ := by
      simpa [IH] using s.exists_mem_eq_sup hs' _
    suffices ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊ by simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]
    rw [hj']
    apply hs <;> grind

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖ ≠ ‖f j‖
rw : (↑(s.sup' hs' fun (i : ι) ↦ ‖f i‖₊) : ℝ) = s.sup' hs' fun (i : ι) ↦ ‖f i‖
rw₁ : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup' hs' fun (i : ι) ↦ ‖f i‖

Tactic:
rw [← coe_nnnorm', nnnorm_prod_eq_sup_of_pairwise_ne, ← Finset.sup'_eq_sup hs']

Premises used: coe_nnnorm', IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_ne, Finset.sup'_eq_sup
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖ ≠ ‖f j‖
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ : ∀ (x y : ℝ≥0), (↑(max x y) : ℝ) = max (↑x : ℝ) (↑y : ℝ)
⊢ ∀ (x y : ℝ≥0), (↑(max x y) : ℝ) = max (↑x : ℝ) (↑y : ℝ)

Tactic:
tauto
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑(s.sup' hs' fun (i : ι) ↦ ‖f i‖₊) : ℝ) = s.sup' hs' fun (i : ι) ↦ ‖f i‖

Tactic:
exact s.comp_sup'_eq_sup'_comp hs' _ (by tauto)

Premises used: Finset.comp_sup'_eq_sup'_comp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
hs' : s.Nonempty
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖ ≠ ‖f j‖
⊢ (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊

Tactic:
simpa [← NNReal.coe_inj] using hs

Premises used: NNReal.coe_inj
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
s : Set E
a_1 b_1 : E
r : ℝ
a b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
simp [dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
rw : dist (f x) 1 = ‖x‖
rw₁ : dist (f x) (f 1) = ‖x‖
rw₂ : dist x 1 = ‖x‖
rw₃ rw₄ : ‖x‖ = ‖x‖
⊢ ‖f x‖ = ‖x‖

Tactic:
rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]

Premises used: Isometry.dist_eq, dist_one_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : IsometryClass 𝓕 E F
inst_4 : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
(IsometryClass.isometry f).norm_map_of_map_one (map_one f) x

Premises used: map_one, Isometry.norm_map_of_map_one, IsometryClass.isometry
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : IsometryClass 𝓕 E F
inst_4 : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ nnnorm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖₊

Tactic:
NNReal.eq <| norm_map' f x

Premises used: norm_map', NNReal.eq
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : IsometryClass 𝓕 E F
inst_4 : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ enorm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖ₑ

Tactic:
simp [enorm]

Premises used: ENorm.enorm
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
rw : dist b (b * a) = dist 1 a
rw₁ : dist b (b * a) = dist (b * 1) (b * a)
rw₂ rw₃ : dist b (b * a) = dist b (b * a)
⊢ dist b (b * a) = ‖a‖

Tactic:
rw [← dist_one_left, ← dist_mul_left b 1 a, mul_one]

Premises used: dist_mul_left, dist_one_left, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
rw : dist b (b * a) = ‖a‖
rw₁ rw₂ : ‖a‖ = ‖a‖
⊢ dist (b * a) b = ‖a‖

Tactic:
rw [dist_comm, dist_self_mul_right]

Premises used: dist_comm, dist_self_mul_right
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
x y : E
⊢ dist.{u_3} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F) ≤ C * dist x y

Tactic:
simpa only [dist_eq_norm_inv_mul, map_mul, map_inv] using h (x⁻¹ * y)

Premises used: HMul.hMul, map_inv, dist_eq_norm_inv_mul, map_mul, Inv.inv
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
s : Set E
f : E → F
C : ℝ≥0
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ (↑C : ℝ) * ‖x⁻¹ * y‖

Tactic:
simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, lipschitzOnWith_iff_dist_le_mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
s : Set E
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a⁻¹ * b‖ ≤ r
ha₁ : 0 ≤ (↑C : ℝ)
⊢ (↑C : ℝ) * ‖a⁻¹ * b‖ ≤ (↑C : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
f : E → F
C : ℝ≥0
⊢ LipschitzWith C f ↔ ∀ (x y : E), ‖(f x)⁻¹ * f y‖ ≤ (↑C : ℝ) * ‖x⁻¹ * y‖

Tactic:
simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzWith C f
hr : ‖a⁻¹ * b‖ ≤ r
ha : 0 ≤ (↑C : ℝ)
⊢ (↑C : ℝ) * ‖a⁻¹ * b‖ ≤ (↑C : ℝ) * r

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : E) → F)

Tactic:
(MonoidHomClass.lipschitz_of_bound f C h).continuous

Premises used: LipschitzWith.continuous, MonoidHomClass.lipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ UniformContinuous.{u_2, u_3} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
(MonoidHomClass.lipschitz_of_bound f C h).uniformContinuous

Premises used: LipschitzWith.uniformContinuous, MonoidHomClass.lipschitz_of_bound
-- Module: Mathlib.Analysis.Normed.Group.Uniform
Goal:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst : SeminormedGroup E
inst_1 : SeminormedGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : MonoidHomClass 𝓕 E F
f : 𝓕
simp :
  (∀ (x y : E), norm.{u_3} (E := F) ((f : (a : E) → F) (x⁻¹ * y) : F) = ‖x⁻¹ * y‖) ↔
    ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖
⊢ Isometry.{u_2, u_3} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    ∀ (x : E), norm.{u_3} (E := F) ((f : (a : E) → F) x : F) = ‖x‖

Tactic:
simp only [isometry_iff_dist_eq, dist_eq_norm_inv_mul, ← map_inv, ← map_mul]

Premises used: map_inv, dist_eq_norm_inv_mul, isometry_iff_dist_eq, map_mul