awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
⊢ ‖star f‖ ≤ ‖f‖
have rw : ‖mkOfCompact (star f)‖ ≤ ‖f‖
Tactic: rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star,
      norm_star, BoundedContinuousFunction.norm_mkOfCompact]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
rw : ‖mkOfCompact (star f)‖ ≤ ‖f‖
⊢ ‖star f‖ ≤ ‖f‖
have rw₁ : ‖star (mkOfCompact f)‖ ≤ ‖f‖
Tactic: rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star,
      norm_star, BoundedContinuousFunction.norm_mkOfCompact]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
rw : ‖mkOfCompact (star f)‖ ≤ ‖f‖
rw₁ : ‖star (mkOfCompact f)‖ ≤ ‖f‖
⊢ ‖star f‖ ≤ ‖f‖
have rw₂ : ‖mkOfCompact f‖ ≤ ‖f‖
Tactic: rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star,
      norm_star, BoundedContinuousFunction.norm_mkOfCompact]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
rw : ‖mkOfCompact (star f)‖ ≤ ‖f‖
rw₁ : ‖star (mkOfCompact f)‖ ≤ ‖f‖
rw₂ : ‖mkOfCompact f‖ ≤ ‖f‖
⊢ ‖star f‖ ≤ ‖f‖
have rw₃ : ‖f‖ ≤ ‖f‖
Tactic: rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star,
      norm_star, BoundedContinuousFunction.norm_mkOfCompact]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖
have rw : ∀ (x : α), norm.{u_2} (E := β) ((f : (a : α) → β) x : β) ≤ √‖star f * f‖
Tactic: rw [← sq, ← Real.le_sqrt (norm_nonneg _) (norm_nonneg _),
      ContinuousMap.norm_le _ (Real.sqrt_nonneg _)]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : NonUnitalNormedRing β
inst_3 : StarRing β
inst_4 : CStarRing β
f : C(α, β)
x : α
⊢ norm.{u_2} (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.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f g : α →C_c β
h : Eq (α := (a : α) → β) ((fun (f : α →C_c β) ↦ f.toFun) f) ((fun (f : α →C_c β) ↦ f.toFun) g)
⊢ f = g
have obtain : ∀ (toFun : α → β) (continuous_toFun : Continuous toFun)
  (hasCompactSupport' : HasCompactSupport { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →C_c β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
      ((fun (f : α →C_c β) ↦ f.toFun) g)),
  { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } = g
Tactic: obtain ⟨⟨_, _⟩, _⟩ := f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
g : α →C_c β
toFun : α → β
continuous_toFun : Continuous toFun
hasCompactSupport' : HasCompactSupport { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun
h :
  Eq (α := (a : α) → β)
    ((fun (f : α →C_c β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
    ((fun (f : α →C_c β) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } = g
have obtain : ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
  (hasCompactSupport'_1 :
    HasCompactSupport { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun)
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : α →C_c β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' })
      ((fun (f : α →C_c β) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, hasCompactSupport' := hasCompactSupport' : α →C_c β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, hasCompactSupport' := hasCompactSupport'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous f'
have rw : Continuous.{u_2, u_3} (X := α) (Y := β) (⇑f : (a : α) → β)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
f : α →C_c β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ HasCompactSupport f'
have simp_rw : HasCompactSupport.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)
Tactic: simp_rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
⊢ HasCompactSupport
    (ContinuousMap.toFun (if Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ) then g.comp (↑f : C(α, β)) else 0))
have pos : ∀ (hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)),
  HasCompactSupport (ContinuousMap.toFun (g.comp (↑f : C(α, β))))
Tactic: split_ifs with hg
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Zero β
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
g : C(β, γ)
f : α →C_c β
pos :
  ∀ (hg : Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)),
    HasCompactSupport (ContinuousMap.toFun (g.comp (↑f : C(α, β))))
⊢ HasCompactSupport
    (ContinuousMap.toFun (if Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ) then g.comp (↑f : C(α, β)) else 0))
have neg : ∀ (hg : ¬Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) 0 : γ) (0 : γ)),
  HasCompactSupport.{u_2, u_5} (α := α) (β := γ) (ContinuousMap.toFun 0)
Tactic: split_ifs with hg
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
have this : IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
Tactic: have : IsCompact (Set.range f) := f.hasCompactSupport.isCompact_range f.continuous
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β_1
inst_2 : Zero β_1
γ : Type u_5
inst_3 : TopologicalSpace γ
inst_4 : Zero γ
β : Type u_6
inst_5 : PseudoMetricSpace β
inst_6 : Zero β
f : α →C_c β
this : IsCompact.{u_6} (X := β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
have rcases : ∀ (C : ℝ)
  (hC :
    ∀ ⦃x : β⦄,
      Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) x →
        ∀ ⦃y : β⦄, Membership.mem (γ := Set β) (Set.range.{u_6, u_2 + 1} (ι := α) (⇑f : (a : α) → β)) y → dist x y ≤ C),
  ∃ (C : ℝ), ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ≤ C
Tactic: rcases Metric.isBounded_iff.1 this.isBounded with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
⊢ (r • f) • g = r • f • g
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) (((r • f) • g : (a : α) → β) x : β) ((r • f • g : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
⊢ Eq.{u_3 + 1} (α := β) (((r • f) • g : (a : α) → β) x_1 : β) ((r • f • g : (a : α) → β) x_1 : β)
have h : HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: simp only [smul_eq_mul, coe_mul, coe_smul, Pi.mul_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h : HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h₁ : HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : IsScalarTower R β β
r : R
f g : α →C_c β
x_1 : α
h :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
h₁ :
  HSMul.hSMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
⊢ HMul.hMul (β := β) (HSMul.hSMul (β := β) r ((f : (a : α) → β) x_1 : β)) ((g : (a : α) → β) x_1 : β) =
    r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
have h₂ : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β)
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
⊢ r • f • g = f • r • g
have h : ∀ (x : α), Eq.{u_3 + 1} (α := β) ((r • f • g : (a : α) → β) x : β) ((f • r • g : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
⊢ Eq.{u_3 + 1} (α := β) ((r • f • g : (a : α) → β) x_1 : β) ((f • r • g : (a : α) → β) x_1 : β)
have h : r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: simp only [smul_eq_mul, coe_smul, coe_mul, Pi.smul_apply, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h₁ : r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
R : Type u_5
inst_2 : Semiring R
inst_3 : NonUnitalNonAssocSemiring β
inst_4 : IsTopologicalSemiring β
inst_5 : Module R β
inst_6 : ContinuousConstSMul R β
inst_7 : SMulCommClass R β β
r : R
f g : α →C_c β
x_1 : α
h :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
h₁ :
  r • HSMul.hSMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
⊢ r • HMul.hMul (α := β) (β := β) ((f : (a : α) → β) x_1 : β) ((g : (a : α) → β) x_1 : β) =
    HMul.hMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
have h₂ : HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β)) =
  HSMul.hSMul (α := β) ((f : (a : α) → β) x_1 : β) (HSMul.hSMul (β := β) r ((g : (a : α) → β) x_1 : β))
Tactic: rw [← smul_eq_mul, ← smul_eq_mul, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
⊢ Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)) x ↔
    Membership.mem (γ := Set α) (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (hypothesis)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
⊢ IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)))
have support_star : Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
  (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
Tactic: have support_star : (Function.support fun (x : α) => star (f x)) = Function.support f := by
          ext x
          simp only [Function.mem_support, ne_eq, star_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : AddMonoid β
inst_3 : StarAddMonoid β
inst_4 : ContinuousStar β
f : α →C_c β
support_star :
  Eq.{u_2 + 1} (α := Set α) (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x))
    (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β))
