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 : 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)
inr :
  ∀ (p : (↑s : Type u_3)),
    HAdd.hAdd (α := ℝ) (β := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
        (((↑p : GroupSeminorm E) : (a : E) → ℝ) 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:
refine ciSup_le fun p ↦ (map_mul_le_add p.1 x y).trans ?_

Premises used: ciSup_le
-- 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 : 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)
inr :
  LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
inr₁ :
  LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
      (((↑p : GroupSeminorm E) : (a : E) → ℝ) 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:
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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 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)
apply :
  BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
      ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) ∘ Subtype.val (p := fun (x : GroupSeminorm E) ↦ x ∈ s)))
⊢ LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p

Premises used: le_ciSup
-- 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 : 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)
x_1 x_2 : GroupSeminorm E
h' : x_1 ≤ x_2
⊢ LE.le (α := ℝ) ((x_1 : (a : E) → ℝ) x : ℝ) ((x_2 : (a : E) → ℝ) x : ℝ)

Tactic:
h' _
-- 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 : 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)
x_1 x_2 : GroupSeminorm E
h' : x_1 ≤ x_2
⊢ LE.le (α := ℝ) ((x_1 : (a : E) → ℝ) x : ℝ) ((x_2 : (a : E) → ℝ) x : ℝ)

Tactic:
exact h' _
-- 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 : 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)
⊢ BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
      ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) ∘ Subtype.val (p := fun (x : GroupSeminorm E) ↦ x ∈ s)))

Tactic:
simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Premises used: Set.range_comp, Monotone.map_bddAbove
-- 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 : 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)
apply :
  BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
      ((fun (x : GroupSeminorm E) ↦ (x : (a : E) → ℝ) y) ∘ Subtype.val (p := fun (x : GroupSeminorm E) ↦ x ∈ s)))
⊢ LE.le (α := ℝ) (((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) y : ℝ)

Tactic:
apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p

Premises used: le_ciSup
-- 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 : 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)
x_1 x_2 : GroupSeminorm E
h' : x_1 ≤ x_2
⊢ LE.le (α := ℝ) ((x_1 : (a : E) → ℝ) y : ℝ) ((x_2 : (a : E) → ℝ) y : ℝ)

Tactic:
h' _
-- 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 : 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)
x_1 x_2 : GroupSeminorm E
h' : x_1 ≤ x_2
⊢ LE.le (α := ℝ) ((x_1 : (a : E) → ℝ) y : ℝ) ((x_2 : (a : E) → ℝ) y : ℝ)

Tactic:
exact h' _
-- 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 : 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)
⊢ BddAbove (α := ℝ)
    (range.{0, max 1 (u_3 + 1)} (ι := { x : GroupSeminorm E // x ∈ s })
      ((fun (x : GroupSeminorm E) ↦ (x : (a : E) → ℝ) y) ∘ Subtype.val (p := fun (x : GroupSeminorm E) ↦ x ∈ s)))

Tactic:
simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

Premises used: Set.range_comp, Monotone.map_bddAbove
-- 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 : E
⊢ Eq (α := ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x⁻¹)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
simp [SupSet.sSup, hs]

Premises used: SupSet.sSup
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
simp :
  Eq (α := ℝ)
    (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x, map_one' := ⋯,
            mul_le' := ⋯, inv' := ⋯ } :
          (a : E) → ℝ)
        x :
      ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
simp [SupSet.sSup, hs]

Premises used: SupSet.sSup
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ Eq (α := ℝ)
    (({ toFun := fun (x : E) ↦ ⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x, map_one' := ⋯,
            mul_le' := ⋯, inv' := ⋯ } :
          (a : E) → ℝ)
        x :
      ℝ)
    (⨆ (p : (↑s : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
rw :
  Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x))
    (sSup ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s))
⊢ Eq (α := ℝ) ((sSup s : (a : E) → ℝ) x : ℝ) (sSup ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s) : ℝ)

Tactic:
rw [coe_sSup_apply hs, ← sSup_range]

Premises used: sSup_range, GroupSeminorm.coe_sSup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
e_a :
  Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
    ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s)
⊢ Eq (α := ℝ) (sSup (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x))
    (sSup ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s))

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
e_a :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x) x_1 ↔
      Membership.mem (γ := Set ℝ) ((fun (x_2 : GroupSeminorm E) ↦ (x_2 : (a : E) → ℝ) x) '' s) x_1
