awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑f⁺ : (a : α) → β) (⇑f : (a : α) → β)⁺

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑f⁻ : (a : α) → β) (⇑f : (a : α) → β)⁻

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
h : |f| ≤ |g|
⊢ ∀ (t : α), norm.{v} (E := β) ((f : (a : α) → β) t : β) ≤ norm.{v} (E := β) ((g : (a : α) → β) t : β)

Tactic:
have i1 : ∀ t, ‖f t‖ ≤ ‖g t‖ := fun t => HasSolidNorm.solid (h t)
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
h : |f| ≤ |g|
i1 : ∀ (t : α), norm.{v} (E := β) ((f : (a : α) → β) t : β) ≤ norm.{v} (E := β) ((g : (a : α) → β) t : β)
rw : ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ ‖g‖
⊢ ‖f‖ ≤ ‖g‖

Tactic:
rw [norm_le (norm_nonneg _)]

Premises used: BoundedContinuousFunction.norm_le, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
h : |f| ≤ |g|
i1 : ∀ (t : α), norm.{v} (E := β) ((f : (a : α) → β) t : β) ≤ norm.{v} (E := β) ((g : (a : α) → β) t : β)
⊢ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ ‖g‖

Tactic:
fun t => (i1 t).trans (norm_coe_le_norm g t)

Premises used: BoundedContinuousFunction.norm_coe_le_norm, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
h : |f| ≤ |g|
i1 : ∀ (t : α), norm.{v} (E := β) ((f : (a : α) → β) t : β) ≤ norm.{v} (E := β) ((g : (a : α) → β) t : β)
⊢ ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ ‖g‖

Tactic:
exact fun t => (i1 t).trans (norm_coe_le_norm g t)

Premises used: BoundedContinuousFunction.norm_coe_le_norm, LE.le.trans
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
h₁ : f ≤ g
h : α →ᵇ β
t : α
⊢ LE.le.{v} (α := (fun (a : α) ↦ β) t) ((fun (f : α →ᵇ β) ↦ f.toFun) (f + h) t) ((fun (f : α →ᵇ β) ↦ f.toFun) (g + h) t)

Tactic:
simpa using h₁ _
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
⊢ Eq (α := (a : α) → ℝ≥0) (⇑f.nnrealPart : (a : α) → ℝ≥0) (Real.toNNReal ∘ (⇑f : (a : α) → ℝ))

Tactic:
rfl

Premises used: NNReal.mk, rfl, Real.toNNReal
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
⊢ Eq (α := (a : α) → ℝ≥0) (⇑f.nnnorm : (a : α) → ℝ≥0) (Function.comp (β := ℝ) NNNorm.nnnorm (⇑f : (a : α) → ℝ))

Tactic:
rfl

Premises used: NNReal.mk, rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
h :
  ∀ (x : α),
    (f : (a : α) → ℝ) x =
      HSub.hSub (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
        (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
⊢ (⇑f : (a : α) → ℝ) =
    HSub.hSub (α := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0)) (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0))

Tactic:
funext x
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
h :
  (f : (a : α) → ℝ) x = HSub.hSub (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
⊢ (f : (a : α) → ℝ) x =
    HSub.hSub (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x

Tactic:
dsimp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (f : (a : α) → ℝ) x = HSub.hSub (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp only [max_zero_sub_max_neg_zero_eq_self]

Premises used: max_zero_sub_max_neg_zero_eq_self
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
h :
  ∀ (x : α),
    (abs ∘ (⇑f : (a : α) → ℝ)) x =
      HAdd.hAdd (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
        (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
⊢ abs ∘ (⇑f : (a : α) → ℝ) =
    HAdd.hAdd (α := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0)) (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0))

Tactic:
funext x
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
h :
  |(f : (a : α) → ℝ) x| =
    HAdd.hAdd (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
⊢ (abs ∘ (⇑f : (a : α) → ℝ)) x =
    HAdd.hAdd (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x

Tactic:
dsimp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ |(f : (a : α) → ℝ) x| =
    HAdd.hAdd (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)

Tactic:
simp only [max_zero_add_max_neg_zero_eq_abs_self]

Premises used: max_zero_add_max_neg_zero_eq_abs_self
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
linarith :
  HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ < 0 →
    HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ - 0 + HSub.hSub (β := ℝ) (-‖f‖) ((f : (a : α) → ℝ) x : ℝ) = 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖

Tactic:
linarith [(abs_le.mp (norm_coe_le_norm f x)).1]

Premises used: abs_le, And.left, BoundedContinuousFunction.norm_coe_le_norm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Normed
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
linarith :
  HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ) < 0 →
    HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ) - 0 + HSub.hSub (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ = 0
⊢ 0 ≤ HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ)

Tactic:
linarith [(abs_le.mp (norm_coe_le_norm f x)).2]

Premises used: abs_le, And.right, BoundedContinuousFunction.norm_coe_le_norm, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑(star f) : (a : α) → β) (star (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
f : α →ᵇ β
x : α
⊢ Eq.{v + 1} (α := β) ((star f : (a : α) → β) x : β) (star ((f : (a : α) → β) x) : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst : NormedField 𝕜
inst_1 : StarRing 𝕜
inst_2 : TopologicalSpace α
inst_3 : SeminormedAddCommGroup β
inst_4 : StarAddMonoid β
inst_5 : NormedStarGroup β
inst_6 : NormedSpace 𝕜 β
inst_7 : StarModule 𝕜 β
f : α →ᵇ β
⊢ ‖star f‖ ≤ ‖f‖

Tactic:
simp only [norm_eq, star_apply, norm_star, le_of_eq]

Premises used: norm_star, BoundedContinuousFunction.norm_eq, BoundedContinuousFunction.star_apply, le_of_eq
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
rw : ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]

Premises used: BoundedContinuousFunction.norm_le, Real.le_sqrt, sq, Real.sqrt_nonneg, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
x : α
rw : ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖
⊢ norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖

Tactic:
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]

Premises used: Real.le_sqrt, sq, CStarRing.norm_star_mul_self, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
x : α
⊢ ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖

Tactic:
norm_coe_le_norm (star f * f) x

Premises used: HMul.hMul, setOf, BoundedContinuousFunction.norm_coe_le_norm, Star.star
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
x : α
⊢ ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖

Tactic:
exact norm_coe_le_norm (star f * f) x

Premises used: HMul.hMul, BoundedContinuousFunction.norm_coe_le_norm, Star.star
-- Module: Mathlib.Topology.ContinuousMap.Bounded.Star
Goal:
α : Type u
β : Type v
𝕜 : Type u_2
inst : NormedField 𝕜
inst_1 : TopologicalSpace α
inst_2 : NormedRing β
inst_3 : NormedAlgebra 𝕜 β
inst_4 : StarAddMonoid β
inst_5 : NormedStarGroup β
f : α →ᵇ β
⊢ Eq (α := (a : α) → β) (⇑((toContinuousMapStarₐ 𝕜 : (a : α →ᵇ β) → C(α, β)) f : C(α, β)) : (a : α) → β)
    (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
⊢ Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f ↔
    HasCompactSupport.{u_1, u_2} (α := α) (β := γ) (⇑f : (a : α) → γ)

Tactic:
TwoSidedIdeal.mem_mk' {z : α →ᵇ γ | HasCompactSupport z} .zero .add .neg .mul_left .mul_right f

Premises used: Set.Mem, setOf, HasCompactSupport.neg, HasCompactSupport.add, HasCompactSupport.mul_right, HasCompactSupport.mul_left, HasCompactSupport.zero, DFunLike.coe, IsCompact, TwoSidedIdeal.mem_mk', HasCompactSupport
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
pos :
  ∀ (hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))),
    ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
neg :
  ∀ (hs : ¬Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))),
    ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
