awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → PseudoMetricSpace (α i)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
inst_3 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : PiLp ∞ α
h : 1 ≤ ENNReal.toReal ∞
⊢ False

Tactic:
norm_num at h
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
inr :
  HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal))
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
simp only [edist_eq_sum, edist_dist, dist_eq_sum, this]

Premises used: PiLp.edist_eq_sum, edist_dist, PiLp.dist_eq_sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ LE.le (α := ℝ) 0 (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal)

Tactic:
simp [Finset.sum_nonneg, Real.rpow_nonneg]

Premises used: Finset.sum_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
inr :
  HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
    ENNReal.ofReal (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) (1 / p.toReal))

Tactic:
rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]

Premises used: ENNReal.ofReal_rpow_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
inst_3 : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
this : 0 < p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (∑ x : ι, ENNReal.ofReal (dist (f.ofLp x) (g.ofLp x)) ^ p.toReal) (1 / p.toReal) =
    ENNReal.ofReal (∑ i : ι, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp [Real.rpow_nonneg, ENNReal.ofReal_sum_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg]

Premises used: ENNReal.ofReal_sum_of_nonneg, ENNReal.ofReal_rpow_of_nonneg, Real.rpow_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
inl : ∀ [Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : PiLp ∞ β), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
inr : ∀ (h : 1 ≤ p.toReal), edist (x.ofLp i) (y.ofLp i) ≤ edist x y
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
rcases p.dichotomy with (rfl | h)

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → PseudoEMetricSpace (β i)
inst_1 : Fintype ι
i : ι
inst_2 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : PiLp ∞ β
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
simpa only [edist_eq_iSup] using le_iSup (fun i => edist (x i) (y i)) i

Premises used: le_iSup, PiLp.edist_eq_iSup, EDist.edist, WithLp.ofLp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
⊢ p.toReal * (1 / p.toReal) = 1

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (zero_lt_one.trans_le h).ne'
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
inr :
  edist (x.ofLp i) (y.ofLp i) ≤ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x y

Tactic:
rw [edist_eq_sum (zero_lt_one.trans_le h)]

Premises used: PiLp.edist_eq_sum, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist (x.ofLp i) (y.ofLp i) = (edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
simp [← ENNReal.rpow_mul, cancel, -one_div]

Premises used: ENNReal.rpow_mul, one_div
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
h₁ : edist (x.ofLp i) (y.ofLp i) ^ p.toReal ≤ ∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal
⊢ (edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist (x.ofLp i) (y.ofLp i) ^ p.toReal ≤ ∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal

Tactic:
Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum, bot_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist (x.ofLp i) (y.ofLp i) ^ p.toReal ≤ ∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal

Tactic:
exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.single_le_sum, bot_le
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : PiLp p β
i : ι
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist : EDist.edist (x.ofLp i) (y.ofLp i) = (EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
edist₁ :
  (EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)
⊢ EDist.edist (x.ofLp i) (y.ofLp i) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal)

Tactic:
calc
      edist (x i) (y i) = (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
        simp [← ENNReal.rpow_mul, cancel, -one_div]
      _ ≤ (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by
        gcongr
        exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)

Premises used: Finset.univ, HDiv.hDiv, ENNReal.toReal, HPow.hPow, EDist.edist, OfNat.ofNat, WithLp.ofLp, Finset.sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
simp_rw : ∀ (b : ι), edist (x.ofLp b) (y.ofLp b) ≤ edist x y
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
simp_rw [edist_pi_def, Finset.sup_le_iff, Finset.mem_univ, forall_true_left]

Premises used: Finset.mem_univ, forall_true_left, edist_pi_def, Finset.sup_le_iff
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x.ofLp b) (y.ofLp b) ≤ edist x y

Tactic:
edist_apply_le_edist_aux _ _

Premises used: _private.0.PiLp.edist_apply_le_edist_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
⊢ ∀ (b : ι), edist (x.ofLp b) (y.ofLp b) ≤ edist x y

Tactic:
exact edist_apply_le_edist_aux _ _

Premises used: _private.0.PiLp.edist_apply_le_edist_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
inl :
  ∀ [inst : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ ((i : ι) → β i)),
    edist x y ≤
      (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) *
        edist x.ofLp y.ofLp
inr :
  ∀ (h : 1 ≤ p.toReal),
    edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
rcases p.dichotomy with (rfl | h)

Premises used: ENNReal.dichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → PseudoEMetricSpace (β i)
inst_1 : Fintype ι
inst_2 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ ((i : ι) → β i)
inl : ∀ (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp
⊢ edist x y ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
simp only [edist_eq_iSup, ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero,
      ENNReal.coe_one, one_mul, iSup_le_iff]

Premises used: ENNReal.div_top, ENNReal.coe_one, PiLp.edist_eq_iSup, ENNReal.toReal_zero, NNReal.rpow_zero, iSup_le_iff, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → PseudoEMetricSpace (β i)
inst_1 : Fintype ι
inst_2 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ ((i : ι) → β i)
⊢ ∀ (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp

Tactic:
fun i => Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → PseudoEMetricSpace (β i)
inst_1 : Fintype ι
inst_2 : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x y : WithLp ∞ ((i : ι) → β i)
⊢ ∀ (i : ι), edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp

Tactic:
exact fun i => Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
⊢ 0 < p.toReal

Tactic:
have pos : 0 < p.toReal := zero_lt_one.trans_le h
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
have nonneg : 0 ≤ 1 / p.toReal := one_div_nonneg.2 (le_of_lt pos)
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
⊢ p.toReal * (1 / p.toReal) = 1

Tactic:
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel₀ 1 (ne_of_gt pos)
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
inr :
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (ENNReal.toReal 1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ edist x y ≤ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
rw [edist_eq_sum pos, ENNReal.toReal_div 1 p]

Premises used: PiLp.edist_eq_sum, OfNat.ofNat, ENNReal.toReal_div
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal)

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp

Tactic:
Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
⊢ edist (x.ofLp i) (y.ofLp i) ≤ edist x.ofLp y.ofLp

Tactic:
exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.le_sup
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
simp :
  HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
⊢ HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal) =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
          ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]

Premises used: Finset.card_univ, ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_one, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (↑(Fintype.card ι) : ℝ≥0∞) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)

Tactic:
have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
          (ENNReal.coe_natCast (Fintype.card ι)).symm
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
this : (↑(Fintype.card ι) : ℝ≥0∞) = (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞)
rw :
  (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp
rw₁ rw₂ :
  (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ≥0∞) ^ (1 / p.toReal) * edist x.ofLp y.ofLp
⊢ HPow.hPow (α := ℝ≥0∞) (↑(Fintype.card ι) : ℝ≥0∞) (1 / p.toReal) * edist x.ofLp y.ofLp =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * edist x.ofLp y.ofLp

Tactic:
rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]

Premises used: ENNReal.coe_rpow_of_nonneg
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
x y : WithLp p ((i : ι) → β i)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
edist :
  HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, EDist.edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal)
edist₁ :
  HPow.hPow (α := ℝ≥0∞) (∑ _i : ι, EDist.edist x.ofLp y.ofLp ^ p.toReal) (1 / p.toReal) =
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) * EDist.edist x.ofLp y.ofLp
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i : ι, EDist.edist (x.ofLp i) (y.ofLp i) ^ p.toReal) (1 / p.toReal) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal)) : ℝ≥0∞) *
      Finset.sup Finset.univ fun (b : ι) ↦ EDist.edist (x.ofLp b) (y.ofLp b)

