awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (α × β)),
    edist (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x)
        (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x_2) =
      edist x x_2
inr :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x x_2 : WithLp ∞ (α × β)),
    edist (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x)
        (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x_2) =
      edist x x_2
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x) ((WithLp.congr p (Equiv.prodComm α β)).toFun x_1) = edist x x_1
have inr₁ : ∀ (hp_1 : 0 < p.toReal),
  edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x) ((WithLp.congr p (Equiv.prodComm α β)).toFun x_1) = edist x x_1
Tactic: rcases p.trichotomy with rfl | rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
__spread.0 : WithLp 0 (α × β) ≃ WithLp 0 (β × α) := WithLp.congr 0 (Equiv.prodComm α β)
x x_1 : WithLp 0 (α × β)
⊢ edist (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x) (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x_1) =
    edist x x_1
have inl : ¬LE.le (α := ℝ≥0∞) 1 0
Tactic: absurd hp.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (WithLp p (α × β) × γ)
⊢ edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (WithLp 0 (α × β) × γ)),
  edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x)
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x_2) =
    edist x x_2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, x_1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (WithLp p (α × β) × γ)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (WithLp 0 (α × β) × γ)),
    edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x)
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x_2) =
      edist x x_2
⊢ edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1
have inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x x_2 : WithLp ∞ (WithLp ∞ (α × β) × γ)),
  edist (α := WithLp ∞ (α × WithLp ∞ (β × γ)))
      ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
          (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
        x)
      ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
          (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
        x_2) =
    edist x x_2
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, x_1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
x x_1 : WithLp p (WithLp p (α × β) × γ)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x x_2 : WithLp 0 (WithLp 0 (α × β) × γ)),
    edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x)
        ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
            (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
          x_2) =
      edist x x_2
inr :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x x_2 : WithLp ∞ (WithLp ∞ (α × β) × γ)),
    edist (α := WithLp ∞ (α × WithLp ∞ (β × γ)))
        ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
            (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
          x)
        ((fun (x : WithLp ∞ (WithLp ∞ (α × β) × γ)) ↦
            (WithLp.toLp ∞ (x.fst.fst, WithLp.toLp ∞ (x.fst.snd, x.snd)) : WithLp ∞ (α × WithLp ∞ (β × γ))))
          x_2) =
      edist x x_2
⊢ edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1
have inr₁ : ∀ (hp_1 : 0 < p.toReal),
  edist (α := WithLp p (α × WithLp p (β × γ)))
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x)
      ((fun (x : WithLp p (WithLp p (α × β) × γ)) ↦ WithLp.toLp p (x.fst.fst, WithLp.toLp p (x.fst.snd, x.snd))) x_1) =
    edist x x_1
Tactic: rcases p.trichotomy with rfl | rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x x_1 : WithLp 0 (WithLp 0 (α × β) × γ)
⊢ edist (α := WithLp 0 (α × WithLp 0 (β × γ)))
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x)
      ((fun (x : WithLp 0 (WithLp 0 (α × β) × γ)) ↦
          (WithLp.toLp 0 (x.fst.fst, WithLp.toLp 0 (x.fst.snd, x.snd)) : WithLp 0 (α × WithLp 0 (β × γ))))
        x_1) =
    edist x x_1
have inl : ¬LE.le (α := ℝ≥0∞) 1 0
Tactic: absurd hp.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
⊢ edist x.fst y.fst = edist x y
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x y : WithLp 0 (α × β)), edist x.fst y.fst = edist x y
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x y : WithLp 0 (α × β)), edist x.fst y.fst = edist x y
⊢ edist x.fst y.fst = edist x y
have inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), edist x.fst y.fst = edist x y
Tactic: rcases p.trichotomy with rfl | rfl | hp
Cleared hypotheses: p, hp, x, y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x y : WithLp 0 (α × β)), edist x.fst y.fst = edist x y
inr : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x y : WithLp ∞ (α × β)), edist x.fst y.fst = edist x y
⊢ edist x.fst y.fst = edist x y
have inr₁ : ∀ (hp : 0 < p.toReal), edist x.fst y.fst = edist x y
Tactic: rcases p.trichotomy with rfl | rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
__spread.0 : WithLp 0 (α × β) ≃ α := Equiv.trans (WithLp.equiv 0 (α × β)) (Equiv.prodUnique α β)
x y : WithLp 0 (α × β)
⊢ edist x.fst y.fst = edist x y
have inl : ¬LE.le (α := ℝ≥0∞) 1 0
Tactic: absurd hp.elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = edist x y
have inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst = edist x y
have inr₁ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ :
  edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst = edist x y
