awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ toLp p (x.fst, x.snd) = x

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemFst = idemSnd
rw₁ rw₂ : Eq (α := AddMonoid.End (WithLp p (α × β))) idemSnd idemSnd
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemFst = idemSnd

Tactic:
rw [← idemFst_add_idemSnd, add_sub_cancel_left]

Premises used: add_sub_cancel_left, WithLp.idemFst_add_idemSnd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
rw : HAdd.hAdd (α := AddMonoid.End (WithLp p (α × β))) idemFst idemSnd - idemSnd = idemFst
rw₁ rw₂ : Eq (α := AddMonoid.End (WithLp p (α × β))) idemFst idemFst
⊢ HSub.hSub (α := AddMonoid.End (WithLp p (α × β))) 1 idemSnd = idemFst

Tactic:
rw [← idemFst_add_idemSnd, add_sub_cancel_right]

Premises used: WithLp.idemFst_add_idemSnd, add_sub_cancel_right
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp ∞ (α × β)
rw :
  max (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (x.fst, 0))) (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (0, x.snd))) =
    max (Norm.norm (E := WithLp ∞ (α × β)) ((idemFst : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
      (Norm.norm (E := WithLp ∞ (α × β)) ((idemSnd : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
⊢ ‖x‖ =
    max (Norm.norm (E := WithLp ∞ (α × β)) ((idemFst : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
      (Norm.norm (E := WithLp ∞ (α × β)) ((idemSnd : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))

Tactic:
rw [WithLp.prod_norm_eq_sup, ← WithLp.norm_toLp_fst ∞ α β x.fst,
    ← WithLp.norm_toLp_snd ∞ α β x.snd]

Premises used: WithLp.snd, WithLp.norm_toLp_fst, WithLp.fst, WithLp.prod_norm_eq_sup, WithLp.norm_toLp_snd, Top.top
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp ∞ (α × β)
⊢ max (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (x.fst, 0))) (Norm.norm (E := WithLp ∞ (α × β)) (toLp ∞ (0, x.snd))) =
    max (Norm.norm (E := WithLp ∞ (α × β)) ((idemFst : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))
      (Norm.norm (E := WithLp ∞ (α × β)) ((idemSnd : (a : WithLp ∞ (α × β)) → WithLp ∞ (α × β)) x : WithLp ∞ (α × β)))

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
inst_2 : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
rw :
  (Norm.norm (E := WithLp p (α × β)) (toLp p (x.fst, 0)) ^ p.toReal +
        Norm.norm (E := WithLp p (α × β)) (toLp p (0, x.snd)) ^ p.toReal) ^
      (1 / p.toReal) =
    (Norm.norm (E := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal +
        Norm.norm (E := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal) ^
      (1 / p.toReal)
⊢ ‖x‖ =
    (Norm.norm (E := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal +
        Norm.norm (E := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal) ^
      (1 / p.toReal)

Tactic:
rw [WithLp.prod_norm_eq_add hp, ← WithLp.norm_toLp_fst p α β x.fst,
    ← WithLp.norm_toLp_snd p α β x.snd]

Premises used: WithLp.prod_norm_eq_add, WithLp.snd, WithLp.norm_toLp_fst, WithLp.fst, WithLp.norm_toLp_snd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
p : ℝ≥0∞
inst_2 : Fact (1 ≤ p)
hp : 0 < p.toReal
x : WithLp p (α × β)
⊢ (Norm.norm (E := WithLp p (α × β)) (toLp p (x.fst, 0)) ^ p.toReal +
        Norm.norm (E := WithLp p (α × β)) (toLp p (0, x.snd)) ^ p.toReal) ^
      (1 / p.toReal) =
    (Norm.norm (E := WithLp p (α × β)) ((idemFst : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal +
        Norm.norm (E := WithLp p (α × β)) ((idemSnd : (a : WithLp p (α × β)) → WithLp p (α × β)) x : WithLp p (α × β)) ^
          p.toReal) ^
      (1 / p.toReal)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
rw :
  (Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
          ENNReal.toReal 1 +
        Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
          ENNReal.toReal 1) ^
      (1 / ENNReal.toReal 1) =
    Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) +
      Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β))
⊢ ‖x‖ =
    Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) +
      Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β))

Tactic:
rw [prod_norm_eq_add_idemFst (lt_of_lt_of_eq zero_lt_one toReal_one.symm)]

Premises used: ENNReal.toReal_one, WithLp.prod_norm_eq_add_idemFst, zero_lt_one, lt_of_lt_of_eq, Eq.symm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ (Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
          ENNReal.toReal 1 +
        Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) ^
          ENNReal.toReal 1) ^
      (1 / ENNReal.toReal 1) =
    Norm.norm (E := WithLp 1 (α × β)) ((idemFst : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β)) +
      Norm.norm (E := WithLp 1 (α × β)) ((idemSnd : (a : WithLp 1 (α × β)) → WithLp 1 (α × β)) x : WithLp 1 (α × β))

Tactic:
simp only [toReal_one, Real.rpow_one, ne_eq, one_ne_zero, not_false_eq_true, div_self]

Premises used: ENNReal.toReal_one, ne_eq, Real.rpow_one, one_ne_zero, not_false_eq_true, div_self
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
x y : α × β
⊢ dist x y = dist (toLp p x) (toLp p y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
x y : α × β
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_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

Premises used: SeminormedAddCommGroup.dist_eq, WithLp.toLp_neg, WithLp.dist_pseudoMetricSpaceToProd, WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α × β
⊢ ‖x‖ = ‖toLp p x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
x : α × β
⊢ ‖x‖₊ = ‖toLp p x‖₊

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
⊢ IsBoundedSMul R (α × β)

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

Premises used: IsBoundedSMul.mk
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
refine_1 : ∀ (x : R) (y z : α × β), dist (x • y) (x • z) ≤ dist x 0 * dist y z
refine_2 : ∀ (x y : R) (z : α × β), dist (x • z) (y • z) ≤ dist x y * dist z 0
⊢ IsBoundedSMul R (α × β)

Tactic:
refine ⟨fun x y z ↦ ?_, fun x y z ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x : R
y z : α × β
⊢ dist (x • y) (x • z) ≤ dist x 0 * dist y z

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

Premises used: WithLp.toLp, WithLp.dist_pseudoMetricSpaceToProd, dist_smul_pair
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsBoundedSMul R α
inst_6 : IsBoundedSMul R β
this : PseudoMetricSpace (α × β) := pseudoMetricSpaceToProd p α β
x y : R
z : α × β
⊢ dist (x • z) (y • z) ≤ dist x y * dist z 0

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

Premises used: dist_pair_smul, WithLp.toLp, WithLp.dist_pseudoMetricSpaceToProd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : NormSMulClass R α
inst_6 : NormSMulClass R β
this : SeminormedAddCommGroup (α × β) := seminormedAddCommGroupToProd p α β
⊢ NormSMulClass R (α × β)

Tactic:
⟨fun x y ↦ norm_smul x (toLp p y)⟩

Premises used: NormSMulClass.mk, norm_smul, WithLp.toLp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
hp : Fact (1 ≤ p)
α : Type u_4
β : Type u_5
inst : SeminormedAddCommGroup α
inst_1 : SeminormedAddCommGroup β
R : Type u_6
inst_2 : SeminormedRing R
inst_3 : Module R α
inst_4 : Module R β
inst_5 : NormSMulClass R α
inst_6 : NormSMulClass R β
this : SeminormedAddCommGroup (α × β) := seminormedAddCommGroupToProd p α β
⊢ NormSMulClass R (α × β)

Tactic:
exact ⟨fun x y ↦ norm_smul x (toLp p y)⟩
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup α
inst_3 : SeminormedAddCommGroup β
R : Type u_6
inst_4 : NormedField R
inst_5 : NormedSpace R α
inst_6 : NormedSpace R β
this : SeminormedAddCommGroup (α × β) := seminormedAddCommGroupToProd p α β
⊢ NormedSpace R (α × β)

Tactic:
exact ⟨fun x y ↦ norm_smul_le x (toLp p y)⟩
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
h : dist x y = 0
⊢ dist (toLp p x) (toLp p y) = 0

Tactic:
rw [dist_pseudoMetricSpaceToProd] at h

Premises used: WithLp.dist_pseudoMetricSpaceToProd
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
h : dist (toLp p x) (toLp p y) = 0
⊢ x = y

Tactic:
toLp_injective p (eq_of_dist_eq_zero h)

Premises used: eq_of_dist_eq_zero, WithLp.toLp_injective
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
h : dist (toLp p x) (toLp p y) = 0
⊢ x = y

Tactic:
exact toLp_injective p (eq_of_dist_eq_zero h)

Premises used: eq_of_dist_eq_zero, WithLp.toLp_injective
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
𝕜 : Type u_1
α_1 : Type u_2
β_1 : Type u_3
hp : Fact (1 ≤ p)
inst : SeminormedAddCommGroup α_1
inst_1 : SeminormedAddCommGroup β_1
α : Type u_4
β : Type u_5
inst_2 : NormedAddCommGroup α
inst_3 : NormedAddCommGroup β
x y : α × β
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_pseudoMetricSpaceToProd, SeminormedAddCommGroup.dist_eq, toLp_add, toLp_neg]

Premises used: SeminormedAddCommGroup.dist_eq, WithLp.toLp_neg, WithLp.dist_pseudoMetricSpaceToProd, WithLp.toLp_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 : WithLp p (α × β)
_ : ∀ (x2 : WithLp p (α × β)), edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
⊢ ∀ (x2 : WithLp p (α × β)), edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2

Tactic:
_
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 x2 : WithLp p (α × β)
inl :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 0)] (x1 x2 : WithLp 0 (α × β)),
    edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2
inr :
  ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (x1 x2 : WithLp ∞ (α × β)),
    edist (WithLp.map ∞ (Prod.map f g) x1) (WithLp.map ∞ (Prod.map f g) x2) = edist x1 x2
inr₁ : ∀ (hp_1 : 0 < p.toReal), edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2
⊢ edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2

Tactic:
rcases p.trichotomy with rfl | rfl | hp

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x1 x2 : WithLp 0 (α × β)
⊢ ¬?_mvar.418756

Tactic:
hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x1 x2 : WithLp 0 (α × β)
inl : ¬LE.le (α := ℝ≥0∞) 1 0
⊢ edist (WithLp.map 0 (Prod.map f g) x1) (WithLp.map 0 (Prod.map f g) x2) = edist x1 x2

Tactic:
absurd hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (LE.le (α := ℝ≥0∞) 1 0)
x1 x2 : WithLp 0 (α × β)
⊢ ¬LE.le (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
x1 x2 : WithLp ∞ (α × β)
⊢ edist (WithLp.map ∞ (Prod.map f g) x1) (WithLp.map ∞ (Prod.map f g) x2) = edist x1 x2

Tactic:
simp [WithLp.prod_edist_eq_sup, hf.edist_eq, hg.edist_eq]

Premises used: Isometry.edist_eq, WithLp.prod_edist_eq_sup
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
α' : Type u_5
β' : Type u_6
hp_1 : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace α'
inst_3 : PseudoEMetricSpace β'
f : α → α'
hf : Isometry f
g : β → β'
hg : Isometry g
x1 x2 : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist (WithLp.map p (Prod.map f g) x1) (WithLp.map p (Prod.map f g) x2) = edist x1 x2

Tactic:
simp [WithLp.prod_edist_eq_add hp, hf.edist_eq, hg.edist_eq]

Premises used: Isometry.edist_eq, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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
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
⊢ 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

Premises used: ENNReal.trichotomy, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 (α × β)
⊢ ¬?_mvar.427019

Tactic:
hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 (α × β)
inl : ¬LE.le (α := ℝ≥0∞) 1 0
⊢ edist (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x) (Equiv.toFun (WithLp.congr 0 (Equiv.prodComm α β)) x_1) =
    edist x x_1

Tactic:
absurd hp.elim

Premises used: Fact.elim
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 (α × β)
⊢ ¬LE.le (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 ∞)
__spread.0 : WithLp ∞ (α × β) ≃ WithLp ∞ (β × α) := WithLp.congr ∞ (Equiv.prodComm α β)
x x_1 : WithLp ∞ (α × β)
⊢ edist (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x) (Equiv.toFun (WithLp.congr ∞ (Equiv.prodComm α β)) x_1) =
    edist x x_1

Tactic:
simp [WithLp.prod_edist_eq_sup, max_comm]

Premises used: WithLp.prod_edist_eq_sup, max_comm
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
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 β'
x x_1 : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist ((WithLp.congr p (Equiv.prodComm α β)).toFun x) ((WithLp.congr p (Equiv.prodComm α β)).toFun x_1) = edist x x_1

Tactic:
simp [WithLp.prod_edist_eq_add hp, add_comm]

Premises used: add_comm, WithLp.prod_edist_eq_add
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : WithLp p (α × β)
⊢ (withLpProdComm p α β : (a : WithLp p (α × β)) → WithLp p (β × α)) x = WithLp.toLp p (x.snd, x.fst)

Tactic:
rfl

Premises used: WithLp.snd, WithLp.fst, Prod.swap, rfl
-- Module: Mathlib.Analysis.Normed.Lp.ProdLp
Goal:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := WithLp p (β × α) ≃ᵢ WithLp p (α × β)) (IsometryEquiv.symm (withLpProdComm p α β)) (withLpProdComm p β α)

Tactic:
rfl

Premises used: Equiv.trans, WithLp.congr, IsometryEquiv.symm, Prod.swap, IsometryEquiv.withLpProdComm, Equiv.symm, rfl