awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N O : Type u
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
inst_2 : SeminormedAddCommGroup O
f : NormedAddGroupHom M N
g : NormedAddGroupHom N O
hf : f.NormNoninc
hg : g.NormNoninc
hgf : (g.comp f).NormNoninc
⊢ mkHom (g.comp f) hgf = mkHom f hf ≫ mkHom g hg

Tactic:
rfl

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.comp, rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
rw : ((↑(Hom.hom (e.hom ≫ e.inv)) : NormedAddGroupHom M.carrier M.carrier) : (a : M.carrier) → M.carrier) r = r
⊢ ((↑(Hom.hom e.inv) : NormedAddGroupHom N.carrier M.carrier) : (a : N.carrier) → M.carrier)
      (((↑(Hom.hom e.hom) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier) r : N.carrier) =
    r

Tactic:
rw [← comp_apply]

Premises used: SemiNormedGrp₁.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ((↑(Hom.hom (e.hom ≫ e.inv)) : NormedAddGroupHom M.carrier M.carrier) : (a : M.carrier) → M.carrier) r = r

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
rw : ((↑(Hom.hom (e.inv ≫ e.hom)) : NormedAddGroupHom N.carrier N.carrier) : (a : N.carrier) → N.carrier) s = s
⊢ ((↑(Hom.hom e.hom) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier)
      (((↑(Hom.hom e.inv) : NormedAddGroupHom N.carrier M.carrier) : (a : N.carrier) → M.carrier) s : M.carrier) =
    s

Tactic:
rw [← comp_apply]

Premises used: SemiNormedGrp₁.comp_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ((↑(Hom.hom (e.inv ≫ e.hom)) : NormedAddGroupHom N.carrier N.carrier) : (a : N.carrier) → N.carrier) s = s

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : Type u
inst : SeminormedAddCommGroup V
⊢ { carrier := V, str := inst : SemiNormedGrp₁.{u} }.carrier = V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
⊢ Eq (α := (a : V.carrier) → V.carrier)
    (⇑(↑(Hom.hom (𝟙 V)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
M N K : SemiNormedGrp₁
f : M ⟶ N
g : N ⟶ K
⊢ Eq (α := (a : M.carrier) → K.carrier)
    (⇑(↑(Hom.hom (f ≫ g)) : NormedAddGroupHom M.carrier K.carrier) : (a : M.carrier) → K.carrier)
    (Function.comp (β := N.carrier)
      (⇑(↑(Hom.hom g) : NormedAddGroupHom N.carrier K.carrier) : (a : N.carrier) → K.carrier)
      (⇑(↑(Hom.hom f) : NormedAddGroupHom M.carrier N.carrier) : (a : M.carrier) → N.carrier))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
x : V.carrier
⊢ Eq (α := W.carrier)
    (((↑(Hom.hom 0) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) x : W.carrier)
    (0 : W.carrier)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
⊢ Limits.IsZero V

Tactic:
⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
refine_1 : ∀ (X : SemiNormedGrp₁.{u_1}) (f : V ⟶ X), f = default
refine_2 : ∀ (X : SemiNormedGrp₁.{u_1}) (f : X ⟶ V), f = default
⊢ Limits.IsZero V

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
refine_1 :
  ∀ (x : V.carrier),
    Eq (α := X.carrier)
      (((↑(Hom.hom f) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
      (((↑(Hom.hom default) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ x = 0

Tactic:
have : x = 0 := Subsingleton.elim _ _
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ Eq (α := X.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)
    (((↑(Hom.hom default) : NormedAddGroupHom V.carrier X.carrier) : (a : V.carrier) → X.carrier) x : X.carrier)

Tactic:
simp only [this, map_zero]

Premises used: map_zero
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
refine_2 :
  ∀ (x : X.carrier),
    Eq (α := V.carrier)
      (((↑(Hom.hom f) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)
      (((↑(Hom.hom default) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V : SemiNormedGrp₁
inst : Subsingleton.{u_1 + 1} V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x : X.carrier
⊢ Eq (α := V.carrier)
    (((↑(Hom.hom f) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)
    (((↑(Hom.hom default) : NormedAddGroupHom X.carrier V.carrier) : (a : X.carrier) → V.carrier) x : V.carrier)

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
⊢ Limits.HasZeroObject SemiNormedGrp₁

Tactic:
⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, PUnit, Exists.intro, SemiNormedGrp₁.isZero_of_subsingleton, SemiNormedGrp₁.of
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
change :
  Isometry (α := V.carrier) (β := W.carrier)
    (⇑{ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
          map_zero' := ⋯, map_add' := ⋯ } :
      (a : V.carrier) → W.carrier)
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier)

Tactic:
change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)

Premises used: AddMonoidHom.mk, map_zero, map_add, ZeroHom.mk, SemiNormedGrp₁.Hom.hom, Subtype.val, CategoryTheory.Iso.hom, DFunLike.coe, Isometry
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑{ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
          map_zero' := ⋯, map_add' := ⋯ } :
      (a : V.carrier) → W.carrier)

Tactic:
AddMonoidHomClass.isometry_of_norm _ ?_

Premises used: AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
refine :
  ∀ (x : V.carrier),
    norm (E := W.carrier)
        (({ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
                map_zero' := ⋯, map_add' := ⋯ : V.carrier →+ W.carrier } :
              (a : V.carrier) → W.carrier)
            x :
          W.carrier) =
      ‖x‖
⊢ Isometry (α := V.carrier) (β := W.carrier)
    (⇑{ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
          map_zero' := ⋯, map_add' := ⋯ } :
      (a : V.carrier) → W.carrier)

Tactic:
refine AddMonoidHomClass.isometry_of_norm _ ?_

Premises used: AddMonoidHomClass.isometry_of_norm
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
apply : ‖v‖ ≤ norm (E := W.carrier) ((i.hom.hom' : (a : V.carrier) → W.carrier) v : W.carrier)
⊢ norm (E := W.carrier)
      (({ toFun := (⇑(↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier),
              map_zero' := ⋯, map_add' := ⋯ : V.carrier →+ W.carrier } :
            (a : V.carrier) → W.carrier)
          v :
        W.carrier) =
    ‖v‖

Tactic:
apply le_antisymm (i.hom.2 v)

Premises used: SemiNormedGrp₁.Hom.normNoninc, le_antisymm, CategoryTheory.Iso.hom
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
rw :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom (i.hom ≫ i.inv)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v :
        V.carrier)
rw₁ :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom (𝟙 V)) : NormedAddGroupHom V.carrier V.carrier) : (a : V.carrier) → V.carrier) v : V.carrier)
rw₂ rw₃ : ‖v‖ = ‖v‖
⊢ ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier)

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

Premises used: SemiNormedGrp₁.comp_apply, CategoryTheory.Iso.hom_inv_id, SemiNormedGrp₁.id_apply
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
⊢ norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier) ≤
    norm (E := W.carrier)
      (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier)

Tactic:
i.inv.2 _

Premises used: SemiNormedGrp₁.Hom.normNoninc, CategoryTheory.Iso.inv
-- Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp
Goal:
V W : SemiNormedGrp₁
i : V ≅ W
v : V.carrier
by :
  ‖v‖ =
    norm (E := V.carrier)
      (((↑(Hom.hom i.inv) : NormedAddGroupHom W.carrier V.carrier) : (a : W.carrier) → V.carrier)
          (((↑(Hom.hom i.hom) : NormedAddGroupHom V.carrier W.carrier) : (a : V.carrier) → W.carrier) v : W.carrier) :
        V.carrier)
⊢ ‖v‖ ≤ norm (E := W.carrier) ((i.hom.hom' : (a : V.carrier) → W.carrier) v : W.carrier)

Tactic:
calc
    ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
    _ ≤ ‖i.hom v‖ := i.inv.2 _

Premises used: SemiNormedGrp₁.Hom.normNoninc, SemiNormedGrp₁.Hom.hom, Subtype.val, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : AddGroup E
inst_1 : FunLike F E ℝ
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x y : E
rw : LE.le (α := ℝ) ((f : (a : E) → ℝ) (x + -y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) (-y)) : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) (x - y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) y) : ℝ)

Tactic:
rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]

Premises used: sub_eq_add_neg, NonarchAddGroupSeminormClass.map_neg_eq_map'
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : AddGroup E
inst_1 : FunLike F E ℝ
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) (x + -y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) (-y)) : ℝ)

Tactic:
map_add_le_max _ _ _

Premises used: NonarchimedeanHomClass.map_add_le_max
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : AddGroup E
inst_1 : FunLike F E ℝ
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) (x + -y) : ℝ) (max ((f : (a : E) → ℝ) x) ((f : (a : E) → ℝ) (-y)) : ℝ)

Tactic:
exact map_add_le_max _ _ _

Premises used: NonarchimedeanHomClass.map_add_le_max
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x x_1 a : E
rw : LE.le (α := ℝ) ((f : (a : E) → ℝ) (a - a) : ℝ) ((f : (a : E) → ℝ) a : ℝ)
⊢ LE.le (α := ℝ) (0 : ℝ) ((f : (a : E) → ℝ) a : ℝ)

Tactic:
rw [← NonarchAddGroupSeminormClass.map_zero f, ← sub_self a]

Premises used: sub_self, NonarchAddGroupSeminormClass.map_zero
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x x_1 a : E
rw rw₁ : LE.le (α := ℝ) ((f : (a : E) → ℝ) a : ℝ) ((f : (a : E) → ℝ) a : ℝ)
⊢ LE.le (α := ℝ) (max ((f : (a : E) → ℝ) a) ((f : (a : E) → ℝ) a) : ℝ) ((f : (a : E) → ℝ) a : ℝ)

Tactic:
rw [max_self (f a)]

Premises used: max_self, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupSeminormClass F E
f : F
x x_1 a : E
⊢ LE.le (α := ℝ) ((f : (a : E) → ℝ) (a - a) : ℝ) ((f : (a : E) → ℝ) a : ℝ)

Tactic:
exact le_trans (map_sub_le_max _ _ _) (by rw [max_self (f a)])

Premises used: map_sub_le_max, le_trans
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : FunLike F E ℝ
inst_1 : AddGroup E
inst_2 : NonarchAddGroupNormClass F E
⊢ AddGroupNormClass F E ℝ

Tactic:
{ ‹NonarchAddGroupNormClass F E› with
    map_add_le_add := map_add_le_add
    map_neg_eq_map := NonarchAddGroupSeminormClass.map_neg_eq_map' }

Premises used: AddGroupNormClass.mk, NonarchAddGroupNormClass.eq_zero_of_map_eq_zero
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q f g : GroupSeminorm E
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : GroupSeminorm E) ↦ f.toFun) f)
    ((fun (f : GroupSeminorm E) ↦ f.toFun) g)
mk :
  ∀ (toFun : E → ℝ) (map_one' : toFun 1 = 0) (mul_le' : ∀ (x y : E), toFun (x * y) ≤ toFun x + toFun y)
    (inv' : ∀ (x : E), toFun x⁻¹ = toFun x)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : GroupSeminorm E) ↦ f.toFun)
          { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
        ((fun (f : GroupSeminorm E) ↦ f.toFun) g)),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q g : GroupSeminorm E
toFun : E → ℝ
map_one' : toFun 1 = 0
mul_le' : ∀ (x y : E), toFun (x * y) ≤ toFun x + toFun y
inv' : ∀ (x : E), toFun x⁻¹ = toFun x
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupSeminorm E) ↦ f.toFun) { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
    ((fun (f : GroupSeminorm E) ↦ f.toFun) g)
mk :
  ∀ (toFun_1 : E → ℝ) (map_one'_1 : toFun_1 1 = 0) (mul_le'_1 : ∀ (x y : E), toFun_1 (x * y) ≤ toFun_1 x + toFun_1 y)
    (inv'_1 : ∀ (x : E), toFun_1 x⁻¹ = toFun_1 x)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : GroupSeminorm E) ↦ f.toFun)
          { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
        ((fun (f : GroupSeminorm E) ↦ f.toFun)
          { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 })),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } =
      { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 }
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
toFun : E → ℝ
map_one' : toFun 1 = 0
mul_le' : ∀ (x y : E), toFun (x * y) ≤ toFun x + toFun y
inv' : ∀ (x : E), toFun x⁻¹ = toFun x
toFun_1 : E → ℝ
map_one'_1 : toFun_1 1 = 0
mul_le'_1 : ∀ (x y : E), toFun_1 (x * y) ≤ toFun_1 x + toFun_1 y
inv'_1 : ∀ (x : E), toFun_1 x⁻¹ = toFun_1 x
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupSeminorm E) ↦ f.toFun) { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' })
    ((fun (f : GroupSeminorm E) ↦ f.toFun)
      { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 })
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E } =
    { toFun := toFun_1, map_one' := map_one'_1, mul_le' := mul_le'_1, inv' := inv'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p : GroupSeminorm E
⊢ p.toFun = (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ (∀ (x : E), Eq (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)) → p = q

Tactic:
DFunLike.ext p q

Premises used: DFunLike.ext
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ p ≤ q ↔ LE.le (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ p < q ↔ LT.lt (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ LE.le (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ LT.lt (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ) ↔ p < q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
⊢ Eq.{u_3 + 1} (α := (a : E) → ℝ) (⇑0 : (a : E) → ℝ) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
x : E
⊢ Eq (α := ℝ) ((0 : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
simp_rw : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0
simp_rw₁ : HAdd.hAdd (α := ℝ) 0 0 = 0
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) = 0

Tactic:
simp_rw [map_one_eq_zero p, map_one_eq_zero q, zero_add]

Premises used: GroupSeminormClass.map_one_eq_zero, zero_add
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q_1 : GroupSeminorm E
f : F →* E
p q : GroupSeminorm E
x : E
simp_rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x⁻¹ : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x⁻¹ : ℝ) ((q : (a : E) → ℝ) x⁻¹ : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
simp_rw [map_inv_eq_map p, map_inv_eq_map q]

Premises used: GroupSeminormClass.map_inv_eq_map
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
⊢ (⇑(p + q) : (a : E) → ℝ) = HAdd.hAdd (α := (a : E) → ℝ) (⇑p : (a : E) → ℝ) (⇑q : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm E
x : E
⊢ (p + q : (a : E) → ℝ) x = HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
⊢ Eq (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
inl :
  ∀ (h : BddAbove.{u_3} (α := GroupSeminorm E) ∅),
    ⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
      HAdd.hAdd (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
inr :
  ∀ (hs : s.Nonempty),
    ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
      HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
        (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)

Tactic:
obtain (rfl | hs) := eq_empty_or_nonempty s

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
x y : E
h : BddAbove.{u_3} (α := GroupSeminorm E) ∅
⊢ ⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑∅ : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
have : Nonempty s := hs.to_subtype
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) (x * y) ≤
    HAdd.hAdd (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
      (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y)

Tactic:
ciSup_le fun p ↦ (map_mul_le_add p.1 x y).trans ?_

Premises used: MulLEAddHomClass.map_mul_le_add, LE.le.trans, Subtype.val, ciSup_le