awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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 ∞
inr₁ : ∀ (_h : 0 < p.toReal), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p

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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Finite α
f : (i : α) → E i
⊢ Memℓp (E := E) f 0

Tactic:
memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite

Premises used: Iff.mpr, memℓp_zero_iff, setOf, Ne, Set.toFinite, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Finite α
f : (i : α) → E i
⊢ Memℓp (E := E) f 0

Tactic:
exact memℓp_zero_iff.mpr { i : α | f i ≠ 0 }.toFinite

Premises used: Iff.mpr, memℓp_zero_iff, setOf, Ne, Set.toFinite, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Finite α
f : (i : α) → E i
⊢ Memℓp (E := E) f ∞

Tactic:
memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)

Premises used: Iff.mpr, Norm.norm, memℓp_infty_iff, Set.toFinite, Set.range, Set.Finite.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Finite α
f : (i : α) → E i
⊢ Memℓp (E := E) f ∞

Tactic:
exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α ↦ ‖f i‖).toFinite)

Premises used: Iff.mpr, Norm.norm, memℓp_infty_iff, Set.toFinite, Set.range, Set.Finite.bddAbove
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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
inr : ∀ (val : Fintype α), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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
val : Fintype α
⊢ Memℓp (E := E) f p

Tactic:
memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩

Premises used: Finset.univ, hasSum_fintype, memℓp_gen, Exists.intro, Finset.sum, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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
val : Fintype α
⊢ Memℓp (E := E) f p

Tactic:
exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩

Premises used: Finset.univ, hasSum_fintype, memℓp_gen, Exists.intro, Finset.sum, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : ↥(lp E p)
⊢ ofLp (p := p) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f) = (↑f : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : PiLp p E
⊢ (↑((Equiv.symm (Equiv.lpPiLp (E := E)) : (a : PiLp p E) → ↥(lp E p)) f) : (i : α) → E i) = f.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : ↥(lp E p)
⊢ ofLp (p := p) ((AddEquiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f) = (↑f : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Finite α
f : PiLp p E
⊢ (↑((AddEquiv.symm (AddEquiv.lpPiLp (E := E)) : (a : PiLp p E) → ↥(lp E p)) f) : (i : α) → E i) = f.ofLp

Tactic:
rfl

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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Fintype α
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:
simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]

Premises used: Equiv.lpPiLp, lp.norm_eq_card_dsupport, PiLp.norm_eq_card
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Fintype α
f : ↥(lp E ∞)
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‖)
⊢ norm (E := PiLp ∞ E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E ∞)) → PiLp ∞ E) f : PiLp ∞ E) = ‖f‖

Tactic:
rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]

Premises used: PiLp.norm_eq_ciSup, lp.norm_eq_ciSup
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : Fintype α
f : ↥(lp E ∞)
⊢ 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:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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
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)
⊢ norm (E := PiLp p E) ((Equiv.lpPiLp (E := E) : (a : ↥(lp E p)) → PiLp p E) f : PiLp p E) = ‖f‖

Tactic:
rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]

