awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₄ : ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₅ : HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₅ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₆ : HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ ^ (p.toReal * (1 / p.toReal)) =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₅ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₆ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ ^ (p.toReal * (1 / p.toReal)) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₇ : HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * HPow.hPow (β := ℝ) ‖b‖₊ 1 =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₅ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₆ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ ^ (p.toReal * (1 / p.toReal)) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₇ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * HPow.hPow (β := ℝ) ‖b‖₊ 1 =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₈ : HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
h : 1 ≤ p.toReal
ne_zero : p.toReal ≠ 0
inr :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖Function.const ι b x‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₁ :
  HPow.hPow (α := ℝ≥0) (∑ x : ι, ‖b‖₊ ^ p.toReal) (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₂ :
  (Finset.card.{u_2} (α := ι) Finset.univ • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₃ :
  (Fintype.card ι • ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₄ :
  ((↑(Fintype.card ι) : ℝ≥0) * ‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₅ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * (‖b‖₊ ^ p.toReal) ^ (1 / p.toReal) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₆ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ ^ (p.toReal * (1 / p.toReal)) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₇ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * HPow.hPow (β := ℝ) ‖b‖₊ 1 =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
inr₈ :
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr₉ : HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p.toReal) * ‖b‖₊ =
  HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (ENNReal.toReal 1 / p.toReal) * ‖b‖₊
Tactic: simp_rw [nnnorm_eq_sum hp, Function.const_apply, Finset.sum_const,
      Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
      mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)],
  nnnorm (E := WithLp ∞ (ι → β)) (toLp ∞ (Function.const ι b)) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal * ‖b‖₊
Tactic: rcases em <| p = ∞ with (rfl | hp)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)],
    nnnorm (E := WithLp ∞ (ι → β)) (toLp ∞ (Function.const ι b)) =
      HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (HDiv.hDiv (α := ℝ≥0∞) 1 ∞).toReal * ‖b‖₊
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
have inr : ∀ (hp_1 : ¬p = ∞), ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊
Tactic: rcases em <| p = ∞ with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
inst_2 : DecidableEq ι
i : ι
⊢ Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    ((basisFun p 𝕜 ι : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
have simp_rw : Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
  ((Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i :
    PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
  (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
Tactic: simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
inst_2 : DecidableEq ι
i : ι
simp_rw :
  Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    ((Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i :
      PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
⊢ Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    ((basisFun p 𝕜 ι : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
have simp_rw₁ : Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
  (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) : (ι → 𝕜) ≃ₗ[𝕜] PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜) :
      (a : ι → 𝕜) → PiLp p fun (x : ι) ↦ 𝕜)
    (Pi.single (M := fun (a : ι) ↦ 𝕜) i 1))
  (single p (β := fun (x : ι) ↦ 𝕜) i 1)
Tactic: simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
inst_2 : DecidableEq ι
i : ι
simp_rw :
  Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    ((Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i :
      PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
simp_rw₁ :
  Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (((LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι → 𝕜)) : (ι → 𝕜) ≃ₗ[𝕜] PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜) :
        (a : ι → 𝕜) → PiLp p fun (x : ι) ↦ 𝕜)
      (Pi.single (M := fun (a : ι) ↦ 𝕜) i 1))
    (single p (β := fun (x : ι) ↦ 𝕜) i 1)
⊢ Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    ((basisFun p 𝕜 ι : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) i : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
    (single p (β := fun (x : ι) ↦ 𝕜) i 1 : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)
have simp_rw₂ : Eq (α := PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜) (toLp p (Pi.single (M := fun (a : ι) ↦ 𝕜) i 1))
  (single p (β := fun (x : ι) ↦ 𝕜) i 1)
Tactic: simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
𝕜 : Type u_5
inst_1 : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp.{u_2, u_5} p fun (x : ι) ↦ 𝕜)
A : Matrix ι ι 𝕜
⊢ b.toMatrix (⇑(basisFun p 𝕜 ι) : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) * A =
    (of : (a : ι → ι → 𝕜) → Matrix ι ι 𝕜) fun (i j : ι) ↦
      (((b.repr : (a : PiLp p fun (x : ι) ↦ 𝕜) → ι →₀ 𝕜) (toLp p (Aᵀ j)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i
have this : (b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun (x : ι) ↦ 𝕜) i))).toMatrix (⇑(Pi.basisFun 𝕜 ι) : (a : ι) → ι → 𝕜) * A =
  (of : (a : ι → ι → 𝕜) → Matrix ι ι 𝕜) fun (i j : ι) ↦
    ((((b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun (x : ι) ↦ 𝕜) i))).repr : (a : ι → 𝕜) → ι →₀ 𝕜) (A.col j) :
          ι →₀ 𝕜) :
        (a : ι) → 𝕜)
      i
Tactic: have := basis_toMatrix_basisFun_mul (b.map (WithLp.linearEquiv _ 𝕜 _)) A
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
ι : Type u_2
inst : Fintype ι
𝕜 : Type u_5
inst_1 : SeminormedCommRing 𝕜
b : Basis ι 𝕜 (PiLp.{u_2, u_5} p fun (x : ι) ↦ 𝕜)
A : Matrix ι ι 𝕜
this :
  (b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun (x : ι) ↦ 𝕜) i))).toMatrix (⇑(Pi.basisFun 𝕜 ι) : (a : ι) → ι → 𝕜) * A =
    (of : (a : ι → ι → 𝕜) → Matrix ι ι 𝕜) fun (i j : ι) ↦
      ((((b.map (WithLp.linearEquiv p 𝕜 ((i : ι) → (fun (x : ι) ↦ 𝕜) i))).repr : (a : ι → 𝕜) → ι →₀ 𝕜) (A.col j) :
            ι →₀ 𝕜) :
          (a : ι) → 𝕜)
        i
