gistfile1.txt

section Mathlib.Init.Algebra.Order

class Preorder (α : Type u) extends LE α, LT α where
class PartialOrder (α : Type u) extends Preorder α where
class LinearOrder (α : Type u) extends PartialOrder α, Min α, Max α, Ord α :=


end Mathlib.Init.Algebra.Order

section Std.Classes.Cast

class NatCast (R : Type u) where
class IntCast (R : Type u) where

end Std.Classes.Cast

section Std.Classes.RatCast

class RatCast (K : Type u) where

end Std.Classes.RatCast

section Mathlib.Init.Data.Nat.Order

instance Nat.linearOrder : LinearOrder Nat where
  le := Nat.le
  lt := Nat.lt

end Mathlib.Init.Data.Nat.Order

section Mathlib.Init.ZeroOne

class Zero.{u} (α : Type u) where
  zero : α
instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1
class One (α : Type u) where
  one : α
instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := ‹One α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

class Inv (α : Type u) where
class Semigroup (G : Type u) extends Mul G where
class AddSemigroup (G : Type u) extends Add G where
class CommSemigroup (G : Type u) extends Semigroup G where
class AddCommSemigroup (G : Type u) extends AddSemigroup G where
class MulOneClass (M : Type u) extends One M, Mul M where
class AddZeroClass (M : Type u) extends Zero M, Add M where
  add_zero : ∀ a : M, a + 0 = a
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
class Group (G : Type u) extends DivInvMonoid G where
class AddGroup (A : Type u) extends SubNegMonoid A where
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ
class SMul (M : Type _) (α : Type _) where
  smul : M → α → α

infixr:73 " • " => HSMul.hSMul

instance instHSMul [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

end Mathlib.Algebra.Group.Defs

section Mathlib.Logic.Nontrivial

class Nontrivial (α : Type _) : Prop where

end Mathlib.Logic.Nontrivial

section Mathlib.Algebra.GroupWithZero.Defs

class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
  extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
class NoZeroDivisors (M₀ : Type _) [Mul M₀] [Zero M₀] : Prop where
class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀
class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀
class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀
class CommMonoidWithZero (M₀ : Type _) extends CommMonoid M₀, MonoidWithZero M₀
class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀

end Mathlib.Algebra.GroupWithZero.Defs

section Mathlib.Data.Nat.Cast.Defs

class AddMonoidWithOne (R : Type u) extends NatCast R, AddMonoid R, One R where
class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

end Mathlib.Data.Nat.Cast.Defs

section Mathlib.Data.Int.Cast.Defs

class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R where

end Mathlib.Data.Int.Cast.Defs

section Mathlib.Algebra.Ring.Defs

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, MulZeroClass α
class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α
class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α
class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R
class CommSemiring (R : Type u) extends Semiring R, CommMonoid R
class CommRing (α : Type u) extends Ring α, CommMonoid α
instance CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
  { s with }
class IsDomain (α : Type u) [Semiring α] extends IsCancelMulZero α, Nontrivial α : Prop

end Mathlib.Algebra.Ring.Defs

section Mathlib.Algebra.Ring.Regular

section IsDomain

instance IsDomain.toCancelCommMonoidWithZero [CommSemiring α] [IsDomain α] :
    CancelCommMonoidWithZero α := { }

end IsDomain

end Mathlib.Algebra.Ring.Regular

section Mathlib.Algebra.Field.Defs

class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, RatCast K where
class Field (K : Type u) extends CommRing K, DivisionRing K

end Mathlib.Algebra.Field.Defs

section Mathlib.Order.Basic

variable [Preorder α] {a b c : α}

theorem le_of_le_of_eq (hab : a ≤ b) (hbc : b = c) : a ≤ c :=
  hbc ▸ hab

end Mathlib.Order.Basic

section Mathlib.Data.FunLike.Basic

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

variable {F α : Sort _} {β : α → Sort _} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

end Mathlib.Data.FunLike.Basic

section Mathlib.Algebra.Hom.Group

section Zero

structure ZeroHom (M : Type _) (N : Type _) [Zero M] [Zero N] where
  toFun : M → N

class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
  extends FunLike F M fun _ => N where

end Zero

section Add

structure AddHom (M : Type _) (N : Type _) [Add M] [Add N] where
  toFun : M → N

class AddHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Add N]
  extends FunLike F M fun _ => N where

