awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
⊢ (∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) ↔
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
have mp : (∃ (p : Seminorm 𝕜 E),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
      ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) →
  ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
mp :
  (∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) →
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ (∃ (p : Seminorm 𝕜 E),
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
        ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p) ↔
    ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
have mpr : (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) →
  ∃ (p : Seminorm 𝕜 E),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
      ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
p : Seminorm 𝕜 E
hp : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
hpf : ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
⊢ ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
have mp : ∀ (C : ℝ) (hC : ∀ (x : E), (p : (a : E) → ℝ) x ≤ C * ‖x‖),
  ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (goal)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
⊢ ∃ (p : Seminorm 𝕜 E),
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑p : (a : E) → ℝ) ∧
      ∀ (k : ι), Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f k) : E →ₛₗ[σ₁₂] F) ≤ p
have mpr : ∀ (i : ι) (x : E),
  LE.le (α := (fun (a : E) ↦ ℝ) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (Seminorm.comp (normSeminorm 𝕜₂ F) (↑(f i) : E →ₛₗ[σ₁₂] F)) x)
    ((fun (f : Seminorm 𝕜 E) ↦ ((⇑f : (a : E) → ℝ) : (a : E) → ℝ))
      (HSMul.hSMul (β := Seminorm 𝕜 E) C.toNNReal (normSeminorm 𝕜 E)) x)
Tactic: refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.NormedSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
ι : Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : SeminormedAddCommGroup E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 :
  ∀ (a : EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0),
    UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_3_to_2 :
  ∀ (a : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)
tfae_2_to_1 :
  ∀ (a : Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f)),
    EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0
tfae_4_iff_5 :
  (∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
tfae_5_iff_7 :
  (∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖) ↔
    ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_6_iff_8 : (∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖)
tfae_8_iff_9 :
  BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖) ↔ LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤
⊢ [EquicontinuousAt.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) 0,
      Equicontinuous.{u_8, u_4, u_5} (X := E) (α := F) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f),
      ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ C ≥ 0, ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖,
      ∃ (C : ℝ), ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (α := ℝ) (Set.range fun (x : ι) ↦ ‖f x‖),
      LT.lt (α := ENNReal) (⨆ (i : ι), (↑‖f i‖₊ : ENNReal)) ⊤].TFAE
have tfae_3_iff_4 : UniformEquicontinuous.{u_8, u_5, u_4} (α := F) (β := E) (DFunLike.coe (β := fun (x : E) ↦ F) ∘ f) ↔
  ∃ (C : ℝ), ∀ (i : ι) (x : E), norm.{u_5} (E := F) ((f i : (a : E) → F) x : F) ≤ C * ‖x‖
Tactic: tfae_have 3 ↔ 4 := by
    refine ((norm_withSeminorms 𝕜₂ F).uniformEquicontinuous_iff_exists_continuous_seminorm _).trans
      ?_
    rw [forall_const]
    constructor
    · intro ⟨p, hp, hpf⟩
      rcases p.bound_of_continuous_normedSpace hp with ⟨C, -, hC⟩
      exact ⟨C, fun i x ↦ (hpf i x).trans (hC x)⟩
    · intro ⟨C, hC⟩
      refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩
      exact (hC i x).trans (mul_le_mul_of_nonneg_right (C.le_coe_toNNReal) (norm_nonneg x))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace 𝕜 G
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
M₄ : Type u_8
inst_7 : SeminormedAddCommGroup M₁
inst_8 : NormedSpace 𝕜 M₁
inst_9 : SeminormedAddCommGroup M₂
inst_10 : NormedSpace 𝕜 M₂
inst_11 : SeminormedAddCommGroup M₃
inst_12 : NormedSpace 𝕜 M₃
inst_13 : SeminormedAddCommGroup M₄
inst_14 : NormedSpace 𝕜 M₄
⊢ Eq (α := (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) → M₁ × M₃ →L[𝕜] M₂ × M₄)
    (fun (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) ↦ p.1.prodMap p.2)
    (⇑(have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
        have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
        have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (fst 𝕜 M₁ M₃);
        have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (snd 𝕜 M₁ M₃);
        have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂) :
      (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
have h : ∀ (x : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)),
  x.1.prodMap x.2 =
    (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₁ M₂ (M₂ × M₄) : (a : M₂ →L[𝕜] M₂ × M₄) → (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄) (inl 𝕜 M₂ M₄);
        have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄ :=
          (compL 𝕜 M₃ M₄ (M₂ × M₄) : (a : M₄ →L[𝕜] M₂ × M₄) → (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄) (inr 𝕜 M₂ M₄);
        have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₁) → (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (fst 𝕜 M₁ M₃);
        have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄ :=
          (flip (compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)) :
              (a : M₁ × M₃ →L[𝕜] M₃) → (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄)
            (snd 𝕜 M₁ M₃);
        have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂ := fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄ := snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄);
        Φ₁' ∘SL Φ₁ ∘SL Ψ₁ + Φ₂' ∘SL Φ₂ ∘SL Ψ₂ :
        (a : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)) → M₁ × M₃ →L[𝕜] M₂ × M₄)
      x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
