awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
ι : Type u_2
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
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:
simp only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero,
      one_mul, nnnorm_eq_ciSup, Function.const_apply, ciSup_const]

Premises used: ENNReal.div_top, Function.const_apply, PiLp.nnnorm_eq_ciSup, ENNReal.toReal_zero, NNReal.rpow_zero, ciSup_const, one_mul
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
hp : ¬p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
nnnorm_toLp_const hp b

Premises used: PiLp.nnnorm_toLp_const
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
hp : ¬p = ∞
⊢ ‖toLp p (Function.const ι b)‖₊ = HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊

Tactic:
exact nnnorm_toLp_const hp b

Premises used: PiLp.nnnorm_toLp_const
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
b : β
⊢ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊) : ℝ) =
    (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ) ^ (1 / p).toReal * ‖b‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
inst_2 : Nonempty ι
b : β
⊢ (↑(HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * ‖b‖₊) : ℝ) =
    (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ) ^ (1 / p).toReal * ‖b‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
inst_2 : One β
⊢ nnnorm (E := WithLp p (ι → β)) (toLp p 1) =
    HPow.hPow (α := ℝ≥0) (↑(Fintype.card ι) : ℝ≥0) (1 / p).toReal * nnnorm.{u_5} (E := β) 1

Tactic:
(nnnorm_toLp_const hp (1 : β)).trans rfl

Premises used: setOf, OfNat.ofNat, PiLp.nnnorm_toLp_const, rfl, Eq.trans
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
hp_1 : Fact (1 ≤ p)
inst : Fintype ι
β : Type u_5
inst_1 : SeminormedAddCommGroup β
hp : p ≠ ∞
inst_2 : One β
⊢ Norm.norm (E := WithLp p (ι → β)) (toLp p 1) =
    (↑(↑(Fintype.card ι) : ℝ≥0) : ℝ) ^ (1 / p).toReal * Norm.norm.{u_5} (E := β) 1

Tactic:
(norm_toLp_const hp (1 : β)).trans rfl

Premises used: setOf, PiLp.norm_toLp_const, OfNat.ofNat, rfl, Eq.trans
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
β : ι → Type u_4
inst : Semiring 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
⊢ Eq (α := (a : PiLp p β) → (i : ι) → β i) (⇑(continuousLinearEquiv p 𝕜 β) : (a : PiLp p β) → (i : ι) → β i) ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
β : ι → Type u_4
inst : Semiring 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (β i)
inst_2 : (i : ι) → Module.{u_1, u_4} 𝕜 (β i)
⊢ Eq (α := (a : (i : ι) → β i) → PiLp p β)
    (⇑(ContinuousLinearEquiv.symm (continuousLinearEquiv p 𝕜 β)) : (a : (i : ι) → β i) → PiLp p β) (toLp p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)
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)
⊢ 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 : ι) ↦ 𝕜)

Tactic:
simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv, toLp_single]

