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
s : Finset ι
hs : s.Nonempty
f : ι → M
simp : ∃ b ∈ s, norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ ‖f b‖
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup' hs fun (x : ι) ↦ ‖f x‖

Tactic:
simp only [Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff
-- 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
j : ι
⊢ ∃ (b : ι), Membership.mem (γ := Finset ι) {j} b ∧ norm.{u_1} (E := M) (∏ i ∈ {j}, f i) ≤ ‖f b‖

Tactic:
simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]

Premises used: Finset.mem_singleton, le_refl, Finset.prod_singleton, exists_eq_left
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
cons : ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
⊢ ∃ b ∈ Finset.cons j t hj, norm.{u_1} (E := M) (∏ i ∈ Finset.cons j t hj, f i) ≤ ‖f b‖

Tactic:
simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]

Premises used: exists_eq_or_imp, Finset.prod_cons, Finset.mem_cons
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
(le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_

Premises used: Norm.norm, le_total, Finset.prod, Or.imp
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
cons : norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f j‖ → ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖
cons₁ : ‖f j‖ ≤ norm.{u_1} (E := M) (∏ i ∈ t, f i) → ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_

Premises used: Norm.norm, le_total, Finset.prod, Or.imp
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
h : norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f j‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

Tactic:
(norm_mul_le_max _ _).trans (max_eq_left h).le

Premises used: Eq.le, max_eq_left, IsUltrametricDist.norm_mul_le_max, LE.le.trans
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
h : norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f j‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖

Tactic:
exact (norm_mul_le_max _ _).trans (max_eq_left h).le

Premises used: Eq.le, max_eq_left, IsUltrametricDist.norm_mul_le_max, LE.le.trans
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
h : ‖f j‖ ≤ norm.{u_1} (E := M) (∏ i ∈ t, f i)
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩

Premises used: Exists.choose_spec, Eq.le, max_eq_right, And.right, And.left, And.intro, Exists.intro, IsUltrametricDist.norm_mul_le_max, LE.le.trans
-- 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
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
h : ‖f j‖ ≤ norm.{u_1} (E := M) (∏ i ∈ t, f i)
⊢ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖

Tactic:
exact ⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
singleton : ∀ (j : ι), ∃ (b : ι), Membership.mem (γ := Finset ι) {j} b ∧ norm.{u_1} (E := M) (∏ i ∈ {j}, f i) ≤ ‖f b‖
cons :
  ∀ (j : ι) (t : Finset ι) (hj : j ∉ t),
    t.Nonempty →
      ∀ (IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖),
        ∃ b ∈ Finset.cons j t hj, norm.{u_1} (E := M) (∏ i ∈ Finset.cons j t hj, f i) ≤ ‖f b‖
⊢ ∃ b ∈ s, norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ ‖f b‖

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton j => simp only [Finset.mem_singleton, Finset.prod_singleton, exists_eq_left, le_refl]
  | cons j t hj _ IH =>
      simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]
      refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_ <;> intro h
      · exact (norm_mul_le_max _ _).trans (max_eq_left h).le
      · exact ⟨_, IH.choose_spec.left, (norm_mul_le_max _ _).trans <|
          ((max_eq_right h).le.trans IH.choose_spec.right)⟩

