awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : ¬x + y = 0
h_1 : y = 0
⊢ LE.le (α := ℝ) 1 (max 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : DecidableEq E
x y : E
hx : ¬x = 0
h : ¬x + y = 0
h_1 : ¬y = 0
⊢ LE.le (α := ℝ) 1 (max 1 1)

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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) 0 : ℝ) = 0

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, map_zero p,
          mul_zero]

Premises used: map_zero, NNReal, MulZeroClass.mul_zero, NNReal.smul_def, smul_one_smul, smul_eq_mul
-- 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
simp :
  HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
    HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
    max (HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)) (HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) y : ℝ))

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ←
          mul_max_of_nonneg _ _ NNReal.zero_le_coe]

Premises used: NNReal, mul_max_of_nonneg, NNReal.smul_def, smul_one_smul, smul_eq_mul, NNReal.zero_le_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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
hbc : LE.le (α := ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)
⊢ HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) ≤
    HMul.hMul (β := ℝ) (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)

Tactic:
gcongr
-- 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ LE.le (α := ℝ) ((p : (a : E) → ℝ) (x + y) : ℝ) (max ((p : (a : E) → ℝ) x) ((p : (a : E) → ℝ) y) : ℝ)

Tactic:
apply 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) (-x) : ℝ) = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
simp_rw [map_neg_eq_map p]

Premises used: AddGroupSeminormClass.map_neg_eq_map
-- 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 : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
inst_4 : SMul R' ℝ
inst_5 : SMul R' ℝ≥0
inst_6 : IsScalarTower R' ℝ≥0 ℝ
inst_7 : SMul R R'
inst_8 : IsScalarTower R R' ℝ
⊢ IsScalarTower.{u_1, u_2, u_3} R R' (NonarchAddGroupSeminorm E)

Tactic:
⟨fun r a p => ext fun x => smul_assoc r a <| p x⟩

Premises used: smul_assoc, IsScalarTower.mk, NonarchAddGroupSeminorm.ext, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
⊢ (⇑(r • p) : (a : E) → ℝ) = HSMul.hSMul (β := (a : E) → ℝ) r (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x : E
⊢ (r • p : (a : E) → ℝ) x = HSMul.hSMul (β := ℝ) r ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
R : Type u_1
E : Type u_3
inst : AddGroup E
inst_1 : SMul R ℝ
inst_2 : SMul R ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

Premises used: NNReal, mul_max_of_nonneg, NNReal.smul_def, smul_one_smul, NNReal.coe_nonneg, HSMul.hSMul, smul_eq_mul, OfNat.ofNat
-- 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
p q f g : GroupNorm E
h : Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : GroupNorm E) ↦ f.toFun) f) ((fun (f : GroupNorm E) ↦ f.toFun) g)
obtain :
  ∀ (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)
    (eq_one_of_map_eq_zero' :
      ∀ (x : E),
        { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E }.toFun x = 0 →
          x = 1)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : GroupNorm E) ↦ f.toFun)
          { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
            eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
        ((fun (f : GroupNorm E) ↦ f.toFun) g)),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨_, _, _, _⟩, _⟩ := 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
p q g : GroupNorm 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
eq_one_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E }.toFun x = 0 → x = 1
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
    ((fun (f : GroupNorm E) ↦ f.toFun) g)