⊢ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) = 1
have refine : 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
Tactic: refine le_antisymm (norm_fst_le ..) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
have let : ∀ (e : E) (he : e ≠ 0), 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
Tactic: let ⟨e, he⟩ := exists_ne (0 : E)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
have this : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * max ‖e‖ (Norm.norm.{u_3} (E := F) 0)
Tactic: have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * max ‖e‖ (Norm.norm.{u_3} (E := F) 0)
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
have this₁ : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * ‖e‖
Tactic: rw [norm_zero, max_eq_left (norm_nonneg e)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial E
e : E
he : e ≠ 0
this : ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E) * ‖e‖
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F)
have rwa : 1 * ‖e‖ ≤ Norm.norm (E := E × F →L[𝕜] E) (fst 𝕜 E F) * ‖e‖
Tactic: rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
⊢ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) = 1
have refine : 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
Tactic: refine le_antisymm (norm_snd_le ..) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
have let : ∀ (f : F) (hf : f ≠ 0), 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
Tactic: let ⟨f, hf⟩ := exists_ne (0 : F)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
have this : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * max (Norm.norm.{u_2} (E := E) 0) ‖f‖
Tactic: have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * max (Norm.norm.{u_2} (E := E) 0) ‖f‖
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
have this₁ : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * ‖f‖
Tactic: rw [norm_zero, max_eq_right (norm_nonneg f)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Operator.Prod (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : Nontrivial F
f : F
hf : f ≠ 0
this : ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F) * ‖f‖
⊢ 1 ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F)
have rwa : 1 * ‖f‖ ≤ Norm.norm (E := E × F →L[𝕜] F) (snd 𝕜 E F) * ‖f‖
Tactic: rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Basic (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α ℝ
inst_1 : Group α
inst_2 : GroupSeminormClass F α ℝ
f : F
x y z : α
⊢ (f : (a : α) → ℝ) (x⁻¹ * z) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : α) → ℝ) (x⁻¹ * y) : ℝ) ((f : (a : α) → ℝ) (y⁻¹ * z) : ℝ)
have h : x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
Tactic: convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
⊢ dist x z ≤ max (dist x y) (dist y z)
have simp : LE.le (α := ℝ) ((f : (a : α) → ℝ) (-x + z) : ℝ) (max ((f : (a : α) → ℝ) (-x + y)) ((f : (a : α) → ℝ) (-y + z)) : ℝ)
Tactic: simp +instances only [hd, dist_eq_norm_neg_add,
      AddGroupSeminormClass.toSeminormedAddGroup_norm_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
⊢ LE.le (α := ℝ) ((f : (a : α) → ℝ) (-x + z) : ℝ) (max ((f : (a : α) → ℝ) (-x + y)) ((f : (a : α) → ℝ) (-y + z)) : ℝ)
have h : -x + z = -x + y + (-y + z)
Tactic: convert! hna (-x + y) (-y + z) using 2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
⊢ -x + z = -x + y + (-y + z)
have h : -x + z = -x + (y + (-y + z))
Tactic: rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
h : -x + z = -x + (y + (-y + z))
⊢ -x + z = -x + y + (-y + z)
have h₁ : -x + z = -x + (y + -y + z)
Tactic: rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Order.Hom.Ultra (goal)
Goal:
F : Type u_1
α : Type u_2
inst_1 : FunLike F α ℝ
inst_2 : AddGroup α
inst_3 : AddGroupSeminormClass F α ℝ
inst : Dist α
f : F
hna : IsNonarchimedean.{0, u_2} (R := ℝ) (α := α) (⇑f : (a : α) → ℝ)
hd : inst = PseudoMetricSpace.toDist
x y z : α
h : -x + z = -x + (y + (-y + z))
h₁ : -x + z = -x + (y + -y + z)
⊢ -x + z = -x + y + (-y + z)
have h₂ : -x + z = -x + (0 + z)
Tactic: rw [add_assoc, ← add_assoc y, add_neg_cancel, zero_add]