end Add

section add_zero

structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass N] extends
  ZeroHom M N, AddHom M N

infixr:25 " →+ " => AddMonoidHom

class AddMonoidHomClass (F : Type _) (M N : outParam (Type _)) [AddZeroClass M] [AddZeroClass N]
  extends AddHomClass F M N, ZeroHomClass F M N

end add_zero

section One

variable [One M] [One N]

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  toFun : M → N

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where

end One

section Mul

variable [Mul M] [Mul N]

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where

end Mul

section Add

variable [Add M] [Add N]

instance AddHom.addHomClass : AddHomClass (AddHom M N) M N where
  coe := AddHom.toFun

def AddHomClass.toAddHom [AddHomClass F M N] (f : F) : AddHom M N where
  toFun := f

instance [AddHomClass F M N] : CoeTC F (AddHom M N) :=
  ⟨AddHomClass.toAddHom⟩

end Add

section mul_one

variable [MulOneClass M] [MulOneClass N]

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N

end mul_one

section MulZeroOne

variable [MulZeroOneClass M] [MulZeroOneClass N]

structure MonoidWithZeroHom (M : Type _) (N : Type _)
  [MulZeroOneClass M] [MulZeroOneClass N] extends ZeroHom M N, MonoidHom M N

infixr:25 " →*₀ " => MonoidWithZeroHom

class MonoidWithZeroHomClass (F : Type _) (M N : outParam (Type _)) [MulZeroOneClass M]
  [MulZeroOneClass N] extends MonoidHomClass F M N, ZeroHomClass F M N

end MulZeroOne

instance [Add M] [AddCommSemigroup N] : Add (AddHom M N) :=
  ⟨fun f g =>
    { toFun := fun m => f m + g m, }⟩

end Mathlib.Algebra.Hom.Group

section Mathlib.Algebra.Hom.Ring

structure NonUnitalRingHom (α β : Type _) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β

infixr:25 " →ₙ+* " => NonUnitalRingHom

structure RingHom (α : Type _) (β : Type _) [NonAssocSemiring α] [NonAssocSemiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

infixr:25 " →+* " => RingHom

section RingHomClass

class RingHomClass (F : Type _) (α β : outParam (Type _)) [NonAssocSemiring α]
  [NonAssocSemiring β] extends MonoidHomClass F α β, AddMonoidHomClass F α β,
  MonoidWithZeroHomClass F α β

end RingHomClass

namespace RingHom

instance {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} : RingHomClass (α →+* β) α β where
  coe f := sorry

/-- The identity ring homomorphism from a semiring to itself. -/
def id (α : Type _) [NonAssocSemiring α] : α →+* α := sorry

end RingHom

end Mathlib.Algebra.Hom.Ring

section Mathlib.Algebra.Order.Hom.Basic

class SubadditiveHomClass (F : Type _) (α β : outParam (Type _)) [Add α] [Add β] [LE β] extends
  FunLike F α fun _ => β where

end Mathlib.Algebra.Order.Hom.Basic

section Mathlib.Algebra.Order.Monoid.Defs

class OrderedAddCommMonoid (α : Type _) extends AddCommMonoid α, PartialOrder α where
class LinearOrderedAddCommMonoid (α : Type _) extends LinearOrder α, OrderedAddCommMonoid α

end Mathlib.Algebra.Order.Monoid.Defs

section Mathlib.Algebra.Order.Monoid.Cancel.Defs

class OrderedCancelAddCommMonoid (α : Type u) extends AddCommMonoid α, PartialOrder α where

end Mathlib.Algebra.Order.Monoid.Cancel.Defs

section Mathlib.Algebra.Order.Ring.Defs

/-- A `StrictOrderedSemiring` is a nontrivial semiring with a partial order such that addition is
strictly monotone and multiplication by a positive number is strictly monotone. -/
class StrictOrderedSemiring (α : Type u) extends Semiring α, OrderedCancelAddCommMonoid α,
    Nontrivial α where

class StrictOrderedCommSemiring (α : Type u) extends StrictOrderedSemiring α, CommSemiring α

class LinearOrderedSemiring (α : Type u) extends StrictOrderedSemiring α,
  LinearOrderedAddCommMonoid α

class LinearOrderedCommSemiring (α : Type _) extends StrictOrderedCommSemiring α,
  LinearOrderedSemiring α

end Mathlib.Algebra.Order.Ring.Defs

section Mathlib.GroupTheory.GroupAction.Defs

class MulAction (α : Type _) (β : Type _) [Monoid α] extends SMul α β where
class DistribMulAction (M A : Type _) [Monoid M] [AddMonoid A] extends MulAction M A where

end Mathlib.GroupTheory.GroupAction.Defs

section Mathlib.Data.Nat.Basic

namespace Nat

instance commSemiring : CommSemiring Nat where
  add := Nat.add
  zero := Nat.zero
  add_zero := sorry
  mul := Nat.mul
  one := Nat.succ Nat.zero

end Nat

end Mathlib.Data.Nat.Basic

section Mathlib.Data.Nat.Order.Basic

namespace Nat

instance linearOrderedCommSemiring : LinearOrderedCommSemiring Nat :=
  { Nat.commSemiring, Nat.linearOrder with
    lt := Nat.lt, }

end Nat

end Mathlib.Data.Nat.Order.Basic

section Mathlib.Algebra.Module.Basic

class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends
  DistribMulAction R M where

end Mathlib.Algebra.Module.Basic

section Mathlib.Algebra.Module.LinearMap

structure LinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type _)
    (M₂ : Type _) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends
    AddHom M M₂ where
  map_smul' : ∀ (r : R) (x : M), toFun (r • x) = σ r • toFun x