Tactic:
calc
      (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
          (∑ _i, edist (ofLp x) (ofLp y) ^ p.toReal) ^ (1 / p.toReal) := by
        gcongr with i
        exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)
      _ =
          ((Fintype.card ι : ℝ≥0) ^ (1 / p.toReal) : ℝ≥0) *
            edist (ofLp x) (ofLp y) := by
        simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
          ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]
        have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) :=
          (ENNReal.coe_natCast (Fintype.card ι)).symm
        rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]

Premises used: Finset.univ, Fintype.card, HDiv.hDiv, Nat.cast, ENNReal.toReal, HPow.hPow, EDist.edist, OfNat.ofNat, WithLp.ofLp, Finset.sum
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
⊢ IsUniformInducing (α := WithLp p ((i : ι) → β i)) ofLp

Tactic:
(antilipschitzWith_ofLp_aux p β).isUniformInducing
      (lipschitzWith_ofLp_aux p β).uniformContinuous

Premises used: AntilipschitzWith.isUniformInducing, LipschitzWith.uniformContinuous, _private.0.PiLp.lipschitzWith_ofLp_aux, _private.0.PiLp.antilipschitzWith_ofLp_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
rw :
  Eq (α := Filter (PiLp p β × PiLp p β))
    (comap (β := ((i : ι) → β i) × ((i : ι) → β i))
      (fun (x : WithLp p ((i : ι) → β i) × WithLp p ((i : ι) → β i)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)))
    (𝓤 (WithLp p ((i : ι) → β i)))