Premises used: PiLp.norm_eq_sum, tsum_fintype, lp.norm_eq_tsum_rpow
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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
⊢ 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:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : α) → NormedSpace.{u_3, u_2} 𝕜 (E i)
inst_4 : Fact (1 ≤ p)
f : ↥(lp E p)
⊢ ofLp (p := p) ((lpPiLpₗᵢ E 𝕜 : (a : ↥(lp E p)) → PiLp p E) f) = (↑f : (i : α) → E i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : α → Type u_2
inst : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst_1 : Fintype α
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : α) → NormedSpace.{u_3, u_2} 𝕜 (E i)
inst_4 : Fact (1 ≤ p)
f : PiLp p E
⊢ (↑((LinearIsometryEquiv.symm (lpPiLpₗᵢ E 𝕜) : (a : PiLp p E) → ↥(lp E p)) f) : (i : α) → E i) = f.ofLp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : Type u_2
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NormedAddCommGroup E
f : ↥(lp (fun (x : α) ↦ E) ∞)
⊢ (⇑((AddEquiv.lpBCF : (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E) f : α →ᵇ E) : (a : α) → E) =
    (↑f : (i : α) → (fun (x : α) ↦ E) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : Type u_2
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NormedAddCommGroup E
f : α →ᵇ E
⊢ Eq (α := (i : α) → (fun (x : α) ↦ E) i)
    (↑((AddEquiv.symm AddEquiv.lpBCF : (a : α →ᵇ E) → ↥(lp (fun (x : α) ↦ E) ∞)) f) : (i : α) → (fun (x : α) ↦ E) i)
    (⇑f : (a : α) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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) ∞)
simp :
  Eq (α := ℝ)
    (⨆ (x : α),
      norm.{u_2} (E := E)
        (((({ toFun := Equiv.toFun (AddEquiv.toEquiv AddEquiv.lpBCF), map_add' := ⋯, map_smul' := ⋯,
                      invFun := Equiv.invFun (AddEquiv.toEquiv AddEquiv.lpBCF), left_inv := ⋯, right_inv := ⋯ } :
                    (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E)
                  f :
                α →ᵇ E) :
              (a : α) → E)
            x :
          E))
    (⨆ (i : α), ‖(↑f : (i : α) → E) i‖)
⊢ 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‖

Tactic:
simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]

Premises used: lp.norm_eq_ciSup, BoundedContinuousFunction.norm_eq_iSup_norm
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
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) ∞)
⊢ Eq (α := ℝ)
    (⨆ (x : α),
      norm.{u_2} (E := E)
        (((({ toFun := Equiv.toFun (AddEquiv.toEquiv AddEquiv.lpBCF), map_add' := ⋯, map_smul' := ⋯,
                      invFun := Equiv.invFun (AddEquiv.toEquiv AddEquiv.lpBCF), left_inv := ⋯, right_inv := ⋯ } :
                    (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E)
                  f :
                α →ᵇ E) :
              (a : α) → E)
            x :
          E))
    (⨆ (i : α), ‖(↑f : (i : α) → E) i‖)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_5
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : ↥(lp (fun (x : α) ↦ E) ∞)
⊢ (⇑((lpBCFₗᵢ E 𝕜 : (a : ↥(lp (fun (x : α) ↦ E) ∞)) → α →ᵇ E) f : α →ᵇ E) : (a : α) → E) =
    (↑f : (i : α) → (fun (x : α) ↦ E) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_5
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : α →ᵇ E
⊢ Eq (α := (i : α) → (fun (x : α) ↦ E) i)
    (↑((LinearIsometryEquiv.symm (lpBCFₗᵢ E 𝕜) : (a : α →ᵇ E) → ↥(lp (fun (x : α) ↦ E) ∞)) f) :
      (i : α) → (fun (x : α) ↦ E) i)
    (⇑f : (a : α) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
R : Type u_3
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NonUnitalNormedRing R
f : ↥(lp (fun (x : α) ↦ R) ∞)
⊢ (⇑((RingEquiv.lpBCF : (a : ↥(lp (fun (x : α) ↦ R) ∞)) → α →ᵇ R) f : α →ᵇ R) : (a : α) → R) =
    (↑f : (i : α) → (fun (x : α) ↦ R) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
R : Type u_3
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
inst_2 : NonUnitalNormedRing R
f : α →ᵇ R
⊢ Eq (α := (i : α) → (fun (x : α) ↦ R) i)
    (↑((RingEquiv.symm RingEquiv.lpBCF : (a : α →ᵇ R) → ↥(lp (fun (x : α) ↦ R) ∞)) f) : (i : α) → (fun (x : α) ↦ R) i)
    (⇑f : (a : α) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
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
f : ↥(lp (fun (x : α) ↦ A) ∞)
⊢ (⇑((AlgEquiv.lpBCF α 𝕜 : (a : ↥(lp (fun (x : α) ↦ A) ∞)) → α →ᵇ A) f : α →ᵇ A) : (a : α) → A) =
    (↑f : (i : α) → (fun (x : α) ↦ A) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.LpEquiv
Goal:
α : Type u_1
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
f : α →ᵇ A
⊢ Eq (α := (i : α) → (fun (x : α) ↦ A) i)
    (↑((AlgEquiv.symm (AlgEquiv.lpBCF α 𝕜) : (a : α →ᵇ A) → ↥(lp (fun (x : α) ↦ A) ∞)) f) :
      (i : α) → (fun (x : α) ↦ A) i)
    (⇑f : (a : α) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p q : ℝ≥0∞
A : Matrix m n R
x : n → R
⊢ Eq (α := WithLp q (m → R))
    ((((toLpLin p q : (a : Matrix m n R) → WithLp p (n → R) →ₗ[R] WithLp q (m → R)) A :
            WithLp p (n → R) →ₗ[R] WithLp q (m → R)) :
          (a : WithLp p (n → R)) → WithLp q (m → R))
        (toLp p x) :
      WithLp q (m → R))
    (toLp q ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x) :
      WithLp q (m → R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p q : ℝ≥0∞
A : Matrix m n R
x : WithLp p (n → R)
⊢ Eq (α := m → R)
    (ofLp (p := q)
        ((((toLpLin p q : (a : Matrix m n R) → WithLp p (n → R) →ₗ[R] WithLp q (m → R)) A :
              WithLp p (n → R) →ₗ[R] WithLp q (m → R)) :
            (a : WithLp p (n → R)) → WithLp q (m → R))
          x) :
      m → R)
    ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) A : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x.ofLp :
      m → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p q : ℝ≥0∞
M : Matrix m n R
v : WithLp p (n → R)
⊢ (((toLpLin p q : (a : Matrix m n R) → WithLp p (n → R) →ₗ[R] WithLp q (m → R)) M :
          WithLp p (n → R) →ₗ[R] WithLp q (m → R)) :
        (a : WithLp p (n → R)) → WithLp q (m → R))
      v =
    toLp q (M *ᵥ v.ofLp)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p q : ℝ≥0∞
inst_3 : Finite m
⊢ Eq (α := Matrix m n R ≃ₗ[R] WithLp p (n → R) →ₗ[R] WithLp q (m → R)) (toLpLin p q)
    (toLin (PiLp.basisFun p R n) (PiLp.basisFun q R m))

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.toLin, LinearEquiv.symm, Function.update, dotProduct, Pi.single, dite, Matrix.mulVec, LinearEquiv.trans, Finset.sum, rfl
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p : ℝ≥0∞
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)
⊢ 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

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p : ℝ≥0∞
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:
simp
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
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
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
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
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:
simp
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
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 : ℝ≥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 p (m → R))
    ((toLpLin p p : (a : Matrix m o R) → WithLp p (o → R) →ₗ[R] WithLp p (m → R)) (A * B) :
      WithLp p (o → R) →ₗ[R] WithLp p (m → R))
    ((toLpLin p p : (a : Matrix m n R) → WithLp p (n → R) →ₗ[R] WithLp p (m → R)) A ∘ₗ
        (toLpLin p p : (a : Matrix n o R) → WithLp p (o → R) →ₗ[R] WithLp p (n → R)) B :
      WithLp p (o → R) →ₗ[R] WithLp p (m → R))

Tactic:
toLpLin_mul _ _ _ _ _

Premises used: Matrix.toLpLin_mul
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
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))
        ((LinearEquiv.symm (toLpLin p p) : (a : WithLp p (n → R) →ₗ[R] WithLp p (n → R)) → Matrix n n R) LinearMap.id) :
      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 :
      WithLp p (n → R) →ₗ[R] WithLp p (n → R))

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
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 : WithLp q (n → R) →ₗ[R] WithLp r (m → R)
B : WithLp p (o → R) →ₗ[R] WithLp q (n → 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))
        ((LinearEquiv.symm (toLpLin p r) : (a : WithLp p (o → R) →ₗ[R] WithLp r (m → R)) → Matrix m o R) (A ∘ₗ B)) :
      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))
        (HMul.hMul (α := Matrix m n R) (β := Matrix n o R)
          ((LinearEquiv.symm (toLpLin q r) : (a : WithLp q (n → R) →ₗ[R] WithLp r (m → R)) → Matrix m n R) A :
            Matrix m n R)
          ((LinearEquiv.symm (toLpLin p q) : (a : WithLp p (o → R) →ₗ[R] WithLp q (n → R)) → Matrix n o R) B :
            Matrix n o R)) :
      WithLp p (o → R) →ₗ[R] WithLp r (m → R))