notation:25 M " →ₛₗ[" σ:25 "] " M₂:0 => LinearMap σ M M₂

notation:25 M " →ₗ[" R:25 "] " M₂:0 => LinearMap (RingHom.id R) M M₂

class SemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S]
  (σ : outParam (R →+* S)) (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂]
  [Module R M] [Module S M₂] extends AddHomClass F M M₂ where
  map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x

variable [Semiring R] [Semiring S]

section

variable [AddCommMonoid M] [AddCommMonoid M₃]
variable [Module R M] [Module S M₃]
variable {σ : R →+* S}

instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ where
  coe f := f.toFun
  map_smulₛₗ := LinearMap.map_smul'

end

end Mathlib.Algebra.Module.LinearMap

section Mathlib.Topology.Basic

class TopologicalSpace (α : Type u) where

end Mathlib.Topology.Basic

section Mathlib.Topology.ContinuousFunction.Basic

structure ContinuousMap (α β : Type _) [TopologicalSpace α] [TopologicalSpace β] where
  toFun : α → β

class ContinuousMapClass (F : Type _) (α β : outParam <| Type _) [TopologicalSpace α]
  [TopologicalSpace β] extends FunLike F α fun _ => β where

end Mathlib.Topology.ContinuousFunction.Basic

section Mathlib.Topology.Algebra.Monoid

variable [TopologicalSpace X]

class ContinuousAdd (M : Type u) [TopologicalSpace M] [Add M] : Prop where

end Mathlib.Topology.Algebra.Monoid

section Mathlib.Topology.Algebra.Group.Basic

class ContinuousNeg (G : Type u) [TopologicalSpace G] [Neg G] : Prop where

class TopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] extends
  ContinuousAdd G, ContinuousNeg G : Prop

end Mathlib.Topology.Algebra.Group.Basic

section Mathlib.Topology.UniformSpace.Basic

structure UniformSpace.Core (α : Type u) where

class UniformSpace (α : Type u) extends TopologicalSpace α, UniformSpace.Core α where

def UniformSpace.ofFun {α : Type u} {β : Type v} [OrderedAddCommMonoid β] (d : α → α → β) :
    UniformSpace α :=
sorry

end Mathlib.Topology.UniformSpace.Basic

section Mathlib.Topology.Algebra.UniformGroup