⊢ IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) fun (x : α) ↦ star ((f : (a : α) → β) x)))
have rw : IsCompact.{u_2} (X := α) (closure (Function.support.{u_2, u_3} (M := β) (⇑f : (a : α) → β)))
Tactic: rw [support_star]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeSup β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousSup β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(s.sup' H f) : (a : α) → β) (s.sup' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_3 + 1} (α := β) ((s.sup' H f : (a : α) → β) x : β) (s.sup' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SemilatticeInf β
inst_2 : Zero β
inst_3 : TopologicalSpace β
inst_4 : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
⊢ Eq (α := (a : α) → β) (⇑(s.inf' H f) : (a : α) → β) (s.inf' H fun (i : ι) ↦ (⇑(f i) : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_3 + 1} (α := β) ((s.inf' H f : (a : α) → β) x : β) (s.inf' H (fun (i : ι) ↦ (⇑(f i) : (a : α) → β)) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
δ : Type u_5
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C_c δ
g : β →co γ
⊢ HasCompactSupport (ContinuousMap.toFun (ContinuousMap.comp (↑f : C(γ, δ)) (↑g : C(β, γ))))
have apply : Subset.{u_3} (α := Set β)
  (tsupport.{u_3, u_5} (α := δ)
    (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
  ((⇑g : (a : β) → γ) ⁻¹' tsupport f.toFun)
Tactic: apply IsCompact.of_isClosed_subset (g.isCompact_preimage_of_isClosed f.2 (isClosed_tsupport _))
      (isClosed_tsupport (f ∘ g))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
δ : Type u_5
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C_c δ
g : β →co γ
x : β
hx :
  Membership.mem (γ := Set β)
    (tsupport.{u_3, u_5} (α := δ)
      (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    x
⊢ Membership.mem (γ := Set β) ((⇑g : (a : β) → γ) ⁻¹' tsupport f.toFun) x
have rw : ∀ (o : Set γ), IsOpen o → Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ) → (o ∩ Function.support f.toFun).Nonempty
Tactic: rw [tsupport, Set.mem_preimage, _root_.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CompactlySupported (goal)
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
δ : Type u_5
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
inst_4 : Zero δ
f : γ →C_c δ
g : β →co γ
x : β
hx :
  Membership.mem (γ := Set β)
    (tsupport.{u_3, u_5} (α := δ)
      (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ)))
    x
o : Set γ
ho : IsOpen o
hgxo : Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ)
⊢ (o ∩ Function.support f.toFun).Nonempty
have rw : ∀
  (hx :
    ∀ (o : Set β),
      IsOpen o →
        x ∈ o →
          (o ∩
              Function.support.{u_3, u_5} (M := δ)
                (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := γ) (⇑f : (a : γ) → δ) (⇑g : (a : β) → γ))).Nonempty)
  (o : Set γ) (ho : IsOpen o) (hgxo : Membership.mem (α := γ) o ((g : (a : β) → γ) x : γ)),
  (o ∩ Function.support f.toFun).Nonempty
Tactic: rw [tsupport, _root_.mem_closure_iff] at hx
Cleared hypotheses: hx, o, ho, hgxo