Premises used: Finset.mem_singleton, le_refl, Finset.prod_singleton, exists_eq_left, exists_eq_or_imp, Finset.prod_cons, Singleton.singleton, Finset.mem_cons
-- 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
inl : nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) ≤ Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
inr : ∀ (hs : s.Nonempty), nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup fun (x : ι) ↦ ‖f x‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup fun (x : ι) ↦ ‖f x‖₊

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
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) ≤ Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp
-- 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
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
simpa only [← Finset.sup'_eq_sup hs, Finset.le_sup'_iff, coe_le_coe, coe_nnnorm']
      using hs.norm_prod_le_sup'_norm f

Premises used: Finset.le_sup'_iff, coe_nnnorm', Finset.Nonempty.norm_prod_le_sup'_norm, Finset.sup'_eq_sup, 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
s : Finset ι
f : ι → M
C : ℝ≥0
hC : ∀ i ∈ s, ‖f i‖₊ ≤ C
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ C

Tactic:
(s.nnnorm_prod_le_sup_nnnorm f).trans <| Finset.sup_le hC

Premises used: Finset.sup_le, LE.le.trans, Finset.nnnorm_prod_le_sup_nnnorm
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
C : ℝ
hC : ∀ i ∈ s, ‖f i‖ ≤ C
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ C

Tactic:
(hs.norm_prod_le_sup'_norm f).trans (Finset.sup'_le hs _ hC)

Premises used: Finset.sup'_le, Finset.Nonempty.norm_prod_le_sup'_norm, LE.le.trans
-- 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
C : ℝ
h_nonneg : 0 ≤ C
hC : ∀ i ∈ s, ‖f i‖ ≤ C
⊢ 0 ≤ C

Tactic:
h_nonneg
-- 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
C : ℝ
h_nonneg : 0 ≤ C
hC : ∀ i ∈ s, ‖f i‖ ≤ C
lift : ∀ (C : ℝ≥0) (hC : ∀ i ∈ s, ‖f i‖ ≤ (↑C : ℝ)), norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ (↑C : ℝ)
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ C

Tactic:
lift C to NNReal using h_nonneg

Premises used: NNReal
-- 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
C : ℝ≥0
hC : ∀ i ∈ s, ‖f i‖ ≤ (↑C : ℝ)
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ (↑C : ℝ)

Tactic:
nnnorm_prod_le_of_forall_le hC

Premises used: NNReal.toReal, IsUltrametricDist.nnnorm_prod_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
s : Finset ι
f : ι → M
C : ℝ≥0
hC : ∀ i ∈ s, ‖f i‖ ≤ (↑C : ℝ)
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ (↑C : ℝ)

Tactic:
exact nnnorm_prod_le_of_forall_le hC

Premises used: IsUltrametricDist.nnnorm_prod_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
t : Finset ι
ht : t.Nonempty
f : ι → M
⊢ ∃ i ∈ t, norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖

Tactic:
match t.exists_mem_eq_sup' ht (‖f ·‖) with
  | ⟨j, hj, hj'⟩ => ⟨j, hj, (ht.norm_prod_le_sup'_norm f).trans (le_of_eq hj')⟩

Premises used: Norm.norm, _private.0.IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty.match_1, Membership.mem, Exists, LE.le, Finset.prod, And, And.intro, Finset.Nonempty.norm_prod_le_sup'_norm, Exists.intro, Finset.exists_mem_eq_sup', LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
t : Finset ι
inst_2 : Nonempty ι
f : ι → M
inl :
  ∃ (i : ι),
    (Finset.Nonempty.{u_2} (α := ι) ∅ → Membership.mem (γ := Finset ι) ∅ i) ∧ norm.{u_1} (E := M) (∏ j ∈ ∅, f j) ≤ ‖f i‖
inr : ∀ (ht : t.Nonempty), ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖
⊢ ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖

Tactic:
rcases t.eq_empty_or_nonempty with rfl | ht

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
inst_2 : Nonempty ι
f : ι → M
⊢ ∃ (i : ι),
    (Finset.Nonempty.{u_2} (α := ι) ∅ → Membership.mem (γ := Finset ι) ∅ i) ∧ norm.{u_1} (E := M) (∏ j ∈ ∅, f j) ≤ ‖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
t : Finset ι
inst_2 : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖

Tactic:
(fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finsetProd_le_of_nonempty ht f

Premises used: IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
t : Finset ι
inst_2 : Nonempty ι
f : ι → M
ht : t.Nonempty
⊢ ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖

Tactic:
exact (fun ⟨i, h, h'⟩ => ⟨i, fun _ ↦ h, h'⟩) <| exists_norm_finsetProd_le_of_nonempty ht f

Premises used: IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Multiset ι
inst_2 : Nonempty ι
f : ι → M
inhabit : ∀ (inhabited_h : Inhabited ι), ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
⊢ ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Tactic:
inhabit ι
-- 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
inhabited_h : Inhabited ι
⊢ ∃ (i : ι),
    (Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 i) ∧ ‖(Multiset.map f 0).prod‖ ≤ ‖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
inst_2 : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
hM : ∃ (i : ι), (t ≠ 0 → i ∈ t) ∧ ‖(Multiset.map f t).prod‖ ≤ ‖f i‖
cons :
  ∀ (M_1 : ι) (hMs : t ≠ 0 → M_1 ∈ t) (hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M_1‖),
    ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
obtain ⟨M, hMs, hM⟩ := hM
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
pos : ∀ (hMa : ‖f M‖ ≤ ‖f a‖), ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
neg : ∀ (hMa : ‖f a‖ < ‖f M‖), ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
by_cases! hMa : ‖f M‖ ≤ ‖f a‖
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ a ::ₘ t ≠ 0 → a ∈ a ::ₘ t

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
pos : ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
refine ⟨a, by simp, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
pos : ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖

Tactic:
le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))