Premises used: PiLp.toLp_single, PiLp.basisFun, Module.Basis.coe_ofEquivFun, WithLp.coe_symm_linearEquiv
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
x : PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜
i : ι
⊢ (((Basis.repr (basisFun p 𝕜 ι) : (a : PiLp p fun (x : ι) ↦ 𝕜) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) i = x.ofLp i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
⊢ Eq (α := (PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜) ≃ₗ[𝕜] ι → 𝕜) (Basis.equivFun (basisFun p 𝕜 ι))
    (WithLp.linearEquiv p 𝕜 (ι → 𝕜))

Tactic:
Basis.equivFun_ofEquivFun _

Premises used: Module.Basis.equivFun_ofEquivFun, PiLp.basisFun
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
⊢ Eq (α := Basis ι 𝕜 (PiLp.{u_2, u_1} p fun (x : ι) ↦ 𝕜)) (basisFun p 𝕜 ι)
    (Basis.map (Pi.basisFun 𝕜 ι) (LinearEquiv.symm (WithLp.linearEquiv p 𝕜 (ι → 𝕜))))

Tactic:
rfl

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, Module.Basis.map, PiLp.basisFun, LinearEquiv.trans, rfl, WithLp.linearEquiv
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst : Finite ι
inst_1 : Ring 𝕜
⊢ Eq (α := Basis ι 𝕜 (ι → 𝕜)) (Basis.map (basisFun p 𝕜 ι) (WithLp.linearEquiv p 𝕜 (ι → 𝕜))) (Pi.basisFun 𝕜 ι)

Tactic:
rfl

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, Module.Basis.map, LinearEquiv.toEquiv, Pi.basisFun, LinearEquiv.refl, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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.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
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 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

Premises used: Module.Basis.map_repr, Module.Basis.toMatrix_map, LinearEquiv.symm_apply_apply, LinearEquiv.trans_apply, Module.Basis.map_apply, Function.comp_def, PiLp.basisFun_map, WithLp.linearEquiv_symm_apply
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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.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
⊢ 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

Tactic:
this

Premises used: Matrix.col
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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.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
⊢ 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

Tactic:
exact this
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → PseudoMetricSpace (α i)
x y : (i : ι) → α i
⊢ dist x y = dist (toLp p x) (toLp p y)

Tactic:
rfl

Premises used: rfl
-- 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 : 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‖
rw₃ rw₄ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

Premises used: SeminormedAddCommGroup.dist_eq, PiLp.dist_pseudoMetricSpaceToPi, WithLp.toLp_neg, WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x : (i : ι) → α i
⊢ ‖x‖ = ‖toLp p x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
Goal:
p : ℝ≥0∞
ι : Type u_2
α : ι → Type u_3
inst : Fact (1 ≤ p)
inst_1 : Fintype ι
inst_2 : (i : ι) → SeminormedAddCommGroup (α i)
x : (i : ι) → α i
⊢ ‖x‖₊ = ‖toLp p x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)

Tactic:
⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩

Premises used: IsBoundedSMul.mk
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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
refine_2 : ∀ (x y : R) (z : (i : ι) → α i), dist (x • z) (y • z) ≤ dist x y * dist z 0
⊢ IsBoundedSMul R ((i : ι) → α i)

Tactic:
refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 α
x : R
y z : (i : ι) → α i
⊢ dist (x • y) (x • z) ≤ dist x 0 * dist y z

Tactic:
simpa [dist_pseudoMetricSpaceToPi] using dist_smul_pair x (toLp p y) (toLp p z)

Premises used: WithLp.toLp, PiLp.dist_pseudoMetricSpaceToPi, dist_smul_pair
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 α
x y : R
z : (i : ι) → α i
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0

Tactic:
simpa [dist_pseudoMetricSpaceToPi] using dist_pair_smul x y (toLp p z)

Premises used: dist_pair_smul, WithLp.toLp, PiLp.dist_pseudoMetricSpaceToPi
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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)

Tactic:
⟨fun x y ↦ ?_⟩

Premises used: NormSMulClass.mk
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 α
refine : ∀ (x : R) (y : (i : ι) → α i), ‖x • y‖ = ‖x‖ * ‖y‖
⊢ NormSMulClass R ((i : ι) → α i)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Lp.PiLp
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 α
x : R
y : (i : ι) → α i
⊢ ‖x • y‖ = ‖x‖ * ‖y‖

Tactic:
simp [norm_seminormedAddCommGroupToPi, norm_smul]

Premises used: norm_smul, PiLp.norm_seminormedAddCommGroupToPi
-- 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 : 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 α
refine : ∀ (x : R) (y : (i : ι) → α i), ‖x • y‖ ≤ ‖x‖ * ‖y‖
⊢ NormedSpace R ((i : ι) → α i)

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- 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 : 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 α
x : R
y : (i : ι) → α i
⊢ ‖x • y‖ ≤ ‖x‖ * ‖y‖

Tactic:
simp [norm_seminormedAddCommGroupToPi, norm_smul]

Premises used: norm_smul, PiLp.norm_seminormedAddCommGroupToPi
-- 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 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist x y = 0
⊢ dist (toLp p x) (toLp p y) = 0

Tactic:
rw [dist_pseudoMetricSpaceToPi] at h

Premises used: PiLp.dist_pseudoMetricSpaceToPi
-- 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 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : dist (toLp p x) (toLp p y) = 0
⊢ toLp p x = toLp p y

Tactic:
apply eq_of_dist_eq_zero at h

Premises used: eq_of_dist_eq_zero
-- 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 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : toLp p x = toLp p y
⊢ x = y

Tactic:
WithLp.toLp_injective p h

Premises used: WithLp.toLp_injective
-- 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 : Fintype ι
inst_2 : (i : ι) → NormedAddCommGroup (α i)
x y : (i : ι) → α i
h : toLp p x = toLp p y
⊢ x = y

Tactic:
exact WithLp.toLp_injective p h

Premises used: WithLp.toLp_injective
-- 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 : 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‖
rw₃ rw₄ : ‖-toLp p x + toLp p y‖ = ‖-toLp p x + toLp p y‖
⊢ dist x y = ‖toLp p (-x + y)‖