have inr₂ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + HPow.hPow (α := ℝ≥0∞) 0 p.toReal) ^ (1 / p.toReal)
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ :
  edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
inr₂ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + HPow.hPow (α := ℝ≥0∞) 0 p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst = edist x y
have inr₃ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + 0) ^ (1 / p.toReal)
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ :
  edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
inr₂ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + HPow.hPow (α := ℝ≥0∞) 0 p.toReal) ^ (1 / p.toReal)
inr₃ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + 0) ^ (1 / p.toReal)
⊢ edist x.fst y.fst = edist x y
have inr₄ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.ProdLp (goal)
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : PseudoEMetricSpace α'
inst_4 : PseudoEMetricSpace β'
inst_5 : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
inr : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
inr₁ :
  edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + edist.{u_3} (α := β) default default ^ p.toReal) ^ (1 / p.toReal)
inr₂ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + HPow.hPow (α := ℝ≥0∞) 0 p.toReal) ^ (1 / p.toReal)
inr₃ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + 0) ^ (1 / p.toReal)
inr₄ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)
⊢ edist x.fst y.fst = edist x y
have inr₅ : edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ p.toReal⁻¹
Tactic: simp_rw [WithLp.prod_edist_eq_add hp, Unique.eq_default, edist_self,
        ENNReal.zero_rpow_of_pos hp, add_zero, one_div, ENNReal.rpow_rpow_inv hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have inl : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
Tactic: rcases eq_or_ne p ∞ with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
inl : ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have inr : ∀ (hp : p ≠ ∞), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
Tactic: rcases eq_or_ne p ∞ with rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
have inl : ∀ (g : E → F) (hg₁ : ContDiff ℝ ∞ g) (hg₂ : ∀ (x : E), dist (g x) (f x) < ε)
  (hg₃ : Function.support g ⊆ Function.support f),
  ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨g, hg₁, hg₂, hg₃⟩ := h₂.exists_contDiff_approx ⊤ (ε := fun _ ↦ ε) (by fun_prop)
      (by intro; positivity)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε
have inl : ∀ (x : E), ‖(f - g) x‖ ≤ ε
Tactic: refine ⟨g, h₁.mono hg₃, hg₁, eLpNormEssSup_le_of_ae_bound (.of_forall fun x ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hf : f =ᶠ[ae μ] 0), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hf : f =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
pos :
  ∀ (hf : f =ᶠ[ae μ] 0), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hf : ¬f =ᶠ[ae μ] 0), ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hf : f =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (goal)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : f =ᶠ[ae μ] 0
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have h : HasCompactSupport.{u_3, u_4} (α := E) (β := F) 0 ∧
  ContDiff.{0, u_3, u_4} ℝ (E := E) (F := F) ∞ 0 ∧ eLpNorm (f - 0) p μ ≤ ENNReal.ofReal ε
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hs₁ : μ (tsupport f) ≠ ⊤ := h₁.measure_lt_top.ne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
have hf₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Measure.measure_support_eq_zero_iff _] at hf
Cleared hypotheses: hf, hs₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.SmoothApprox (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : MeasurableSpace E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : FiniteDimensional ℝ E
inst_5 : BorelSpace E
inst_6 : NormedSpace ℝ F
μ : Measure E
inst_7 : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
hp : p ≠ ∞
hf : ¬f =ᶠ[ae μ] 0
hs₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (tsupport f) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (g : E → F), HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
have hs₂ : 0 < ENNReal.toReal ((μ : (a : Set E) → ℝ≥0∞) (tsupport f))
Tactic: have hs₂ : 0 < (μ <| tsupport f).toReal := by
    -- Since `f` is not the zero function `tsupport f` has positive measure
    rw [← Measure.measure_support_eq_zero_iff _] at hf
    exact toReal_pos (pos_mono (subset_tsupport f) (pos_of_ne_zero hf)).ne' hs₁