awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact norm_lt_iff_of_compactlySupported h hM

Premises used: norm_lt_iff_of_compactlySupported
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h_1 : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
hM : M ≤ 0
h : ‖f‖ < M
⊢ 0 ≤ ‖f‖

Tactic:
positivity
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h_1 : Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) f
M : ℝ
hM : M ≤ 0
h : ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M
⊢ 0 ≤ norm.{u_2} (E := γ) ((f : (a : α) → γ) (Classical.arbitrary α) : γ)

Tactic:
positivity
-- 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 : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), norm.{u_2} (E := γ) ((f : (a : α) → γ) x : γ) < M

Tactic:
exact ⟨fun h ↦ False.elim <| (h.trans_le hM).not_ge (by positivity),
      fun h ↦ False.elim <| (h (Classical.arbitrary α) |>.trans_le hM).not_ge (by positivity)⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
h : IsCompact.{u_1} (X := α) univ
⊢ Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤

Tactic:
eq_top_iff.mpr fun _ _ ↦ h.of_isClosed_subset (isClosed_tsupport _) (subset_univ _)

Premises used: Iff.mpr, eq_top_iff, Set.subset_univ, HSub.hSub, tsupport, isClosed_tsupport, IsCompact.of_isClosed_subset, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : CompactSpace α
⊢ Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤

Tactic:
compactlySupported_eq_top_of_isCompact CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ, compactlySupported_eq_top_of_isCompact
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
⊢ Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤ ↔ IsCompact.{u_1} (X := α) univ

Tactic:
⟨fun h ↦ ?_, compactlySupported_eq_top_of_isCompact⟩

Premises used: compactlySupported_eq_top_of_isCompact, Iff.intro
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
refine : ∀ (h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤), IsCompact.{u_1} (X := α) univ
⊢ Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤ ↔ IsCompact.{u_1} (X := α) univ

Tactic:
refine ⟨fun h ↦ ?_, compactlySupported_eq_top_of_isCompact⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤
obtain : ∀ (x : γ) (hx : x ≠ 0), IsCompact.{u_1} (X := α) univ
⊢ IsCompact.{u_1} (X := α) univ

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : γ)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤
x : γ
hx : x ≠ 0
⊢ Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) (const α x)

Tactic:
simp [h]
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
inst_2 : Nontrivial γ
h : Eq (α := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) ⊤
x : γ
hx : x ≠ 0
⊢ IsCompact.{u_1} (X := α) univ

Tactic:
simpa [tsupport, Function.support_const hx]
    using (mem_compactlySupported (f := const α x).mp (by simp [h])).isCompact

Premises used: tsupport, mem_compactlySupported, HasCompactSupport.isCompact, Iff.mp, Function.support_const
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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
inr : ∀ (hs : (tsupport g).Nonempty), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty

Premises used: tsupport, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∀ (x y : α), dist (g x) (g y) ≤ 0

Tactic:
simp [tsupport_eq_empty_iff.mp hs]

Premises used: Iff.mp, tsupport_eq_empty_iff
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
exact ⟨0, by simp [tsupport_eq_empty_iff.mp hs]⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
inr :
  ∀ z ∈ tsupport g,
    ∀ (hmax : IsMaxOn (β := ℝ) (fun (x : α) ↦ ‖g x‖) (tsupport g) z), ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
obtain ⟨z, _, hmax⟩ := hg₂.exists_isMaxOn hs <| hg₁.norm.continuousOn

Premises used: Continuous.continuousOn, Continuous.norm, IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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

Tactic:
⟨2 * ‖g z‖, dist_le_two_norm' fun x ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, Exists.intro, OfNat.ofNat, BoundedContinuousFunction.dist_le_two_norm'
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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
inr : ∀ (x : α), ‖g x‖ ≤ ‖g z‖
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
refine ⟨2 * ‖g z‖, dist_le_two_norm' fun x ↦ ?_⟩
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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‖
neg : ∀ (hx : x ∉ tsupport g), ‖g x‖ ≤ ‖g z‖
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
by_cases hx : x ∈ tsupport g

Premises used: tsupport
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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 : α
hx : x ∈ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
isMaxOn_iff.mp hmax x hx

Premises used: isMaxOn_iff, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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 : α
hx : x ∈ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
exact isMaxOn_iff.mp hmax x hx

Premises used: isMaxOn_iff, Iff.mp
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
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 : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

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 γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
⊢ Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ) (ofCompactSupport g hg₁ hg₂)

Tactic:
mem_compactlySupported.mpr hg₂

Premises used: Iff.mpr, mem_compactlySupported
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
apply :
  HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑(ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) ⋯ ⋯) :
      (a : α) → γ)
⊢ Membership.mem (γ := TwoSidedIdeal (α →ᵇ γ)) C_cb(α, γ)
    (ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) ⋯ ⋯)

Tactic:
apply mem_compactlySupported.mpr

Premises used: Iff.mpr, mem_compactlySupported
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
rw :
  HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑{ toFun := HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ), continuous_toFun := ⋯,
          map_bounded' := ⋯ : α →ᵇ γ } :
      (a : α) → γ)