Premises used: le_refl, max_le, IsUltrametricDist.norm_mul_le_max, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f M‖ ≤ ‖f a‖
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖

Tactic:
exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))

Premises used: le_refl, max_le, IsUltrametricDist.norm_mul_le_max, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
neg :
  ∀ (hMs : Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 M)
    (hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖),
    ∃ (i : ι), (a ::ₘ 0 ≠ 0 → i ∈ a ::ₘ 0) ∧ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f i‖
neg₁ : ∀ (ht : t ≠ 0), ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
rcases eq_or_ne t 0 with rfl | ht

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 M
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ a ::ₘ 0 ≠ 0 → a ∈ a ::ₘ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 M
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f a‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a M : ι
hMa : ‖f a‖ < ‖f M‖
hMs : Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 M
hM : ‖(Multiset.map f 0).prod‖ ≤ ‖f M‖
⊢ ∃ (i : ι), (a ::ₘ 0 ≠ 0 → i ∈ a ::ₘ 0) ∧ ‖(Multiset.map f (a ::ₘ 0)).prod‖ ≤ ‖f i‖

Tactic:
exact ⟨a, by simp, by simp⟩
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
⟨M, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
neg : a ::ₘ t ≠ 0 → M ∈ a ::ₘ t
neg₁ : ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f M‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖

Tactic:
refine ⟨M, ?_, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ a ::ₘ t ≠ 0 → M ∈ a ::ₘ t

Tactic:
simp [hMs ht]
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
neg : ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f M‖

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons]

Premises used: Multiset.map_cons, Multiset.prod_cons
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖

Tactic:
le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

Premises used: LT.lt.le, max_le, IsUltrametricDist.norm_mul_le_max, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M_1 : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M_1
inst_1 : IsUltrametricDist M_1
inst_2 : Nonempty ι
f : ι → M_1
inhabited_h : Inhabited ι
a : ι
t : Multiset ι
M : ι
hMs : t ≠ 0 → M ∈ t
hM : ‖(Multiset.map f t).prod‖ ≤ ‖f M‖
hMa : ‖f a‖ < ‖f M‖
ht : t ≠ 0
⊢ ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖

Tactic:
exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

Premises used: LT.lt.le, max_le, IsUltrametricDist.norm_mul_le_max, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Multiset ι
inst_2 : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
empty :
  ∃ (i : ι),
    (Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 i) ∧ ‖(Multiset.map f 0).prod‖ ≤ ‖f i‖
cons :
  ∀ (a : ι) (t : Multiset ι) (hM : ∃ (i : ι), (t ≠ 0 → i ∈ t) ∧ ‖(Multiset.map f t).prod‖ ≤ ‖f i‖),
    ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
⊢ ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons a t hM =>
      obtain ⟨M, hMs, hM⟩ := hM
      by_cases! hMa : ‖f M‖ ≤ ‖f a‖
      · refine ⟨a, by simp, ?_⟩
        · rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le (le_refl _) (le_trans hM hMa))
      · rcases eq_or_ne t 0 with rfl | ht
        · exact ⟨a, by simp, by simp⟩
        · refine ⟨M, ?_, ?_⟩
          · simp [hMs ht]
          rw [Multiset.map_cons, Multiset.prod_cons]
          exact le_trans (norm_mul_le_max _ _) (max_le hMa.le hM)

Premises used: Multiset.map_cons, Multiset.prod_cons, rfl
-- Module: Mathlib.Analysis.Normed.Group.Ultra
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
inl : ∀ (hι : IsEmpty ι), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
inr : ∀ (hι : Nonempty ι), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι

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
hι : IsEmpty ι
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
simp only [tprod_empty, norm_one', Real.iSup_of_isEmpty, le_refl]

Premises used: le_refl, norm_one', tprod_empty, Real.iSup_of_isEmpty
-- 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 ι
pos : ∀ (h : Multipliable f), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
neg : ∀ (h : ¬Multipliable f), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
by_cases h : Multipliable f

Premises used: Multipliable, SummationFilter.unconditional
-- 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
neg : LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖

Tactic:
rw [tprod_eq_one_of_not_multipliable h, norm_one']

Premises used: norm_one', tprod_eq_one_of_not_multipliable
-- 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
pos : ∀ (h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
neg : ∀ (h_bd : ¬BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)

Tactic:
by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)

Premises used: Norm.norm, BddAbove, Set.range