class UniformAddGroup (α : Type _) [UniformSpace α] [AddGroup α] : Prop where

end Mathlib.Topology.Algebra.UniformGroup

section Mathlib.Topology.Algebra.Module.Basic

structure ContinuousLinearMap {R : Type _} {S : Type _} [Semiring R] [Semiring S] (σ : R →+* S)
    (M : Type _) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type _) [TopologicalSpace M₂]
    [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂ where

@[inherit_doc]
notation:25 M " →SL[" σ "] " M₂ => ContinuousLinearMap σ M M₂

@[inherit_doc]
notation:25 M " →L[" R "] " M₂ => ContinuousLinearMap (RingHom.id R) M M₂

class ContinuousSemilinearMapClass (F : Type _) {R S : outParam (Type _)} [Semiring R] [Semiring S]
    (σ : outParam <| R →+* S) (M : outParam (Type _)) [TopologicalSpace M] [AddCommMonoid M]
    (M₂ : outParam (Type _)) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
    [Module S M₂] extends SemilinearMapClass F σ M M₂, ContinuousMapClass F M M₂
abbrev ContinuousLinearMapClass (F : Type _) (R : outParam (Type _)) [Semiring R]
    (M : outParam (Type _)) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam (Type _))
    [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] :=
  ContinuousSemilinearMapClass F (RingHom.id R) M M₂

namespace ContinuousLinearMap

section Semiring

variable {R₁ : Type _} {R₂ : Type _} [Semiring R₁] [Semiring R₂]
  {σ₁₂ : R₁ →+* R₂} {M₁ : Type _} [TopologicalSpace M₁]
  [AddCommMonoid M₁] {M₂ : Type _}
  [TopologicalSpace M₂] [AddCommMonoid M₂]
  [Module R₁ M₁]
  [Module R₂ M₂]

instance LinearMap.coe : Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) := ⟨toLinearMap⟩

instance continuousSemilinearMapClass :
    ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂ where
  coe f := f.toLinearMap
  map_smulₛₗ f := sorry

section Add

variable [ContinuousAdd M₂]

instance add : Add (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun f g => ⟨f + g, sorry⟩⟩

instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) where
  zero := sorry
  add := (· + ·)
  add_zero := sorry

end Add

end Semiring

section Ring

variable {R : Type _} [Ring R] {R₂ : Type _} [Ring R₂] {M : Type _}
  [TopologicalSpace M] [AddCommGroup M] {M₂ : Type _} [TopologicalSpace M₂] [AddCommGroup M₂]
  [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂}

variable [TopologicalAddGroup M₂]

instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) :=
  { ContinuousLinearMap.addCommMonoid with
    zero := sorry
    add := (· + ·)
    neg := sorry
    sub := sorry }

end Ring

end ContinuousLinearMap

end Mathlib.Topology.Algebra.Module.Basic

section Mathlib.Topology.MetricSpace.Basic

def UniformSpace.ofDist (dist : α → α → Nat) : UniformSpace α :=
  .ofFun dist

class Dist (α : Type _) where
  dist : α → α → Nat

class PseudoMetricSpace (α : Type u) extends Dist α : Type u where
  toUniformSpace : UniformSpace α := .ofDist dist

attribute [instance] PseudoMetricSpace.toUniformSpace

class MetricSpace (α : Type u) extends PseudoMetricSpace α : Type u where

end Mathlib.Topology.MetricSpace.Basic

section Mathlib.Analysis.Normed.Group.Seminorm

structure AddGroupSeminorm (G : Type _) [AddGroup G] where
  protected toFun : G → Nat
  protected add_le' : ∀ r s, toFun (r + s) ≤ toFun r + toFun s

class AddGroupSeminormClass (F : Type _) (α β : outParam <| Type _) [AddGroup α]
  [OrderedAddCommMonoid β] extends SubadditiveHomClass F α β where

instance addGroupSeminormClass [AddGroup E] : AddGroupSeminormClass (AddGroupSeminorm E) E Nat
    where
  coe f := f.toFun

instance [AddGroup E] : CoeFun (AddGroupSeminorm E) fun _ => E → Nat :=
  ⟨FunLike.coe⟩

