awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (d * fun (n : ℕ) ↦ ∏ k ∈ range (n + 1), v k)
have suffices : ∀ n ≥ N, d n = d N
Tactic: suffices ∀ n ≥ N, d n = d N from (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
-- 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
n : ℕ
hn : n ≥ N
⊢ Eq.{u_2 + 1} (α := E) (∏ k ∈ range (n + 1), u k / v k) (∏ k ∈ range (N + 1), u k / v k)
have rw : ∀ n ≥ N + 1, u n / v n = 1
Tactic: rw [eventually_constant_prod (N := N + 1) _ (by gcongr)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)
have obtain : ∀ (C : ℝ) (hC : ∀ (m n : ℕ), dist (u m) (u n) < C), BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)
Tactic: obtain ⟨C, -, hC⟩ := cauchySeq_bdd hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (hypothesis)
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), dist (u m) (u n) < C
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)
have hC₁ : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
Tactic: simp_rw [SeminormedGroup.dist_eq] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ C + ‖u 0‖
have rw : ‖u n‖ ≤ ‖u 0‖ + C
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
n : ℕ
⊢ ‖u n‖ ≤ ‖u 0‖ + C
have refine : ‖u 0‖ + ‖(u n)⁻¹ * u 0‖ ≤ ‖u 0‖ + C
Tactic: refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (hypothesis)
Goal:
G : Type u_4
inst : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
⊢ BddAbove (α := ℝ) (Set.range fun (n : ℕ) ↦ ‖u n‖)
have this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
Tactic: have : ∀ n, ‖u n‖ ≤ C + ‖u 0‖ := by
    intro n
    rw [add_comm]
    refine (norm_le_norm_add_norm_inv_mul (u n) (u 0)).trans ?_
    simp [(hC _ _).le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Uniform (goal)
Goal:
E : Type u_2
F : Type u_3
inst : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
a b : E
r : ℝ
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 : SeminormedCommGroup E
inst_1 : SeminormedCommGroup F
f : E → F
C : ℝ≥0
a b : E
r : ℝ
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.ZeroAtInfty (hypothesis)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have h : Tendsto.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)
Tactic: have h := zero_at_infty f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (hypothesis)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Tendsto.{u_1, u_2} (β := F) (⇑f : (a : E) → F) (cocompact E) (𝓝 0)
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have h₁ : ∀ (s : Set ℝ),
  Membership.mem (γ := Filter ℝ) (𝓝 0) s →
    (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) ⁻¹' s ∈ cocompact E
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (hypothesis)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h :
  ∀ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝 0) s →
      (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) ⁻¹' s ∈ cocompact E
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have h₁ : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
Tactic: specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have rcases : ∀ (r : ℝ)
  (hr :
    Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
      (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))),
  ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
Tactic: rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
⊢ ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have h₁ : ∀ (x : E) (_hx : r < ‖x‖), norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
⊢ norm.{u_2} (E := F) ((f : (a : E) → F) x : F) < ε
have h₁ : Membership.mem (γ := Set E)
  (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε)) x
Tactic: suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : FunLike 𝓕 E F
inst_3 : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε) ∈ cocompact E
r : ℝ
hr :
  Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε))
x : E
hr' : r < ‖x‖
⊢ Membership.mem (γ := Set E)
    (Set.preimage (β := ℝ) (fun (x : E) ↦ norm.{u_2} (E := F) ((f : (a : E) → F) x : F)) (Metric.ball 0 ε)) x