⊢ HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑(ofCompactSupport (HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ)) ⋯ ⋯) :
      (a : α) → γ)

Tactic:
rw [ofCompactSupport]

Premises used: ofCompactSupport
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑{ toFun := HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ), continuous_toFun := ⋯,
          map_bounded' := ⋯ : α →ᵇ γ } :
      (a : α) → γ)

Tactic:
HasCompactSupport.mul_left <| mem_compactlySupported.mp f.2

Premises used: mem_compactlySupported, HasCompactSupport.mul_left, Iff.mp, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : NonUnitalNormedRing γ
g : C(α, γ)
f : ↥C_cb(α, γ)
⊢ HasCompactSupport.{u_1, u_2} (α := α) (β := γ)
    (⇑{ toFun := HMul.hMul (α := (a : α) → γ) (⇑g : (a : α) → γ) (⇑(↑f : α →ᵇ γ) : (a : α) → γ), continuous_toFun := ⋯,
          map_bounded' := ⋯ : α →ᵇ γ } :
      (a : α) → γ)

Tactic:
exact HasCompactSupport.mul_left <| mem_compactlySupported.mp f.2

Premises used: mem_compactlySupported, HasCompactSupport.mul_left, Iff.mp, Subtype.property
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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)
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
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
g : CocompactMap α β
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)
obtain :
  ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
    (cocompact_tendsto'_1 :
      Tendsto { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : 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)
          { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 })),
    { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
        CocompactMap α β } =
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 }
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
      CocompactMap α β } =
    g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := g
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
toFun : α → β
continuous_toFun : Continuous toFun
cocompact_tendsto' :
  Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (cocompact β)
toFun_1 : α → β
continuous_toFun_1 : Continuous toFun_1
cocompact_tendsto'_1 :
  Tendsto { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : 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)
      { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 })
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
      CocompactMap α β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
⊢ Eq (α := (a : α) → β) (⇑f.toContinuousMap : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : CocompactMap α β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
rw : Continuous.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)
⊢ Continuous f'

Tactic:
rw [h]
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
f.continuous_toFun

Premises used: ContinuousMap.continuous_toFun, CocompactMap.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
exact f.continuous_toFun

Premises used: ContinuousMap.continuous_toFun, CocompactMap.toContinuousMap
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
simp_rw : Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)
⊢ Tendsto f' (cocompact α) (cocompact β)

Tactic:
simp_rw [h]
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)

Tactic:
f.cocompact_tendsto'

Premises used: CocompactMap.cocompact_tendsto'
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)

Tactic:
exact f.cocompact_tendsto'

Premises used: CocompactMap.cocompact_tendsto'
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
h : Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)
⊢ Eq (α := (a : α) → β) (⇑{ toContinuousMap := f, cocompact_tendsto' := h : CocompactMap α β } : (a : α) → β)
    (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := (a : α) → α) (⇑(CocompactMap.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : CocompactMap β γ
g : CocompactMap α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : CocompactMap β γ
g : CocompactMap α β
a : α
⊢ Eq.{u_3 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
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 : CocompactMap γ δ
g : CocompactMap β γ
h : CocompactMap α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: ContinuousMap.comp, CocompactMap.comp, rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
⊢ comp (CocompactMap.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: CocompactMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
⊢ f.comp (CocompactMap.id α) = f

Tactic:
ext fun _ => rfl

Premises used: CocompactMap.ext, rfl
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)
s : Set β
hs : s ∈ cocompact β
t : Set β
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ (f ⁻¹' t)ᶜ ⊆ f ⁻¹' s

Tactic:
simpa using preimage_mono hts

Premises used: Set.preimage_mono
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
⊢ ((⇑f : (a : α) → β) ⁻¹' s)ᶜ ∈ cocompact α

Tactic:
simpa only [preimage_image_preimage, preimage_compl] using
          mem_map.mp
            (cocompact_tendsto f <|
              mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)

Premises used: Iff.mpr, CocompactMapClass.cocompact_tendsto, Set.compl_subset_compl, And.intro, Set.image_preimage_subset, Exists.intro, Iff.mp, Set.preimage_compl, DFunLike.coe, Filter.mem_map, Set.preimage_image_preimage, Filter.mem_cocompact
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
obtain :
  ∀ (t : Set α) (ht : IsCompact t) (hts : ((⇑f : (a : α) → β) ⁻¹' s)ᶜᶜ ⊆ t),
    IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)

Tactic:
obtain ⟨t, ht, hts⟩ :=
    mem_cocompact'.mp
      (by
        simpa only [preimage_image_preimage, preimage_compl] using
          mem_map.mp
            (cocompact_tendsto f <|
              mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))

Premises used: Iff.mp, Filter.mem_cocompact'
-- Module: Mathlib.Topology.ContinuousMap.CocompactMap
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
t : Set α
ht : IsCompact t
hts : ((⇑f : (a : α) → β) ⁻¹' s)ᶜᶜ ⊆ t
⊢ (⇑f : (a : α) → β) ⁻¹' s ⊆ t

Tactic:
simpa using hts