awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
have cons₁ : ‖f j‖ ≤ norm.{u_1} (E := M) (∏ i ∈ t, f i) → ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
Tactic: refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
⊢ ∃ b ∈ s, norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ ‖f b‖
have singleton : ∀ (j : ι), ∃ (b : ι), Membership.mem (γ := Finset ι) {j} b ∧ norm.{u_1} (E := M) (∏ i ∈ {j}, 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)⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ b ∈ s, norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ ‖f b‖
have 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‖
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)⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup fun (x : ι) ↦ ‖f x‖₊
have inl : nnnorm.{u_1} (E := M) (∏ i ∈ ∅, f i) ≤ Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup fun (x : ι) ↦ ‖f x‖₊
have inr : ∀ (hs : s.Nonempty), 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ C
have lift : ∀ (C : ℝ≥0) (hC : ∀ i ∈ s, ‖f i‖ ≤ (↑C : ℝ)), norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ (↑C : ℝ)
Tactic: lift C to NNReal using h_nonneg
Cleared hypotheses: C, h_nonneg, hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
t : Finset ι
inst_2 : Nonempty ι
f : ι → M
⊢ ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖
have inl : ∃ (i : ι),
  (Finset.Nonempty.{u_2} (α := ι) ∅ → Membership.mem (γ := Finset ι) ∅ i) ∧ norm.{u_1} (E := M) (∏ j ∈ ∅, f j) ≤ ‖f i‖
Tactic: rcases t.eq_empty_or_nonempty with rfl | ht
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (t.Nonempty → i ∈ t) ∧ norm.{u_1} (E := M) (∏ j ∈ t, f j) ≤ ‖f i‖
have inr : ∀ (ht : t.Nonempty), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Multiset ι
inst_2 : Nonempty ι
f : ι → M
⊢ ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
have inhabit : ∀ (inhabited_h : Inhabited ι), ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have 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‖
Tactic: obtain ⟨M, hMs, hM⟩ := hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have pos : ∀ (hMa : ‖f M‖ ≤ ‖f a‖), ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
Tactic: by_cases! hMa : ‖f M‖ ≤ ‖f a‖
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have neg : ∀ (hMa : ‖f a‖ < ‖f M‖), ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
Tactic: by_cases! hMa : ‖f M‖ ≤ ‖f a‖
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have pos : ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖
Tactic: refine ⟨a, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f a‖
have pos : ‖f a * (Multiset.map f t).prod‖ ≤ ‖f a‖
Tactic: rw [Multiset.map_cons, Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have 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‖
Tactic: rcases eq_or_ne t 0 with rfl | ht
Cleared hypotheses: t, hMs, hM
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have neg₁ : ∀ (ht : t ≠ 0), ∃ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
have neg : a ::ₘ t ≠ 0 → M ∈ a ::ₘ t
Tactic: refine ⟨M, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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
⊢ ∃ (i : ι), (a ::ₘ t ≠ 0 → i ∈ a ::ₘ t) ∧ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f i‖
have neg₁ : ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f M‖
Tactic: refine ⟨M, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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
⊢ ‖(Multiset.map f (a ::ₘ t)).prod‖ ≤ ‖f M‖
have neg : ‖f a * (Multiset.map f t).prod‖ ≤ ‖f M‖
Tactic: rw [Multiset.map_cons, Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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 ι
⊢ ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
have empty : ∃ (i : ι),
  (Ne.{u_2 + 1} (α := Multiset ι) 0 0 → Membership.mem (γ := Multiset ι) 0 i) ∧ ‖(Multiset.map f 0).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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ ∃ (i : ι), (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖f i‖
have 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‖
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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have inl : ∀ (hι : IsEmpty ι), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have inr : ∀ (hι : Nonempty ι), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
Tactic: rcases isEmpty_or_nonempty ι with hι | hι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have pos : ∀ (h : Multipliable f), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
Tactic: by_cases h : Multipliable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have neg : ∀ (h : ¬Multipliable f), norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
Tactic: by_cases h : Multipliable f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have neg : LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
Tactic: rw [tprod_eq_one_of_not_multipliable h, norm_one']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : ¬Multipliable f
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
have pos : ∀ (h_bd : BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
Tactic: by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖)
⊢ LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
have neg : ∀ (h_bd : ¬BddAbove (α := ℝ) (Set.range fun (i : ι) ↦ ‖f i‖)), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
Tactic: by_cases h_bd : BddAbove (Set.range fun i ↦ ‖f i‖)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖)
have neg : LE.le (α := ℝ) 0 0
Tactic: rw [Real.iSup_of_not_bddAbove h_bd]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (hypothesis)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
f : ι → M
hι : Nonempty ι
h : Multipliable f
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have h_bd : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖
have pos : ∀ (s : Finset ι), LE.le (α := ℝ) 0 (⨆ (i : ι), ‖f i‖)
Tactic: refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖)
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ ⨆ (i : ι), ‖f i‖
have pos₁ : ∀ (s : Finset ι), ∀ i ∈ s, ‖f i‖ ≤ ⨆ (i : ι), ‖f i‖
Tactic: refine le_of_tendsto' h.hasProd.norm' (fun s ↦ norm_prod_le_of_forall_le_of_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
have inl : IsEmpty ι → norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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
⊢ norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
have inr : Nonempty ι → norm.{u_1} (E := M) (∏' (i : ι), f i) ≤ C
Tactic: rcases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
have 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‖₊
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs'
Cleared hypotheses: s, ha, IH, hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
have 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‖₊
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (hypothesis)
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 ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
have IH₁ : nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
Tactic: specialize IH (hs.mono (by simp))
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
have 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‖₊
Tactic: obtain ⟨j, hj, hj'⟩ : ∃ j ∈ s, ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊ := by
      simpa [IH] using s.exists_mem_eq_sup hs' _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ Finset.cons a s ha, f i) = (Finset.cons a s ha).sup fun (i : ι) ↦ ‖f i‖₊
have cons : ‖f a‖₊ ≠ nnnorm.{u_1} (E := M) (∏ x ∈ s, f x)
Tactic: suffices ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊ by simp [← IH, nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ ‖f a‖₊ ≠ nnnorm.{u_1} (E := M) (∏ x ∈ s, f x)
have cons : ‖f a‖₊ ≠ ‖f j‖₊
Tactic: rw [hj']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
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‖₊
⊢ ‖f a‖₊ ≠ ‖f j‖₊
have cons : a ∈ (↑(Finset.cons a s ha) : Set ι)
Tactic: apply hs