have h₁ : Membership.mem (γ := Set E) (Metric.closedBall 0 r)ᶜ x
Tactic: apply hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
⊢ Tendsto f (cocompact E) (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : E) ↦ ‖f x‖) (cocompact E) (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) (𝓝 0) s
⊢ Membership.mem (γ := Filter ℝ) (map (fun (x : E) ↦ ‖f x‖) (cocompact E)) s
have rw : ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
Tactic: rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) (𝓝 0) s
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
have hs₁ : ∃ ε > 0, Metric.ball 0 ε ⊆ s
Tactic: rw [Metric.mem_nhds_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
have rcases : ∀ (ε : ℝ) (hε : ε > 0) (hs : Metric.ball 0 ε ⊆ s),
  ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
Tactic: rcases hs with ⟨ε, hε, hs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
have rcases : ∀ (r : ℝ) (hr : ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε),
  ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
Tactic: rcases h ε hε with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.ZeroAtInfty (goal)
Goal:
E : Type u_1
F : Type u_2
inst : SeminormedAddGroup E
inst_1 : SeminormedAddCommGroup F
inst_2 : ProperSpace E
f : E → F
h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε
⊢ ∃ (r : ℝ), Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
have h₁ : Subset.{u_1} (α := Set E) (Metric.closedBall 0 r)ᶜ ((fun (x : E) ↦ ‖f x‖) ⁻¹' s)
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : (i : α) → E i
⊢ Memℓp (E := E) f p
have inl : Memℓp (E := E) f 0
Tactic: rcases p.trichotomy with (rfl | rfl | _h)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : (i : α) → E i
inl : Memℓp (E := E) f 0
⊢ Memℓp (E := E) f p
have inr : Memℓp (E := E) f ∞
Tactic: rcases p.trichotomy with (rfl | rfl | _h)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : (i : α) → E i
inl : Memℓp (E := E) f 0
inr : Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₁ : ∀ (_h : 0 < p.toReal), Memℓp (E := E) f p
Tactic: rcases p.trichotomy with (rfl | rfl | _h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : (i : α) → E i
_h : 0 < p.toReal
⊢ Memℓp (E := E) f p
have inr : ∀ (val : Fintype α), Memℓp (E := E) f p
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
f : ↥(lp E p)
⊢ norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖
have inl : ∀ (f : ↥(lp E 0)), norm (E := PiLp 0 E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E 0)) → PiLp 0 E) f : PiLp 0 E) = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
f : ↥(lp E p)
inl : ∀ (f : ↥(lp E 0)), norm (E := PiLp 0 E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E 0)) → PiLp 0 E) f : PiLp 0 E) = ‖f‖
⊢ norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖
have inr : ∀ (f : ↥(lp E ∞)), norm (E := PiLp ∞ E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E ∞)) → PiLp ∞ E) f : PiLp ∞ E) = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
f : ↥(lp E p)
inl : ∀ (f : ↥(lp E 0)), norm (E := PiLp 0 E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E 0)) → PiLp 0 E) f : PiLp 0 E) = ‖f‖
inr : ∀ (f : ↥(lp E ∞)), norm (E := PiLp ∞ E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E ∞)) → PiLp ∞ E) f : PiLp ∞ E) = ‖f‖
⊢ norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖
have inr₁ : ∀ (h : 0 < p.toReal), norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Fintype α
f : ↥(lp E ∞)
⊢ norm (E := PiLp ∞ E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E ∞)) → PiLp ∞ E) f : PiLp ∞ E) = ‖f‖
have inr : Eq (α := ℝ)
  (⨆ (i : α), norm.{u_2} (E := E i) (ofLp (p := ∞) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E ∞)) → PiLp ∞ E) f) i))
  (⨆ (i : α), ‖(↑f : (i : α) → E i) i‖)
Tactic: rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
f : ↥(lp E p)
h : 0 < p.toReal
⊢ norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖
have inr : HPow.hPow (α := ℝ)
    (∑ i : α,
      norm.{u_2} (E := E i) (ofLp (p := p) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f) i) ^ p.toReal)
    (1 / p.toReal) =
  HPow.hPow (α := ℝ) (∑ b : α, ‖(↑f : (i : α) → E i) b‖ ^ p.toReal) (1 / p.toReal)