⊢ b.toMatrix (⇑(basisFun p 𝕜 ι) : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) * A =
    (of : (a : ι → ι → 𝕜) → Matrix ι ι 𝕜) fun (i j : ι) ↦
      (((b.repr : (a : PiLp p fun (x : ι) ↦ 𝕜) → ι →₀ 𝕜) (toLp p (Aᵀ j)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i
have this₁ : (b.toMatrix fun (x : ι) ↦ (basisFun p 𝕜 ι : (a : ι) → PiLp p fun (x : ι) ↦ 𝕜) x) * A =
  (of : (a : ι → ι → 𝕜) → Matrix ι ι 𝕜) fun (i j : ι) ↦
    (((b.repr : (a : PiLp p fun (x : ι) ↦ 𝕜) → ι →₀ 𝕜)
            (Equiv.invFun (AddEquiv.toEquiv (WithLp.addEquiv p (ι → 𝕜))) (A.col j)) :
          ι →₀ 𝕜) :
        (a : ι) → 𝕜)
      i
Tactic: simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply,
    WithLp.linearEquiv_symm_apply, Basis.toMatrix_map, Function.comp_def, Basis.map_apply,
    LinearEquiv.symm_apply_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist x y = ‖toLp p (-x + y)‖
have rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₃ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst_3 : SeminormedRing R
inst_4 : (i : ι) → Module.{u_5, u_3} R (α i)
inst_5 : ∀ (i : ι), IsBoundedSMul.{u_5, u_3} R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
⊢ IsBoundedSMul R ((i : ι) → α i)
have refine_1 : ∀ (x : R) (y z : (i : ι) → α i), dist (x • y) (x • z) ≤ dist x 0 * dist y z
Tactic: refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst_3 : SeminormedRing R
inst_4 : (i : ι) → Module.{u_5, u_3} R (α i)
inst_5 : ∀ (i : ι), IsBoundedSMul.{u_5, u_3} R (α i)
this : PseudoMetricSpace ((i : ι) → α i) := pseudoMetricSpaceToPi p α
refine_1 : ∀ (x : R) (y z : (i : ι) → α i), dist (x • y) (x • z) ≤ dist x 0 * dist y z
⊢ IsBoundedSMul R ((i : ι) → α i)
have refine_2 : ∀ (x y : R) (z : (i : ι) → α i), dist (x • z) (y • z) ≤ dist x y * dist z 0
Tactic: refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst_3 : SeminormedRing R
inst_4 : (i : ι) → Module.{u_5, u_3} R (α i)
inst_5 : ∀ (i : ι), NormSMulClass.{u_5, u_3} R (α i)
this : SeminormedAddCommGroup ((i : ι) → α i) := seminormedAddCommGroupToPi p α
⊢ NormSMulClass R ((i : ι) → α i)
have refine : ∀ (x : R) (y : (i : ι) → α i), ‖x • y‖ = ‖x‖ * ‖y‖
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
R : Type u_5
inst_3 : NormedField R
inst_4 : (i : ι) → NormedSpace.{u_5, u_3} R (α i)
this : SeminormedAddCommGroup ((i : ι) → α i) := seminormedAddCommGroupToPi p α
⊢ NormedSpace R ((i : ι) → α i)
have refine : ∀ (x : R) (y : (i : ι) → α i), ‖x • y‖ ≤ ‖x‖ * ‖y‖
Tactic: refine ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist x y = 0
⊢ x = y
have h₁ : dist (toLp p x) (toLp p y) = 0
Tactic: rw [dist_pseudoMetricSpaceToPi] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (hypothesis)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist (toLp p x) (toLp p y) = 0
⊢ x = y
have h₁ : toLp p x = toLp p y
Tactic: apply eq_of_dist_eq_zero at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
⊢ dist x y = ‖toLp p (-x + y)‖
have rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.PiLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
rw : dist (toLp p x) (toLp p y) = ‖toLp p (-x + y)‖
rw₁ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x + y)‖
rw₂ : ‖-toLp p x + toLp p y‖ = ‖toLp p (-x) + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖
have rw₃ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
Tactic: rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]