awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NormedAddCommGroup β
inst_2 : Lattice β
inst_3 : HasSolidNorm β
inst_4 : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist.{v} (α := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β) ≤ C₂
x y : α
⊢ dist.{v} (α := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
      (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β) ≤
    C₁ + C₂
have simp_rw : ∀ (hf : ∀ (x y : α), ‖HSub.hSub (α := β) (β := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)‖ ≤ C₁)
  (hg : ∀ (x y : α), ‖HSub.hSub (α := β) (β := β) ((g : (a : α) → β) x : β) ((g : (a : α) → β) y : β)‖ ≤ C₂),
  ‖HSub.hSub (α := β) (β := β) (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) x : β)
        (((⇑f : (a : α) → β) ⊓ (⇑g : (a : α) → β)) y : β)‖ ≤
    C₁ + C₂
Tactic: simp_rw [dist_eq_norm_sub] at hf hg ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (hypothesis)
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|
⊢ ‖f‖ ≤ ‖g‖
have i1 : ∀ (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)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
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 : β)
⊢ ‖f‖ ≤ ‖g‖
have rw : ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ ‖g‖
Tactic: rw [norm_le (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
⊢ (⇑f : (a : α) → ℝ) =
    HSub.hSub (α := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0)) (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0))
have h : ∀ (x : α),
  (f : (a : α) → ℝ) x =
    HSub.hSub (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (f : (a : α) → ℝ) x =
    HSub.hSub (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
have h : (f : (a : α) → ℝ) x = HSub.hSub (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
⊢ abs ∘ (⇑f : (a : α) → ℝ) =
    HAdd.hAdd (α := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0)) (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0))
have h : ∀ (x : α),
  (abs ∘ (⇑f : (a : α) → ℝ)) x =
    HAdd.hAdd (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (abs ∘ (⇑f : (a : α) → ℝ)) x =
    HAdd.hAdd (α := α → ℝ) (β := α → ℝ) (toReal ∘ (⇑f.nnrealPart : (a : α) → ℝ≥0))
      (toReal ∘ (⇑(-f).nnrealPart : (a : α) → ℝ≥0)) x
have h : |(f : (a : α) → ℝ) x| = HAdd.hAdd (α := ℝ) (β := ℝ) (max ((f : (a : α) → ℝ) x) 0 : ℝ) (max (-(f : (a : α) → ℝ) x) 0 : ℝ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖
have linarith : HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ < 0 →
  HAdd.hAdd (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ - 0 + HSub.hSub (β := ℝ) (-‖f‖) ((f : (a : α) → ℝ) x : ℝ) = 0
Tactic: linarith [(abs_le.mp (norm_coe_le_norm f x)).1]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Normed (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ)
have linarith : HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ) < 0 →
  HSub.hSub (β := ℝ) ‖f‖ ((f : (a : α) → ℝ) x : ℝ) - 0 + HSub.hSub (α := ℝ) ((f : (a : α) → ℝ) x : ℝ) ‖f‖ = 0
Tactic: linarith [(abs_le.mp (norm_coe_le_norm f x)).2]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Star (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
have rw : ∀ (x : α), norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖
Tactic: rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _), norm_le (Real.sqrt_nonneg _)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Bounded.Star (goal)
Goal:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing β
inst_2 : StarRing β
inst_3 : CStarRing β
f : α →ᵇ β
x : α
⊢ norm.{v} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖
have rw : ‖HMul.hMul (α := β) (β := β) (star ((f : (a : α) → β) x) : β) ((f : (a : α) → β) x : β)‖ ≤ ‖star f * f‖
Tactic: rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
have pos : ∀ (hs : Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))),
  ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
Tactic: by_cases hs : (tsupport f).Nonempty
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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‖
⊢ ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
have neg : ∀ (hs : ¬Set.Nonempty.{u_1} (α := α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ))),
  ∃ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
Tactic: by_cases hs : (tsupport f).Nonempty
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
have 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‖
Tactic: obtain ⟨x, _, hmax⟩ := mem_compactlySupported.mp h |>.exists_isMaxOn hs <|
      (map_continuous f).norm.continuousOn
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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‖
have pos : ∀ (y : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
Tactic: refine ⟨x, le_antisymm (norm_coe_le_norm f x) (norm_le (norm_nonneg _) |>.mpr fun y ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : α
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
have 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 : γ)
Tactic: by_cases hy : y ∈ tsupport f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : γ)
⊢ norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
have neg : ∀ (hy : y ∉ tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)),
  norm.{u_2} (E := γ) ((f : (a : α) → γ) y : γ) ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ)