Tactic:
rw [dist_pseudoMetricSpaceToPi, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

Premises used: SeminormedAddCommGroup.dist_eq, PiLp.dist_pseudoMetricSpaceToPi, WithLp.toLp_neg, WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
⊢ Eq.{u_2 + 1} (α := α) (WithLp.fst.{u_2, u_3} (p := p) (β := β) 0) 0

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
⊢ Eq.{u_3 + 1} (α := β) (WithLp.snd.{u_2, u_3} (p := p) (α := α) 0) 0

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x y : WithLp p (α × β)
⊢ (x + y).fst = x.fst + y.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x y : WithLp p (α × β)
⊢ (x + y).snd = x.snd + y.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x y : WithLp p (α × β)
⊢ (x - y).fst = x.fst - y.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x y : WithLp p (α × β)
⊢ (x - y).snd = x.snd - y.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x : WithLp p (α × β)
⊢ (-x).fst = -x.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : AddCommGroup α
inst_1 : AddCommGroup β
x : WithLp p (α × β)
⊢ (-x).snd = -x.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup α
inst_2 : AddCommGroup β
x : WithLp p (α × β)
c : 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
⊢ (c • x).fst = c • x.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring 𝕜
inst_1 : AddCommGroup α
inst_2 : AddCommGroup β
x : WithLp p (α × β)
c : 𝕜
inst_3 : Module 𝕜 α
inst_4 : Module 𝕜 β
⊢ (c • x).snd = c • x.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
x : α × β
⊢ (toLp p x).fst = x.1

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
x : α × β
⊢ (toLp p x).snd = x.2

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
x : WithLp p (α × β)
⊢ x.ofLp.1 = x.fst

Tactic:
rfl

Premises used: WithLp.fst, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
x : WithLp p (α × β)
⊢ x.ofLp.2 = x.snd

Tactic:
rfl

Premises used: WithLp.snd, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : EDist α
inst_1 : EDist β
f g : WithLp 0 (α × β)
⊢ (if Eq (α := ℝ≥0∞) 0 0 then
      HAdd.hAdd (α := ℝ≥0∞) (if edist f.fst g.fst = 0 then 0 else 1) (if edist f.snd g.snd = 0 then 0 else 1)
    else
      if Eq (α := ℝ≥0∞) 0 ∞ then max (edist f.fst g.fst) (edist f.snd g.snd)
      else (edist f.fst g.fst ^ ENNReal.toReal 0 + edist f.snd g.snd ^ ENNReal.toReal 0) ^ (1 / ENNReal.toReal 0)) =
    HAdd.hAdd (α := ℝ≥0∞) (if edist f.fst g.fst = 0 then 0 else 1) (if edist f.snd g.snd = 0 then 0 else 1)

Tactic:
if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : EDist α
inst_1 : EDist β
f g : WithLp 0 (α × β)
⊢ edist f g = HAdd.hAdd (α := ℝ≥0∞) (if edist f.fst g.fst = 0 then 0 else 1) (if edist f.snd g.snd = 0 then 0 else 1)

Tactic:
convert! if_pos rfl

Premises used: if_pos, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : EDist α
inst_1 : EDist β
hp : 0 < p.toReal
f g : WithLp p (α × β)
⊢ edist f g = (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
let hp' := ENNReal.toReal_pos_iff.mp hp
  (if_neg hp'.1.ne').trans (if_neg hp'.2.ne)

Premises used: ENNReal.toReal_pos_iff, dite, LT.lt.ne', And.right, And.left, Iff.mp, if_neg, Eq.trans, LT.lt.ne, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : EDist α
inst_1 : EDist β
f g : WithLp ∞ (α × β)
⊢ edist f g = max (edist f.fst g.fst) (edist f.snd g.snd)

Tactic:
rfl

Premises used: dite, rfl, ite
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp p (α × β)
inl : ∀ (f : WithLp 0 (α × β)), edist f f = 0
inr : ∀ (f : WithLp ∞ (α × β)), edist f f = 0
inr₁ : ∀ (h : 0 < p.toReal), edist f f = 0
⊢ edist f f = 0

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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp 0 (α × β)
⊢ edist f f = 0

Tactic:
classical
    simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : WithLp ∞ (α × β)
⊢ edist f f = 0

Tactic:
simp [prod_edist_eq_sup]

Premises used: WithLp.prod_edist_eq_sup