Tactic:
simp [toLpLin_mul (q := q)]

Premises used: Matrix.toLpLin_mul
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p : ℝ≥0∞
A : Matrix n n R
k : ℕ
⊢ (toLpLin p p : (a : Matrix n n R) → WithLp p (n → R) →ₗ[R] WithLp p (n → R)) (A ^ k) =
    HPow.hPow (α := 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)) A :
        WithLp p (n → R) →ₗ[R] WithLp p (n → R))
      k

Tactic:
map_pow (toLpLinAlgEquiv p) A k

Premises used: map_pow, Matrix.toLpLinAlgEquiv
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
p : ℝ≥0∞
A : Module.End R (WithLp p (n → R))
k : ℕ
⊢ (LinearEquiv.symm (toLpLin p p) : (a : WithLp p (n → R) →ₗ[R] WithLp p (n → R)) → Matrix n n R) (A ^ k) =
    HPow.hPow (α := Matrix n n R)
      ((LinearEquiv.symm (toLpLin p p) : (a : WithLp p (n → R) →ₗ[R] WithLp p (n → R)) → Matrix n n R) A : Matrix n n R)
      k

Tactic:
map_pow (toLpLinAlgEquiv p).symm A k

Premises used: AlgEquiv.symm, map_pow, Matrix.toLpLinAlgEquiv
-- Module: Mathlib.Analysis.Normed.Lp.Matrix
Goal:
ι : Type u_5
R : Type u_6
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
p : ℝ≥0∞
m : Matrix ι ι R
⊢ (LinearMap.det : (a : WithLp p (ι → R) →ₗ[R] WithLp p (ι → R)) → R)
      ((toLpLin p p : (a : Matrix ι ι R) → WithLp p (ι → R) →ₗ[R] WithLp p (ι → R)) m :
        WithLp p (ι → R) →ₗ[R] WithLp p (ι → R)) =
    m.det

Tactic:
simp [Matrix.toLpLin_eq_toLin]

Premises used: Matrix.toLpLin_eq_toLin
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
⊢ Measurable.{u_1, u_1} (α := WithLp p X) ofLp

Tactic:
comap_measurable _

Premises used: comap_measurable
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
s : Set (WithLp p X)
hs : MeasurableSet s
obtain : ∀ (t : Set X) (ht : MeasurableSet t), MeasurableSet (toLp p ⁻¹' ofLp ⁻¹' t)
⊢ MeasurableSet (toLp p ⁻¹' s)

Tactic:
obtain ⟨t, ht, rfl⟩ := hs

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.MeasurableSpace
Goal:
p : ℝ≥0∞
X : Type u_1
inst : MeasurableSpace X
t : Set X
ht : MeasurableSet t
⊢ MeasurableSet (toLp p ⁻¹' ofLp ⁻¹' t)

Tactic:
simpa [Set.preimage_preimage]

Premises used: Set.preimage_preimage