Tactic: by_cases hy : y ∈ tsupport f
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖
have neg : f = 0
Tactic: suffices f = 0 by simp [this]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : α) → γ))
⊢ f = 0
have neg : ∀ (hs : Eq.{u_1 + 1} (α := Set α) (tsupport.{u_1, u_2} (α := γ) (⇑f : (a : α) → γ)) ∅), f = 0
Tactic: rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
⊢ f = 0
have neg₁ : ∀ (hs : Eq (α := α → γ) (⇑f : (a : α) → γ) 0), f = 0
Tactic: rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
⊢ f = 0
have neg₂ : ∀ (hs : Eq (α := α → γ) (⇑f : (a : α) → γ) (⇑0 : (a : α) → γ)), f = 0
Tactic: rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
⊢ f = 0
have neg₃ : ∀ (hs : f = 0), f = 0
Tactic: rwa [not_nonempty_iff_eq_empty, tsupport_eq_empty_iff, ← coe_zero, ← DFunLike.ext'_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
have refine : (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
Tactic: refine ⟨fun hn x ↦ lt_of_le_of_lt (norm_coe_le_norm f x) hn, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
M0 : 0 < M
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
have inl : ∀ (he : IsEmpty α), (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
Tactic: obtain (he | he) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
⊢ (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
have inr : ∀ (he : Nonempty α), (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
Tactic: obtain (he | he) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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 : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
have inr : ∀ (x : α) (hx : norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) = ‖f‖),
  (∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M) → ‖f‖ < M
Tactic: obtain ⟨x, hx⟩ := exist_norm_eq h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
have inl : ∀ (hM : 0 < M), ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
Tactic: obtain (hM | hM) := lt_or_ge 0 M
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
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
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
have inr : ∀ (hM : M ≤ 0), ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
Tactic: obtain (hM | hM) := lt_or_ge 0 M
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
⊢ Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤ ↔ IsCompact.{u_1} (X := α) univ
have refine : ∀ (h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤), IsCompact.{u_1} (X := α) univ
Tactic: refine ⟨fun h ↦ ?_, compactlySupported_eq_top_of_isCompact⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤
⊢ IsCompact.{u_1} (X := α) univ
have obtain : ∀ (x : γ) (hx : x ≠ 0), IsCompact.{u_1} (X := α) univ
Tactic: obtain ⟨x, hx⟩ := exists_ne (0 : γ)
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
have inl : ∀ (hs : tsupport g = ∅), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
Tactic: obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
inl : ∀ (hs : tsupport g = ∅), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
have inr : ∀ (hs : (tsupport g).Nonempty), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
Tactic: obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
have inr : ∀ z ∈ tsupport g,
  ∀ (hmax : IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖g x‖) (tsupport g) z), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
Tactic: obtain ⟨z, _, hmax⟩ := hg₂.exists_isMaxOn hs <| hg₁.norm.continuousOn
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left : z ∈ tsupport g
hmax : IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖g x‖) (tsupport g) z
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
have inr : ∀ (x : α), ‖g x‖ ≤ ‖g z‖
Tactic: refine ⟨2 * ‖g z‖, dist_le_two_norm' fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left : z ∈ tsupport g
hmax : IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖g x‖) (tsupport g) z
x : α
⊢ ‖g x‖ ≤ ‖g z‖
have pos : ∀ (hx : x ∈ tsupport g), ‖g x‖ ≤ ‖g z‖
Tactic: by_cases hx : x ∈ tsupport g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left : z ∈ tsupport g
hmax : IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖g x‖) (tsupport g) z
x : α
pos : ∀ (hx : x ∈ tsupport g), ‖g x‖ ≤ ‖g z‖
⊢ ‖g x‖ ≤ ‖g z‖
have neg : ∀ (hx : x ∉ tsupport g), ‖g x‖ ≤ ‖g z‖
Tactic: by_cases hx : x ∈ tsupport g
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ)
    (ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) ⋯ ⋯)
have apply : HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
  (⇑(ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) sorry sorry) :
    (a : α) → γ)
Tactic: apply mem_compactlySupported.mpr
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.BoundedCompactlySupported (goal)
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑(ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) ⋯ ⋯) :
      (a : α) → γ)
have rw : HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
  (⇑{ toFun := HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ), continuous_toFun := sorry,
        map_bounded' := sorry : α →ᵇ γ } :
    (a : α) → γ)
Tactic: rw [ofCompactSupport]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : CocompactMap α β
h : Eq (α := (a : α) → β) ((fun (f : CocompactMap α β) ↦ f.toFun) f) ((fun (f : CocompactMap α β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (continuous_toFun : Continuous toFun)
  (cocompact_tendsto' :
    Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (cocompact β))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : CocompactMap α β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' })
      ((fun (f : CocompactMap α β) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
      CocompactMap α β } =
    g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h