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
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 ι)
⊢ ‖f a‖₊ ≠ ‖f j‖₊
have cons₁ : j ∈ (↑(Finset.cons a s ha) : Set ι)
Tactic: apply 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‖₊
cons : a ∈ (↑(Finset.cons a s ha) : Set ι)
cons₁ : j ∈ (↑(Finset.cons a s ha) : Set ι)
⊢ ‖f a‖₊ ≠ ‖f j‖₊
have cons₂ : a ≠ j
Tactic: apply 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
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‖₊
have 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‖₊
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
Cleared hypotheses: s, 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
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‖₊
⊢ nnnorm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup fun (i : ι) ↦ ‖f i‖₊
have 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‖₊
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
Cleared hypotheses: s, 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
hs' : s.Nonempty
hs : (↑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‖
have rw : (↑(s.sup' hs' fun (i : ι) ↦ ‖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']
-- 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
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‖
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) = s.sup' hs' fun (i : ι) ↦ ‖f i‖
have rw₁ : (↑s : Set ι).Pairwise fun (i j : ι) ↦ ‖f i‖₊ ≠ ‖f j‖₊
Tactic: rw [← coe_nnnorm', nnnorm_prod_eq_sup_of_pairwise_ne, ← Finset.sup'_eq_sup hs']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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
⊢ ‖f x‖ = ‖x‖
have rw : dist (f x) 1 = ‖x‖
Tactic: rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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‖
⊢ ‖f x‖ = ‖x‖
have rw₁ : dist (f x) (f 1) = ‖x‖
Tactic: rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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‖
⊢ ‖f x‖ = ‖x‖
have rw₂ : dist x 1 = ‖x‖
Tactic: rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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‖
⊢ ‖f x‖ = ‖x‖
have rw₃ : ‖x‖ = ‖x‖
Tactic: rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
⊢ dist b (b * a) = ‖a‖
have rw : dist b (b * a) = dist 1 a
Tactic: rw [← dist_one_left, ← dist_mul_left b 1 a, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
rw : dist b (b * a) = dist 1 a
⊢ dist b (b * a) = ‖a‖
have rw₁ : dist b (b * a) = dist (b * 1) (b * a)
Tactic: rw [← dist_one_left, ← dist_mul_left b 1 a, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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)
⊢ dist b (b * a) = ‖a‖
have rw₂ : dist b (b * a) = dist b (b * a)
Tactic: rw [← dist_one_left, ← dist_mul_left b 1 a, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
⊢ dist (b * a) b = ‖a‖
have rw : dist b (b * a) = ‖a‖
Tactic: rw [dist_comm, dist_self_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedGroup E
a b : E
rw : dist b (b * a) = ‖a‖
⊢ dist (b * a) b = ‖a‖
have rw₁ : ‖a‖ = ‖a‖
Tactic: rw [dist_comm, dist_self_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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
⊢ (↑C : ℝ) * ‖a⁻¹ * b‖ ≤ (↑C : ℝ) * r
have ha₁ : 0 ≤ (↑C : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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
⊢ (↑C : ℝ) * ‖a⁻¹ * b‖ ≤ (↑C : ℝ) * r
have ha : 0 ≤ (↑C : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
⊢ 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‖
have 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‖
Tactic: simp only [isometry_iff_dist_eq, dist_eq_norm_inv_mul, ← map_inv, ← map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
⊢ (∀ (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‖
have refine : ∀ (h : ∀ (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‖
Tactic: refine ⟨fun h x => ?_, fun h x y => h _⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
⊢ (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) ↔
    ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_1 : (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) →
  ∀ (K : ℝ≥0) (hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) (x : E),
    ((↑K : ℝ) + 1)⁻¹ * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
Tactic: refine ⟨fun ⟨K, hK⟩ ↦ ⟨(K + 1)⁻¹, by positivity, fun x ↦ ?_⟩, fun ⟨c, hc0, hc⟩ ↦
    ⟨.mk c⁻¹ (by positivity), MonoidHomClass.antilipschitz_of_bound f fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
refine_1 :
  (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) →
    ∀ (K : ℝ≥0) (hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) (x : E),
      ((↑K : ℝ) + 1)⁻¹ * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
⊢ (∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)) ↔
    ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_2 : (∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)) →
  ∀ (c : ℝ) (hc0 : c > 0) (hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)) (x : E),
    ‖x‖ ≤ (↑(NNReal.mk c⁻¹ sorry) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
Tactic: refine ⟨fun ⟨K, hK⟩ ↦ ⟨(K + 1)⁻¹, by positivity, fun x ↦ ?_⟩, fun ⟨c, hc0, hc⟩ ↦
    ⟨.mk c⁻¹ (by positivity), MonoidHomClass.antilipschitz_of_bound f fun x ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
h : ∃ (K : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
K : ℝ≥0
hK : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) K (⇑f : (a : E) → F)
x : E
⊢ ((↑K : ℝ) + 1)⁻¹ * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_1 : ((↑K : ℝ) + 1)⁻¹ * (↑K : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F) ≤
  norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
Tactic: grw [hK.le_mul_norm' (map_one f), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x : E
⊢ ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have h₂ : 0 ≤ (↑(NNReal.mk c⁻¹ sorry) : ℝ)
Tactic: grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x : E
h₂ : 0 ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ)
⊢ ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_2 : ‖x‖ ≤ (↑(NNReal.mk c⁻¹ sorry) : ℝ) * (c * ‖x‖)
Tactic: grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x : E
h₂ : 0 ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ)
refine_2 : ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * (c * ‖x‖)
⊢ ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_2₁ : ‖x‖ ≤ c⁻¹ * (c * ‖x‖)
Tactic: grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
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 : 𝓕
h : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
x : E
h₂ : 0 ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ)
refine_2 : ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * (c * ‖x‖)
refine_2₁ : ‖x‖ ≤ c⁻¹ * (c * ‖x‖)
⊢ ‖x‖ ≤ (↑(NNReal.mk c⁻¹ ⋯) : ℝ) * norm.{u_3} (E := F) ((f : (a : E) → F) x : F)
have refine_2₂ : ‖x‖ ≤ ‖x‖
Tactic: grw [← hc, NNReal.coe_mk, inv_mul_cancel_left₀ hc0.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = ‖b‖
have rw : dist a (b * a) = dist 1 b
Tactic: rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = dist 1 b
⊢ dist a (b * a) = ‖b‖
have rw₁ : dist a (b * a) = dist (a * 1) (a * b)
Tactic: rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = dist 1 b
rw₁ : dist a (b * a) = dist (a * 1) (a * b)
⊢ dist a (b * a) = ‖b‖
have rw₂ : dist a (b * a) = dist a (a * b)
Tactic: rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = dist 1 b
rw₁ : dist a (b * a) = dist (a * 1) (a * b)
rw₂ : dist a (b * a) = dist a (a * b)
⊢ dist a (b * a) = ‖b‖
have rw₃ : dist a (a * b) = dist a (a * b)
Tactic: rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
⊢ dist (b * a) a = ‖b‖
have rw : dist a (b * a) = ‖b‖
Tactic: rw [dist_comm, dist_mul_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (b * a) = ‖b‖
⊢ dist (b * a) a = ‖b‖
have rw₁ : ‖b‖ = ‖b‖
Tactic: rw [dist_comm, dist_mul_self_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
⊢ dist a (a / b) = ‖b‖
have rw : dist a (a * b⁻¹) = ‖b‖
Tactic: rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (a * b⁻¹) = ‖b‖
⊢ dist a (a / b) = ‖b‖
have rw₁ : ‖b⁻¹‖ = ‖b‖
Tactic: rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (a * b⁻¹) = ‖b‖
rw₁ : ‖b⁻¹‖ = ‖b‖
⊢ dist a (a / b) = ‖b‖
have rw₂ : ‖b‖ = ‖b‖
Tactic: rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
⊢ dist (a / b) a = ‖b‖
have rw : dist a (a / b) = ‖b‖
Tactic: rw [dist_comm, dist_self_div_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b : E
rw : dist a (a / b) = ‖b‖
⊢ dist (a / b) a = ‖b‖
have rw₁ : ‖b‖ = ‖b‖
Tactic: rw [dist_comm, dist_self_div_right]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
⊢ dist (a / b) c = dist a (c * b)
have rw : dist (a / b * b) (c * b) = dist a (c * b)
Tactic: rw [← dist_mul_right _ _ b, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
rw : dist (a / b * b) (c * b) = dist a (c * b)
⊢ dist (a / b) c = dist a (c * b)
have rw₁ : dist a (c * b) = dist a (c * b)
Tactic: rw [← dist_mul_right _ _ b, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
⊢ dist a (b / c) = dist (a * c) b
have rw : dist (a * c) (b / c * c) = dist (a * c) b
Tactic: rw [← dist_mul_right _ _ c, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a b c : E
rw : dist (a * c) (b / c * c) = dist (a * c) b
⊢ dist a (b / c) = dist (a * c) b
have rw₁ : dist (a * c) b = dist (a * c) b
Tactic: rw [← dist_mul_right _ _ c, div_mul_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂
have simp : (↑(nndist (a₁ * a₂) (b₁ * b₂)) : ℝ≥0∞) ≤ (↑(nndist a₁ b₁) : ℝ≥0∞) + (↑(nndist a₂ b₂) : ℝ≥0∞)
Tactic: simp only [edist_nndist]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ (↑(nndist (a₁ * a₂) (b₁ * b₂)) : ℝ≥0∞) ≤ (↑(nndist a₁ b₁) : ℝ≥0∞) + (↑(nndist a₂ b₂) : ℝ≥0∞)
have norm_cast : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
have obtain : ∀ (Kf : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝[s] x) (hKf : LipschitzOnWith Kf f t),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
Tactic: obtain ⟨Kf, t, ht, hKf⟩ := hf hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
have obtain : ∀ (Kg : ℝ≥0) (u : Set α) (hu : u ∈ 𝓝[s] x) (hKg : LipschitzOnWith Kg g u),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] x, LipschitzOnWith.{u_4, u_5} (β := E) K (fun (x : α) ↦ f x * g x) t
Tactic: obtain ⟨Kg, u, hu, hKg⟩ := hg hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
⊢ AntilipschitzWith.{u_4, u_5} (β := E) (Kf⁻¹ - Kg)⁻¹ fun (x : α) ↦ f x * g x
have refine : ∀ (x y : α), dist x y ≤ (↑(Kf⁻¹ - Kg)⁻¹ : ℝ) * dist (f x * g x) (f y * g y)
Tactic: refine AntilipschitzWith.of_le_mul_dist fun x y => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist x y ≤ (↑(Kf⁻¹ - Kg)⁻¹ : ℝ) * dist (f x * g x) (f y * g y)
have rw : dist x y ≤ dist (f x * g x) (f y * g y) / (↑(Kf⁻¹ - Kg) : ℝ)
Tactic: rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist x y ≤ dist (f x * g x) (f y * g y) / (↑(Kf⁻¹ - Kg) : ℝ)
have rw : dist x y * (↑(Kf⁻¹ - Kg) : ℝ) ≤ dist (f x * g x) (f y * g y)
Tactic: rw [le_div_iff₀ (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
α : Type u_4
E : Type u_5
inst : SeminormedCommGroup E
inst_1 : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace ⋯
x y : α
⊢ dist x y * (↑(Kf⁻¹ - Kg) : ℝ) ≤ dist (f x * g x) (f y * g y)
have rw : (↑Kf⁻¹ : ℝ) * dist x y - (↑Kg : ℝ) * dist x y ≤ dist (f x * g x) (f y * g y)
Tactic: rw [mul_comm, NNReal.coe_sub hK.le, sub_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
p : E
⊢ Eq (α := SeparationQuotient E) (mk p) 1 ↔ ‖p‖ = 0
have rw : Eq (α := SeparationQuotient E) (mk p) 1 ↔ norm (E := SeparationQuotient E) (mk p) = 0
Tactic: rw [← norm_mk', norm_eq_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
p : E
rw : Eq (α := SeparationQuotient E) (mk p) 1 ↔ norm (E := SeparationQuotient E) (mk p) = 0
⊢ Eq (α := SeparationQuotient E) (mk p) 1 ↔ ‖p‖ = 0
have rw₁ : Eq (α := SeparationQuotient E) (mk p) 1 ↔ Eq (α := SeparationQuotient E) (mk p) 1
Tactic: rw [← norm_mk', norm_eq_zero']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ (fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k) = d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
have h : ∀ (n : ℕ), ∏ k ∈ range (n + 1), u k = HMul.hMul (β := (n : ℕ) → E) d (fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
inst : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ CauchySeq.{u_2, 0} (α := E) fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), u k
have rw : CauchySeq (d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k)
Tactic: rw [show (fun n => ∏ k ∈ range (n + 1), u k) = d * fun n => ∏ k ∈ range (n + 1), v k
      by ext n; simp [d]]