end Mathlib.Analysis.Normed.Group.Seminorm

section Mathlib.Analysis.Normed.Group.Basic

class Norm (E : Type _) where
  norm : E → Nat

export Norm (norm)

notation "‖" e "‖" => norm e

class SeminormedAddGroup (E : Type _) extends Norm E, AddGroup E, PseudoMetricSpace E where
  dist := fun x y => ‖x - y‖
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by intros; rfl

class SeminormedAddCommGroup (E : Type _) extends Norm E, AddCommGroup E,
  PseudoMetricSpace E where
  dist := fun x y => ‖x - y‖
  dist_eq : ∀ x y, dist x y = ‖x - y‖ := by intros; rfl

instance (priority := 100) SeminormedAddCommGroup.toSeminormedAddGroup [SeminormedAddCommGroup E] :
    SeminormedAddGroup E :=
  { ‹SeminormedAddCommGroup E› with }

def AddGroupSeminorm.toSeminormedAddGroup [AddGroup E] (f : AddGroupSeminorm E) :
    SeminormedAddGroup E where
  dist x y := f (x - y)
  norm := f
  dist_eq _ _ := rfl

def AddGroupSeminorm.toSeminormedAddCommGroup [AddCommGroup E] (f : AddGroupSeminorm E) :
    SeminormedAddCommGroup E :=
  sorry -- With this sorry, we time out without #2210, or fail to typecheck on the final line with #2210.
-- With this definition, the file works fine with or without #2210.
-- { AddGroupSeminorm.toSeminormedAddGroup f with }

section SeminormedGroup

variable [SeminormedAddGroup E] {s : Set E}
  {a a₁ a₂ b b₁ b₂ : E} {r r₁ r₂ : Nat}

theorem norm_add_le_of_le (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ + a₂‖ ≤ r₁ + r₂ :=
  sorry

end SeminormedGroup

end Mathlib.Analysis.Normed.Group.Basic

section Mathlib.Analysis.Normed.Field.Basic

class NormedField (α : Type _) extends Norm α, Field α, MetricSpace α where

class NontriviallyNormedField (α : Type _) extends NormedField α where

section RingHomIsometric

class RingHomIsometric [Semiring R₁] [Semiring R₂] [Norm R₁] [Norm R₂] (σ : R₁ →+* R₂) : Prop where

end RingHomIsometric

end Mathlib.Analysis.Normed.Field.Basic

section Mathlib.Analysis.NormedSpace.Basic

class NormedSpace (α : Type _) (β : Type _) [NormedField α] [SeminormedAddCommGroup β] extends
  Module α β where

end Mathlib.Analysis.NormedSpace.Basic

noncomputable section

section SemiNormed

variable [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]

variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂]
  [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F]
  {σ₁₂ : 𝕜 →+* 𝕜₂}

namespace ContinuousLinearMap

theorem bound [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) : ∃ C, 0 < C ∧ ∀ x : E, ‖f x‖ ≤ C * ‖x‖ :=
  sorry

section OpNorm

def opNorm (_f : E →SL[σ₁₂] F) := 0

instance hasOpNorm : Norm (E →SL[σ₁₂] F) :=
  ⟨opNorm⟩

theorem op_norm_le_bound (f : E →SL[σ₁₂] F) {M : Nat} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) :
    ‖f‖ ≤ M :=
  sorry

section

variable [RingHomIsometric σ₁₂] (f g : E →SL[σ₁₂] F) (x : E)

theorem le_op_norm : ‖f x‖ ≤ ‖f‖ * ‖x‖ := by
  have := f.bound
  exact sorry

theorem op_norm_add_le : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=
  (f + g).op_norm_le_bound sorry fun x =>
    le_of_le_of_eq (norm_add_le_of_le (f.le_op_norm x) (g.le_op_norm x)) sorry

protected def tmpSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) :=
  AddGroupSeminorm.toSeminormedAddCommGroup
    { toFun := norm
      add_le' := op_norm_add_le }

instance toSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) where
  dist_eq L M := ContinuousLinearMap.tmpSeminormedAddCommGroup.dist_eq L M