⊢ Eq (α := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
    ((fun (x_1 : GroupSeminorm E) ↦ (x_1 : (a : E) → ℝ) x) '' s)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
x_1 : ℝ
⊢ Membership.mem (γ := Set ℝ) (range fun (p : (↑s : Type u_3)) ↦ ((↑p : GroupSeminorm E) : (a : E) → ℝ) x) x_1 ↔
    Membership.mem (γ := Set ℝ) ((fun (x_2 : GroupSeminorm E) ↦ (x_2 : (a : E) → ℝ) x) '' s) x_1

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
rw :
  Eq (α := ℝ) (⨆ (p : (↑(range f) : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
    (⨆ (i : ι), (f i : (a : E) → ℝ) x)
⊢ Eq (α := ℝ) ((⨆ (i : ι), f i : (a : E) → ℝ) x : ℝ) (⨆ (i : ι), (f i : (a : E) → ℝ) x : ℝ)

Tactic:
rw [← sSup_range, coe_sSup_apply h]

Premises used: sSup_range, GroupSeminorm.coe_sSup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι),
    Eq (α := ℝ) (((↑(rangeFactorization f x_1) : GroupSeminorm E) : (a : E) → ℝ) x : ℝ) ((f x_1 : (a : E) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ Eq (α := ℝ) (⨆ (p : (↑(range f) : Type u_3)), ((↑p : GroupSeminorm E) : (a : E) → ℝ) x)
    (⨆ (i : ι), (f i : (a : E) → ℝ) x)

Tactic:
exact (Set.rangeFactorization_surjective.iSup_congr _ (by simp)) |>.symm

Premises used: Function.Surjective.iSup_congr, Set.rangeFactorization_surjective, Eq.symm
-- 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
rw : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) (0 : ℝ)
rw₁ : Eq (α := ℝ) (max ((p : (a : E) → ℝ) 1) ((q : (a : E) → ℝ) 1) : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
rw₂ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) ((p : (a : E) → ℝ) 1 : ℝ)
rw₃ : LE.le (α := ℝ) ((q : (a : E) → ℝ) 1 : ℝ) (0 : ℝ)
rw₄ rw₅ : LE.le (α := ℝ) 0 0
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) 1) 0

Tactic:
rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]

Premises used: GroupSeminormClass.map_one_eq_zero, sup_eq_left, Pi.sup_apply
-- 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
rw :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x : ℝ)
rw₁ :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x⁻¹) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
rw₂ :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x⁻¹) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
rw₃ rw₄ :
  Eq (α := ℝ) (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
    (max ((p : (a : E) → ℝ) x) ((q : (a : E) → ℝ) x) : ℝ)
⊢ Eq (α := ℝ) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x⁻¹) (((⇑p : (a : E) → ℝ) ⊔ (⇑q : (a : E) → ℝ)) x)

Tactic:
rw [Pi.sup_apply, Pi.sup_apply, map_inv_eq_map p, map_inv_eq_map q]

Premises used: GroupSeminormClass.map_inv_eq_map, Pi.sup_apply
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p q : GroupSeminorm 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 : GroupSeminorm 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 : Group E
inst_1 : Group F
inst_2 : Group G
p_1 q : GroupSeminorm E
f_1 : F →* E
p : GroupSeminorm E
f : F →* E
simp_rw : Eq (α := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) 1 : E) : ℝ) (0 : ℝ)

Tactic:
simp_rw [f.map_one, map_one_eq_zero p]

Premises used: GroupSeminormClass.map_one_eq_zero, MonoidHom.map_one
-- 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 : GroupSeminorm E
f_1 : F →* E
p : GroupSeminorm E
f : F →* E
x : F
simp_rw :
  Eq (α := ℝ) ((p : (a : E) → ℝ) (((f : (a : F) → E) x)⁻¹ : E) : ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x : E) : ℝ)
⊢ Eq (α := ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x⁻¹ : E) : ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x : E) : ℝ)

Tactic:
simp_rw [map_inv, map_inv_eq_map p]