Tactic: rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.LpEquiv (goal)
Goal:
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NormedRing A
inst_3 : NormOneClass A
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace 𝕜 E
inst_8 : NonUnitalNormedRing R
f : ↥(lp (fun (x : α) ↦ E) ∞)
⊢ norm (E := α →ᵇ E)
      (({ toFun := Equiv.toFun (AddEquiv.toEquiv AddEquiv.lpBCF), map_add' := ⋯, map_smul' := ⋯,
              invFun := Equiv.invFun (AddEquiv.toEquiv AddEquiv.lpBCF), left_inv := ⋯, right_inv := ⋯ :
              ↥(lp (fun (x : α) ↦ E) ∞) ≃ₗ[𝕜] α →ᵇ E } :
            (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E)
          f :
        α →ᵇ E) =
    ‖f‖
have simp : Eq (α := ℝ)
  (⨆ (x : α),
    norm.{u_2} (E := E)
      (((({ toFun := Equiv.toFun (AddEquiv.toEquiv AddEquiv.lpBCF), map_add' := sorry, map_smul' := sorry,
                    invFun := Equiv.invFun (AddEquiv.toEquiv AddEquiv.lpBCF), left_inv := sorry, right_inv := sorry } :
                  (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E)
                f :
              α →ᵇ E) :
            (a : α) → E)
          x :
        E))
  (⨆ (i : α), ‖(↑f : (i : α) → E) i‖)
Tactic: simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.Matrix (goal)
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p : ℝ≥0∞
⊢ Eq (α := WithLp p (n → R) →ₗ[R] WithLp p (n → R))
    ((toLpLin p p : (a : Matrix n n R) → WithLp p (n → R) →ₗ[R] WithLp p (n → R)) 1) LinearMap.id
have h : ∀ (x : WithLp p (n → R)) (i : n),
  Eq.{u_4 + 1} (α := R)
    (ofLp (p := p)
      (((toLpLin p p : (a : Matrix n n R) → WithLp p (n → R) →ₗ[R] WithLp p (n → R)) 1 :
          (a : WithLp p (n → R)) → WithLp p (n → R))
        x)
      i)
    (ofLp (p := p) ((LinearMap.id : (a : WithLp p (n → R)) → WithLp p (n → R)) x) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.Matrix (goal)
Goal:
m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p q r : ℝ≥0∞
inst_3 : Fintype o
inst_4 : DecidableEq o
A : Matrix m n R
B : Matrix n o R
⊢ Eq (α := WithLp p (o → R) →ₗ[R] WithLp r (m → R))
    ((toLpLin p r : (a : Matrix m o R) → WithLp p (o → R) →ₗ[R] WithLp r (m → R)) (A * B) :
      WithLp p (o → R) →ₗ[R] WithLp r (m → R))
    ((toLpLin q r : (a : Matrix m n R) → WithLp q (n → R) →ₗ[R] WithLp r (m → R)) A ∘ₗ
        (toLpLin p q : (a : Matrix n o R) → WithLp p (o → R) →ₗ[R] WithLp q (n → R)) B :
      WithLp p (o → R) →ₗ[R] WithLp r (m → R))
have h : ∀ (x : WithLp p (o → R)) (i : m),
  Eq.{u_4 + 1} (α := R)
    (ofLp (p := r)
      ((((toLpLin p r : (a : Matrix m o R) → WithLp p (o → R) →ₗ[R] WithLp r (m → R)) (A * B) :
            WithLp p (o → R) →ₗ[R] WithLp r (m → R)) :
          (a : WithLp p (o → R)) → WithLp r (m → R))
        x)
      i)
    (ofLp (p := r)
      (((toLpLin q r : (a : Matrix m n R) → WithLp q (n → R) →ₗ[R] WithLp r (m → R)) A ∘ₗ
            (toLpLin p q : (a : Matrix n o R) → WithLp p (o → R) →ₗ[R] WithLp q (n → R)) B :
          (a : WithLp p (o → R)) → WithLp r (m → R))
        x)
      i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
s : Set (WithLp p X)
hs : MeasurableSet s
⊢ MeasurableSet (toLp p ⁻¹' s)
have obtain : ∀ (t : Set X) (ht : MeasurableSet t), MeasurableSet (toLp p ⁻¹' ofLp ⁻¹' t)
Tactic: obtain ⟨t, ht, rfl⟩ := hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
Y : Type u_2
inst_1 : MeasurableSpace Y
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : BorelSpace X
inst_5 : BorelSpace Y
inst_6 : SecondCountableTopologyEither X Y
rw : Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
⊢ Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
have rw₁ : Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (MeasurableSpace.comap ofLp (borel (X × Y)))
Tactic: rw [instProdTopologicalSpace, borel_comap, measurableSpace,
      BorelSpace.measurable_eq (α := X × Y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
Y : Type u_2
inst_1 : MeasurableSpace Y
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : BorelSpace X
inst_5 : BorelSpace Y
inst_6 : SecondCountableTopologyEither X Y
rw : Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
rw₁ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (MeasurableSpace.comap ofLp (borel (X × Y)))
⊢ Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
have rw₂ : Eq (α := MeasurableSpace (WithLp p (X × Y))) (MeasurableSpace.comap ofLp inferInstance)
  (MeasurableSpace.comap ofLp (borel (X × Y)))
Tactic: rw [instProdTopologicalSpace, borel_comap, measurableSpace,
      BorelSpace.measurable_eq (α := X × Y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
Y : Type u_2
inst_1 : MeasurableSpace Y
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : BorelSpace X
inst_5 : BorelSpace Y
inst_6 : SecondCountableTopologyEither X Y
rw : Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
rw₁ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (MeasurableSpace.comap ofLp (borel (X × Y)))
rw₂ :
  Eq (α := MeasurableSpace (WithLp p (X × Y))) (MeasurableSpace.comap ofLp inferInstance)
    (MeasurableSpace.comap ofLp (borel (X × Y)))
⊢ Eq (α := MeasurableSpace (WithLp p (X × Y))) (measurableSpace p (X × Y)) (borel (WithLp p (X × Y)))
have rw₃ : Eq (α := MeasurableSpace (WithLp p (X × Y))) (MeasurableSpace.comap ofLp inferInstance)
  (MeasurableSpace.comap ofLp (borel (X × Y)))
Tactic: rw [instProdTopologicalSpace, borel_comap, measurableSpace,
      BorelSpace.measurable_eq (α := X × Y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X_1 : Type u_1
inst : MeasurableSpace X_1
ι : Type u_2
X : ι → Type u_3
inst_1 : Countable ι
inst_2 : (i : ι) → MeasurableSpace (X i)
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (X i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (X i)
rw : Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
⊢ Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
have rw₁ : Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i))
  (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
Tactic: rw [topologicalSpace, borel_comap, WithLp.measurableSpace,
      BorelSpace.measurable_eq (α := Π i, X i)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.MeasurableSpace (goal)
Goal:
p : ℝ≥0∞
X_1 : Type u_1
inst : MeasurableSpace X_1
ι : Type u_2
X : ι → Type u_3
inst_1 : Countable ι
inst_2 : (i : ι) → MeasurableSpace (X i)
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), BorelSpace.{u_3} (X i)
inst_5 : ∀ (i : ι), SecondCountableTopology.{u_3} (X i)
rw : Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
rw₁ :
  Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i))
    (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
⊢ Eq (α := MeasurableSpace (PiLp p X)) (WithLp.measurableSpace p ((i : ι) → X i)) (borel (PiLp p X))
have rw₂ : Eq (α := MeasurableSpace (PiLp p X)) (MeasurableSpace.comap WithLp.ofLp inferInstance)
  (MeasurableSpace.comap WithLp.ofLp (borel ((i : ι) → X i)))
Tactic: rw [topologicalSpace, borel_comap, WithLp.measurableSpace,
      BorelSpace.measurable_eq (α := Π i, X i)]