mk :
  ∀ (toGroupSeminorm : GroupSeminorm E) (eq_one_of_map_eq_zero'_1 : ∀ (x : E), toGroupSeminorm.toFun x = 0 → x = 1)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : GroupNorm E) ↦ f.toFun)
          { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
            eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
        ((fun (f : GroupNorm E) ↦ f.toFun)
          { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 })),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
      { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 }
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm 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
p q : GroupNorm 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
eq_one_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' : GroupSeminorm E }.toFun x = 0 → x = 1
toGroupSeminorm : GroupSeminorm E
eq_one_of_map_eq_zero'_1 : ∀ (x : E), toGroupSeminorm.toFun x = 0 → x = 1
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : GroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
        eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' })
    ((fun (f : GroupNorm E) ↦ f.toFun)
      { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 })
⊢ { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv',
      eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' : GroupNorm E } =
    { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero'_1 }

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupNorm 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 : GroupNorm 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 : GroupNorm 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 : GroupNorm 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 : GroupNorm 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
p q : GroupNorm 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 : GroupNorm 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:
E : Type u_3
inst : Group E
p q : GroupNorm E
⊢ Eq (α := (a : E) → ℝ) (⇑(p ⊔ q) : (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 : GroupNorm E
x : E
⊢ Eq (α := ℝ) ((p ⊔ q : (a : E) → ℝ) x : ℝ) (max ((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 : AddGroup E
p q f g : NonarchAddGroupNorm E
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ) ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) f)
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)
obtain :
  ∀ (toFun : E → ℝ) (map_zero' : toFun 0 = 0)
    (add_le_max' :
      ∀ (r s : E),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
          max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
            ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s))
    (neg' :
      ∀ (r : E),
        { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
          { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
    (eq_zero_of_map_eq_zero' :
      ∀ (x : E),
        { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' :
                  NonarchAddGroupSeminorm E }.toFun
              x =
            0 →
          x = 0)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
            eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _, _⟩, _⟩ := 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 : AddGroup E
p q g : NonarchAddGroupNorm E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le_max' :
  ∀ (r s : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
      max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
        ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s)
neg' :
  ∀ (r : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r
eq_zero_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' :
              NonarchAddGroupSeminorm E }.toFun
          x =
        0 →
      x = 0
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun) g)
mk :
  ∀ (toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm E)
    (eq_zero_of_map_eq_zero'_1 : ∀ (x : E), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0)
    (h :
      Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
        ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
          { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
            eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
        ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
          { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm,
            eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm E
toFun : E → ℝ
map_zero' : toFun 0 = 0
add_le_max' :
  ∀ (r s : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (r + s) ≤
      max ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r)
        ({ toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun s)
neg' :
  ∀ (r : E),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun (-r) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom E ℝ }.toFun r
eq_zero_of_map_eq_zero' :
  ∀ (x : E),
    { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg' :
              NonarchAddGroupSeminorm E }.toFun
          x =
        0 →
      x = 0
toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm E
eq_zero_of_map_eq_zero'_1 : ∀ (x : E), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0
h :
  Eq.{max (u_3 + 1) 1} (α := (a : E) → ℝ)
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
      { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
        eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' })
    ((fun (f : NonarchAddGroupNorm E) ↦ f.toFun)
      { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 })
⊢ { toFun := toFun, map_zero' := map_zero', add_le_max' := add_le_max', neg' := neg',
      eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' : NonarchAddGroupNorm E } =
    { toNonarchAddGroupSeminorm := toNonarchAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'_1 }

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p : NonarchAddGroupNorm E
⊢ Eq (α := (a : E) → ℝ) (⇑p.toNonarchAddGroupSeminorm : (a : E) → ℝ) (⇑p : (a : E) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : AddGroup E
p q : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm 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 : AddGroup E
p q : NonarchAddGroupNorm E
⊢ Eq (α := (a : E) → ℝ) (⇑(p ⊔ q) : (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 : AddGroup E
p q : NonarchAddGroupNorm E
x : E
⊢ Eq (α := ℝ) ((p ⊔ q : (a : E) → ℝ) x : ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
⊢ ∀ (v : M),
    norm (E := SeparationQuotient M) (ZeroHom.toFun (↑mkAddMonoidHom : ZeroHom M (SeparationQuotient M)) v) ≤ 1 * ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
inst : SeminormedAddCommGroup M
m : M
⊢ norm (E := SeparationQuotient M) ((normedMk : (a : M) → SeparationQuotient M) m : SeparationQuotient M) ≤ 1 * ‖m‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : Inseparable x y
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x - y) : N) (0 : N)
⊢ HSub.hSub (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) = 0

Tactic:
rw [← map_sub]

Premises used: map_sub
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : Inseparable x y
⊢ ‖x - y‖ = 0

Tactic:
rw [Metric.inseparable_iff, dist_eq_norm] at h

Premises used: dist_eq_norm, Metric.inseparable_iff
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : ‖x - y‖ = 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x - y) : N) (0 : N)

Tactic:
hf (x - y) h

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
x y : M
h : ‖x - y‖ = 0
⊢ Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (x - y) : N) (0 : N)

Tactic:
exact hf (x - y) h

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
⊢ ∃ (C : ℝ),
    ∀ (v : SeparationQuotient M),
      norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤
        C * ‖v‖

Tactic:
⟨‖f‖, fun v ↦ ?_⟩

Premises used: Norm.norm, Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
refine :
  ∀ (v : SeparationQuotient M),
    norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤
      ‖f‖ * ‖v‖
⊢ ∃ (C : ℝ),
    ∀ (v : SeparationQuotient M),
      norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤
        C * ‖v‖

Tactic:
refine ⟨‖f‖, fun v ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
v : SeparationQuotient M
obtain :
  ∀ (v : M),
    norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) (mk v) : N) ≤
      ‖f‖ * norm (E := SeparationQuotient M) (mk v)
⊢ norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) v : N) ≤ ‖f‖ * ‖v‖

Tactic:
obtain ⟨v, rfl⟩ := surjective_mk v

Premises used: SeparationQuotient.surjective_mk, rfl
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
v : M
⊢ norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) (mk v) : N) ≤
    ‖f‖ * norm (E := SeparationQuotient M) (mk v)

Tactic:
le_opNorm f v

Premises used: Quotient.liftOn', NormedAddGroupHom.le_opNorm, SeparationQuotient.lift
-- Module: Mathlib.Analysis.Normed.Group.SeparationQuotient
Goal:
M : Type u_1
N : Type u_2
inst : SeminormedAddCommGroup M
inst_1 : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (0 : N)
v : M
⊢ norm.{u_2} (E := N) ((liftContinuousAddMonoidHom (↑f : M →ₜ+ N) ⋯ : (a : SeparationQuotient M) → N) (mk v) : N) ≤
    ‖f‖ * norm (E := SeparationQuotient M) (mk v)

Tactic:
exact le_opNorm f v

Premises used: NormedAddGroupHom.le_opNorm