Premises used: map_inv, GroupSeminormClass.map_inv_eq_map
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
p : GroupSeminorm E
f : F →* E
⊢ Eq (α := (a : F) → ℝ) (⇑(p.comp f) : (a : F) → ℝ) (Function.comp (β := E) (⇑p : (a : E) → ℝ) (⇑f : (a : F) → E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
p : GroupSeminorm E
f : F →* E
x : F
⊢ Eq (α := ℝ) ((p.comp f : (a : F) → ℝ) x : ℝ) ((p : (a : E) → ℝ) ((f : (a : F) → E) x : E) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : Group E
p : GroupSeminorm E
⊢ p.comp (MonoidHom.id E) = p

Tactic:
ext fun _ => rfl

Premises used: GroupSeminorm.ext, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
p : GroupSeminorm E
⊢ Eq.{u_4 + 1} (α := GroupSeminorm F) (p.comp 1) 0

Tactic:
ext fun _ => map_one_eq_zero p

Premises used: GroupSeminormClass.map_one_eq_zero, GroupSeminorm.ext
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
f : F →* E
⊢ comp 0 f = 0

Tactic:
ext fun _ => rfl

Premises used: GroupSeminorm.ext, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
G : Type u_5
inst : Group E
inst_1 : Group F
inst_2 : Group G
p : GroupSeminorm E
g : F →* E
f : G →* F
⊢ p.comp (g.comp f) = (p.comp g).comp f

Tactic:
ext fun _ => rfl

Premises used: GroupSeminorm.ext, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
p q : GroupSeminorm E
f : F →* E
⊢ (p + q).comp f = p.comp f + q.comp f

Tactic:
ext fun _ => rfl

Premises used: GroupSeminorm.ext, rfl
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : Group E
inst_1 : Group F
p q : GroupSeminorm E
f : F →* E
hp : p ≤ q
⊢ p.comp f ≤ q.comp f

Tactic:
fun _ => hp _

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
F : Type u_4
inst : CommGroup E
inst_1 : CommGroup F
p : GroupSeminorm E
f g : F →* E
⊢ p.comp (f * g) ≤ p.comp f + p.comp g

Tactic:
fun _ =>
  map_mul_le_add p _ _

Premises used: MulLEAddHomClass.map_mul_le_add, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : CommGroup E
p q : GroupSeminorm E
x_1 x : E
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x : ℝ) ((q : (a : E) → ℝ) (x_1 / x) : ℝ)

Tactic:
positivity
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x : E
p q : GroupSeminorm E
x_1 : E
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_1 : ℝ) ((q : (a : E) → ℝ) (1 / x_1) : ℝ)

Tactic:
positivity
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
rwa : HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
rwa₁ : HAdd.hAdd (α := ℝ) (β := ℝ) (0 : ℝ) ((q : (a : E) → ℝ) 1 : ℝ) < r
rwa₂ : HAdd.hAdd (α := ℝ) 0 0 < r
rwa₃ rwa₄ rwa₅ rwa₆ : 0 < r
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) 1 : ℝ) ((q : (a : E) → ℝ) (1 / 1) : ℝ) < r

Tactic:
rwa [div_one, map_one_eq_zero p, map_one_eq_zero q, add_zero]

Premises used: GroupSeminormClass.map_one_eq_zero, add_zero, div_one
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
⊢ ⨅ (y_1 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y_1 : ℝ) ((q : (a : E) → ℝ) (x * y / y_1) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)

Tactic:
ciInf_le_of_le mul_bddBelow_range_add (u * v) ?_

Premises used: HMul.hMul, ciInf_le_of_le, GroupSeminorm.mul_bddBelow_range_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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
refine :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x * y / (u * v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
⊢ ⨅ (y_1 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y_1 : ℝ) ((q : (a : E) → ℝ) (x * y / y_1) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)

Tactic:
refine ciInf_le_of_le mul_bddBelow_range_add (u * v) ?_

Premises used: HMul.hMul, ciInf_le_of_le, GroupSeminorm.mul_bddBelow_range_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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x / u * (y / v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((p : (a : E) → ℝ) v : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x * y / (u * v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) v : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)

Tactic:
rw [mul_div_mul_comm, add_add_add_comm]

Premises used: mul_div_mul_comm, add_add_add_comm
-- 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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x / u * (y / v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((p : (a : E) → ℝ) v : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)

Tactic:
add_le_add (map_mul_le_add p _ _) (map_mul_le_add q _ _)

Premises used: add_le_add, MulLEAddHomClass.map_mul_le_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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x y u v : E
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) (u * v) : ℝ) ((q : (a : E) → ℝ) (x / u * (y / v)) : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) u : ℝ) ((p : (a : E) → ℝ) v : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((q : (a : E) → ℝ) (x / u) : ℝ) ((q : (a : E) → ℝ) (y / v) : ℝ)

Tactic:
exact add_le_add (map_mul_le_add p _ _) (map_mul_le_add q _ _)

Premises used: add_le_add, MulLEAddHomClass.map_mul_le_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 : CommGroup E
inst_1 : CommGroup F
p_1 q_1 : GroupSeminorm E
x_1 : E
p q : GroupSeminorm E
x : E
simp_rw :
  Eq (α := ℝ)
    (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
simp_rw₁ :
  Eq (α := ℝ) (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2 : ℝ) ((q : (a : E) → ℝ) (x / x_2)⁻¹ : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))
⊢ Eq (α := ℝ)
    (⨅ (x_2 : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) x_2⁻¹ : ℝ) ((q : (a : E) → ℝ) (x⁻¹ / x_2⁻¹) : ℝ))
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ))

Tactic:
simp_rw [map_inv_eq_map p, ← inv_div', map_inv_eq_map q]

Premises used: GroupSeminormClass.map_inv_eq_map, inv_div'
-- Module: Mathlib.Analysis.Normed.Group.Seminorm
Goal:
E : Type u_3
inst : CommGroup E
p q : GroupSeminorm E
x : E
⊢ Eq (α := ℝ) ((p ⊓ q : (a : E) → ℝ) x : ℝ)
    (⨅ (y : E), HAdd.hAdd (α := ℝ) (β := ℝ) ((p : (a : E) → ℝ) y : ℝ) ((q : (a : E) → ℝ) (x / y) : ℝ) : ℝ)

Tactic:
rfl

Premises used: iInf, rfl