⊢ Eq (α := Filter (PiLp p β × PiLp p β)) (𝓤 (PiLp p β)) (𝓤 (WithLp p ((i : ι) → β i)))

Tactic:
rw [← (isUniformInducing_ofLp_aux p β).comap_uniformity]

Premises used: IsUniformInducing.comap_uniformity, _private.0.PiLp.isUniformInducing_ofLp_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoEMetricSpace (β i)
inst_2 : Fintype ι
⊢ Eq (α := Filter (PiLp p β × PiLp p β))
    (comap (β := ((i : ι) → β i) × ((i : ι) → β i))
      (fun (x : WithLp p ((i : ι) → β i) × WithLp p ((i : ι) → β i)) ↦ (x.1.ofLp, x.2.ofLp)) (𝓤 ((i : ι) → β i)))
    (𝓤 (WithLp p ((i : ι) → β i)))

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : (i : ι) → PseudoMetricSpace (α i)
inst_2 : Fintype ι
⊢ Eq (α := Filter (PiLp p α)) (cobounded (PiLp p α)) (cobounded (PiLp p α))

Tactic:
le_antisymm (antilipschitzWith_ofLp_aux p α).tendsto_cobounded.le_comap
    (lipschitzWith_ofLp_aux p α).comap_cobounded_le

Premises used: Filter.Tendsto.le_comap, AntilipschitzWith.tendsto_cobounded, LipschitzWith.comap_cobounded_le, le_antisymm, _private.0.PiLp.lipschitzWith_ofLp_aux, _private.0.PiLp.antilipschitzWith_ofLp_aux
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
⊢ Continuous[topologicalSpace p β, Pi.topologicalSpace] ofLp

Tactic:
continuous_induced_dom

Premises used: continuous_induced_dom
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
i : ι
⊢ Continuous[topologicalSpace p β, inst i] fun (f : PiLp p β) ↦ f.ofLp i

Tactic:
(continuous_apply i).comp (continuous_ofLp p β)

Premises used: Continuous.comp, PiLp.continuous_ofLp, continuous_apply
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
⊢ Continuous[Pi.topologicalSpace, topologicalSpace p β] (toLp p)

Tactic:
continuous_induced_rng.2 continuous_id

Premises used: Iff.mpr, continuous_id, continuous_induced_rng
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
⊢ Homeomorph.toEquiv (homeomorph p β) = WithLp.equiv p ((i : ι) → β i)

Tactic:
rfl

Premises used: WithLp.equiv, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
i : ι
⊢ IsOpenMap (Y := β i) fun (f : PiLp p β) ↦ f.ofLp i

Tactic:
(isOpenMap_eval i).comp (homeomorph p β).isOpenMap

Premises used: isOpenMap_eval, IsOpenMap.comp, PiLp.homeomorph, Homeomorph.isOpenMap
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : (i : ι) → TopologicalSpace (β i)
inst_1 : ∀ (i : ι), T0Space.{u_4} (β i)
⊢ T0Space (PiLp p β)

Tactic:
(homeomorph p β).symm.t0Space

Premises used: PiLp.homeomorph, Homeomorph.t0Space, Homeomorph.symm
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Countable ι
inst_1 : (i : ι) → TopologicalSpace (β i)
inst_2 : ∀ (i : ι), SecondCountableTopology.{u_4} (β i)
⊢ SecondCountableTopology (PiLp p β)

Tactic:
(homeomorph p β).secondCountableTopology

Premises used: PiLp.homeomorph, Homeomorph.secondCountableTopology
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst : (i : ι) → UniformSpace (β i)
⊢ UniformContinuous (α := WithLp p ((i : ι) → β i)) ofLp

Tactic:
uniformContinuous_comap

Premises used: uniformContinuous_comap