by_cases hs : (tsupport f).Nonempty

Premises used: tsupport, Set.Nonempty, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
pos :
  ∀ (x : α),
    Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x →
      ∀
        (hmax :
          IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
            (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x),
        ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
obtain ⟨x, _, hmax⟩ := mem_compactlySupported.mp h |>.exists_isMaxOn hs <|
      (map_continuous f).norm.continuousOn

Premises used: Continuous.continuousOn, Continuous.norm, mem_compactlySupported, Iff.mp, ContinuousMapClass.map_continuous, IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, le_antisymm, BoundedContinuousFunction.norm_coe_le_norm, Exists.intro, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
pos : ∀ (y : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
refine ⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
y : α
pos :
  ∀ (hy : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) y),
    norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
neg :
  ∀ (hy : y ∉ tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)),
    norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)

Tactic:
by_cases hy : y ∈ tsupport f

Premises used: tsupport, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
y : α
hy : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) y
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)

Tactic:
hmax hy

Premises used: Set.Mem
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
y : α
hy : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) y
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)

Tactic:
exact hmax hy
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
x : α
left : Membership.mem (γ := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
hmax :
  IsMaxOn (β := ℝ) (fun (x : α) ↦ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ))
    (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) x
y : α
hy : y ∉ tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)

Tactic:
simp [image_eq_zero_of_notMem_tsupport hy]

Premises used: image_eq_zero_of_notMem_tsupport
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : ¬Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
this : f = 0
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
simp [this]
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : ¬Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
neg : f = 0
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖

Tactic:
suffices f = 0 by simp [this]
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
hs : ¬Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))
neg : ∀ (hs : Eq.{u_1 + 1} (α := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) ∅), f = 0
neg₁ : ∀ (hs : Eq (α := α → γ) (⇑f : (a : α) → γ) 0), f = 0
neg₂ : ∀ (hs : Eq (α := α → γ) (⇑f : (a : α) → γ) (⇑0 : (a : α) → γ)), f = 0
neg₃ neg₄ neg₅ neg₆ : ∀ (hs : f = 0), f = 0
⊢ f = 0

Tactic:
rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs

Premises used: DFunLike.ext'_iff, Set.not_nonempty_iff_eq_empty, BoundedContinuousFunction.coe_zero, tsupport_eq_empty_iff
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M

Tactic:
⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩

Premises used: lt_of_le_of_lt, BoundedContinuousFunction.norm_coe_le_norm, Iff.intro
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
refine : (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M

Tactic:
refine ⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
inl : ∀ (he : IsEmpty α), (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
inr : ∀ (he : Nonempty α), (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M

Tactic:
obtain (he | he) := isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M

Tactic:
simpa
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
he : Nonempty α
inr :
  ∀ (x : α) (hx : norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖),
    (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M

Tactic:
obtain ⟨x, hx⟩ := exist_norm_eq h

Premises used: exist_norm_eq
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
he : Nonempty α
x : α
hx : norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M

Tactic:
fun h ↦ hx ▸ h x

Premises used: Eq.rec
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
he : Nonempty α
x : α
hx : norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M

Tactic:
exact fun h ↦ hx ▸ h x
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
inl : ∀ (hM : 0 < M), ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
inr : ∀ (hM : M ≤ 0), ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M

Tactic:
obtain (hM | hM) := lt_or_ge 0 M

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M

Tactic:
norm_lt_iff_of_compactlySupported h hM

Premises used: norm_lt_iff_of_compactlySupported