awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed[inst] (f i)
⊢ IsClosed[inst] (⋃ i ∈ s, f i)
have simp : ∀ (h : ∀ i ∈ s, IsOpen[inst] (f i)ᶜ), IsOpen[inst] (⋂ i ∈ s, (f i)ᶜ)
Tactic: simp only [← isOpen_compl_iff, compl_iUnion] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
inst_1 : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (s i)
⊢ IsClosed[inst] (⋃ (i : ι), s i)
have simp : ∀ (h : ∀ (i : ι), IsOpen[inst] (s i)ᶜ), IsOpen[inst] (⋂ (i : ι), (s i)ᶜ)
Tactic: simp only [← isOpen_compl_iff, compl_iUnion] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ (x : X), map g f ≤ 𝓝 x
⊢ f.limUnder g = Classical.choice hX
have simp_rw : (map g f).lim = Classical.choice hX
Tactic: simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ (x : X), map g f ≤ 𝓝 x
simp_rw : (map g f).lim = Classical.choice hX
⊢ f.limUnder g = Classical.choice hX
have simp_rw₁ : (Classical.epsilon fun (x : X) ↦ map g f ≤ 𝓝 x) = Classical.choice hX
Tactic: simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ (x : X), map g f ≤ 𝓝 x
simp_rw : (map g f).lim = Classical.choice hX
simp_rw₁ : (Classical.epsilon fun (x : X) ↦ map g f ≤ 𝓝 x) = Classical.choice hX
⊢ f.limUnder g = Classical.choice hX
have simp_rw₂ : (↑(Classical.strongIndefiniteDescription (fun (x : X) ↦ map g f ≤ 𝓝 x) hX) : X) = Classical.choice hX
Tactic: simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]
-- Lean 4 proof step from Mathlib.Topology.Basic (goal)
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ (x : X), map g f ≤ 𝓝 x
simp_rw : (map g f).lim = Classical.choice hX
simp_rw₁ : (Classical.epsilon fun (x : X) ↦ map g f ≤ 𝓝 x) = Classical.choice hX
simp_rw₂ : (↑(Classical.strongIndefiniteDescription (fun (x : X) ↦ map g f ≤ 𝓝 x) hX) : X) = Classical.choice hX
⊢ f.limUnder g = Classical.choice hX
have simp_rw₃ : (↑(if hp : ∃ (x : X), map g f ≤ 𝓝 x then
        Subtype.mk (p := fun (x : X) ↦ (∃ (y : X), map g f ≤ 𝓝 y) → map g f ≤ 𝓝 x)
          (↑(Classical.indefiniteDescription (fun (x : X) ↦ map g f ≤ 𝓝 x) hp) : X) sorry
      else Subtype.mk (p := fun (x : X) ↦ (∃ (y : X), map g f ≤ 𝓝 y) → map g f ≤ 𝓝 x) (Classical.choice hX) sorry) :
    X) =
  Classical.choice hX
Tactic: simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • (s₁ + s₂)
have rw : t₁ + t₂ ⊆ x • s₁ + x • s₂
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ HSMul.hSMul (β := Set α) a univ
have rw : s ⊆ univ
Tactic: rw [smul_set_univ₀ ha]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ c • s ↔ MapsTo (fun (x : α) ↦ c⁻¹ • x) t s
have rw : t ⊆ (fun (x : α) ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun (x : α) ↦ c⁻¹ • x) t s
Tactic: rw [← preimage_smul_inv₀ hc]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s t
have rw : Absorbs M s (⋃ x ∈ t, {x})
Tactic: rw [← Set.biUnion_of_singleton t]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) (x +ᵥ t)
have rw : Absorbs M (s₁ + s₂) (HVAdd.hVAdd (α := Set E) {x} t)
Tactic: rw [← singleton_vadd]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Absorbs (goal)
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid N
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : MulAction N α
inst_4 : IsScalarTower M N α
inst_5 : Bornology M
inst_6 : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun (x : M) ↦ HSMul.hSMul (β := N) x 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ HSMul.hSMul (β := N) x 1 • s
⊢ t ⊆ x • s
have rwa : ∀ (hx : t ⊆ x • s), t ⊆ x • s
Tactic: rwa [smul_one_smul N x s] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
⊢ t = t'
have mk : ∀ (cobounded : Filter α) (le_cofinite : cobounded ≤ cofinite)
  (h_cobounded : Bornology.cobounded α = Bornology.cobounded α),
  { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } = t'
Tactic: cases t
Cleared hypotheses: t, h_cobounded
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
t' : Bornology α
cobounded : Filter α
le_cofinite : cobounded ≤ cofinite
h_cobounded : Bornology.cobounded α = Bornology.cobounded α
⊢ { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } = t'
have mk : ∀ (cobounded_1 : Filter α) (le_cofinite_1 : cobounded_1 ≤ cofinite)
  (h_cobounded : Bornology.cobounded α = Bornology.cobounded α),
  { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } =
    { cobounded := cobounded_1, le_cofinite := le_cofinite_1 }
Tactic: cases t'
Cleared hypotheses: t', h_cobounded
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B
have rw : ∀ (sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b) (x : α), {x} ∈ B
Tactic: rw [sUnion_eq_univ_iff] at sUnion_univ
Cleared hypotheses: sUnion_univ, x
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
⊢ {x} ∈ B
have rcases : ∀ (s : Set α) (hs : s ∈ B) (hxs : x ∈ s), {x} ∈ B
Tactic: rcases sUnion_univ x with ⟨s, hs, hxs⟩
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
s : Set α
⊢ IsBounded sᶜ ↔ IsCobounded s
have rw : sᶜᶜ ∈ cobounded α ↔ IsCobounded s
Tactic: rw [isBounded_def, isCobounded_def, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
s : Set α
rw : sᶜᶜ ∈ cobounded α ↔ IsCobounded s
⊢ IsBounded sᶜ ↔ IsCobounded s
have rw₁ : sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α
Tactic: rw [isBounded_def, isCobounded_def, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
s : Set α
rw : sᶜᶜ ∈ cobounded α ↔ IsCobounded s
rw₁ : sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α
⊢ IsBounded sᶜ ↔ IsCobounded s
have rw₂ : s ∈ cobounded α ↔ s ∈ cobounded α
Tactic: rw [isBounded_def, isCobounded_def, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
⊢ IsBounded.{u_2} (α := α) ∅
have rw : univ ∈ cobounded α
Tactic: rw [isBounded_def, compl_empty]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s.Nonempty
have rw : s ≠ ∅
Tactic: rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
x : Bornology α
s : Set α
h : ∀ x_1 ∈ s, IsBounded s
⊢ IsBounded s
have inl : ∀ (h : ∀ (x_1 : α), Membership.mem (γ := Set α) ∅ x_1 → IsBounded.{u_2} (α := α) ∅), IsBounded.{u_2} (α := α) ∅
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)
have h : ∀ (h : comap f (cobounded β) ≤ cobounded α) (s : Set α) (hs : IsBounded s), IsBounded (f '' s)
Tactic: refine
    ⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
⊢ IsBounded (f '' s)
have obtain : ∀ (t : Set β) (ht : t ∈ cobounded β) (hts : f ⁻¹' t ⊆ sᶜ), IsBounded (f '' s)
Tactic: obtain ⟨t, ht, hts⟩ := h hs.compl
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ IsBounded (f '' s)
have hts₁ : s ⊆ f ⁻¹' tᶜ
Tactic: rw [subset_compl_comm, ← preimage_compl] at hts
Cleared hypotheses: hts
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B
have rw : sᶜ ∈ cobounded α ↔ s ∈ B
Tactic: rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
rw : sᶜ ∈ cobounded α ↔ s ∈ B
⊢ IsBounded s ↔ s ∈ B
have rw₁ : sᶜ ∈ comk (fun (x : Set α) ↦ x ∈ B) empty_mem subset_mem union_mem ↔ s ∈ B
Tactic: rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
rw : sᶜ ∈ cobounded α ↔ s ∈ B
rw₁ : sᶜ ∈ comk (fun (x : Set α) ↦ x ∈ B) empty_mem subset_mem union_mem ↔ s ∈ B
⊢ IsBounded s ↔ s ∈ B
have rw₂ : s ∈ B ↔ s ∈ B
Tactic: rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s
have rw : IsBounded.{u_2} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsBounded s
Tactic: rw [sUnion_eq_biUnion, isBounded_biUnion hs]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
S : Set (Set α)
hs : S.Finite
rw : IsBounded.{u_2} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsBounded s
⊢ IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s
have rw₁ : (∀ i ∈ S, IsBounded i) ↔ ∀ s ∈ S, IsBounded s
Tactic: rw [sUnion_eq_biUnion, isBounded_biUnion hs]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
inst_1 : Finite ι
s : ι → Set α
⊢ IsBounded.{u_2} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
have rw : IsBounded (⋃₀ range s) ↔ ∀ (i : ι), IsBounded (s i)
Tactic: rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
inst_1 : Finite ι
s : ι → Set α
rw : IsBounded (⋃₀ range s) ↔ ∀ (i : ι), IsBounded (s i)
⊢ IsBounded.{u_2} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
have rw₁ : (∀ s_1 ∈ range s, IsBounded s_1) ↔ ∀ (i : ι), IsBounded (s i)
Tactic: rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
inst_1 : Finite ι
s : ι → Set α
rw : IsBounded (⋃₀ range s) ↔ ∀ (i : ι), IsBounded (s i)
rw₁ : (∀ s_1 ∈ range s, IsBounded s_1) ↔ ∀ (i : ι), IsBounded (s i)
⊢ IsBounded.{u_2} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)
have rw₂ : (∀ (i : ι), IsBounded (s i)) ↔ ∀ (i : ι), IsBounded (s i)
Tactic: rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
⊢ cobounded α = ⊥ ↔ BoundedSpace α
have rw : cobounded α = ⊥ ↔ IsBounded.{u_2} (α := α) univ
Tactic: rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
rw : cobounded α = ⊥ ↔ IsBounded.{u_2} (α := α) univ
⊢ cobounded α = ⊥ ↔ BoundedSpace α
have rw₁ : cobounded α = ⊥ ↔ univᶜ ∈ cobounded α
Tactic: rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
rw : cobounded α = ⊥ ↔ IsBounded.{u_2} (α := α) univ
rw₁ : cobounded α = ⊥ ↔ univᶜ ∈ cobounded α
⊢ cobounded α = ⊥ ↔ BoundedSpace α
have rw₂ : cobounded α = ⊥ ↔ ∅ ∈ cobounded α
Tactic: rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Basic (goal)
Goal:
α : Type u_2
inst : Bornology α
rw : cobounded α = ⊥ ↔ IsBounded.{u_2} (α := α) univ
rw₁ : cobounded α = ⊥ ↔ univᶜ ∈ cobounded α
rw₂ : cobounded α = ⊥ ↔ ∅ ∈ cobounded α
⊢ cobounded α = ⊥ ↔ BoundedSpace α
have rw₃ : cobounded α = ⊥ ↔ cobounded α = ⊥
Tactic: rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
X : Type u_2
inst : PseudoMetricSpace R
inst_1 : Sub R
inst_2 : BoundedSub R
f g : X → R
f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
have obtain : ∀ (C : ℝ) (hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C),
  ∃ (C : ℝ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
Tactic: obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <|
    isBounded_sub (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
X : Type u_2
inst : PseudoMetricSpace R
inst_1 : Sub R
inst_2 : BoundedSub R
f g : X → R
f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
have h : ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
Tactic: use C
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_1
inst : PseudoMetricSpace R
inst_1 : Sub R
K : ℝ≥0
lip : LipschitzWith (β := R) K fun (p : R × R) ↦ p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
⊢ Bornology.IsBounded (s - t)
have bdd : Bornology.IsBounded (s ×ˢ t)
Tactic: have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : PseudoMetricSpace R
inst_1 : Sub R
K : ℝ≥0
lip : LipschitzWith (β := R) K fun (p : R × R) ↦ p.1 - p.2
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ Bornology.IsBounded (s - t)
have h : s - t = (fun (p : R × R) ↦ p.1 - p.2) '' s ×ˢ t
Tactic: convert! lip.isBounded_image bdd
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
have pos : ∀ (s_empty : s = ∅), Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
Tactic: by_cases s_empty : s = ∅
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
pos : ∀ (s_empty : s = ∅), Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
have neg : ∀ (s_empty : ¬s = ∅), Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
Tactic: by_cases s_empty : s = ∅
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : ¬s = ∅
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
have s_empty₁ : s.Nonempty
Tactic: simp_rw [← nonempty_iff_ne_empty] at s_empty
Cleared hypotheses: s_empty
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
x : R
hx : Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ (n + 1)) '' s) x
⊢ x ∈ (fun (x : R) ↦ x ^ n) '' s * s
have hx₁ : ∃ x_1 ∈ s, x_1 ^ (n + 1) = x
Tactic: simp only [mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
x : R
hx : ∃ x_1 ∈ s, x_1 ^ (n + 1) = x
⊢ x ∈ (fun (x : R) ↦ x ^ n) '' s * s
have obtain : ∀ (y : R) (y_in_s : y ∈ s) (ypow_eq_x : y ^ (n + 1) = x), x ∈ (fun (x : R) ↦ x ^ n) '' s * s
Tactic: obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ x ∈ (fun (x : R) ↦ x ^ n) '' s * s
have rw : y ^ n * y ∈ (fun (x : R) ↦ x ^ n) '' s * s
Tactic: rw [← ypow_eq_x, pow_succ y n]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
⊢ y ^ n * y ∈ (fun (x : R) ↦ x ^ n) '' s * s
have apply : Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' s) (y ^ n)
Tactic: apply Set.mul_mem_mul _ y_in_s
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
x y : R
y_in_s : y ∈ s
ypow_eq_x : y ^ (n + 1) = x
w : R
⊢ Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' s) (y ^ n)
have h : y ∈ s ∧ (fun (x : R) ↦ x ^ n) y = y ^ n
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ (n + 1)) '' s)
have obs : (fun (x : R) ↦ x ^ (n + 1)) '' s ⊆ (fun (x : R) ↦ x ^ n) '' s * s
Tactic: have obs : ((fun x ↦ x ^ (n + 1)) '' s) ⊆ ((fun x ↦ x ^ n) '' s) * s := by
      intro x hx
      simp only [mem_image] at hx
      obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
      rw [← ypow_eq_x, pow_succ y n]
      apply Set.mul_mem_mul _ y_in_s
      use y
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
have zero : Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
Tactic: induction n with
  | zero =>
    by_cases s_empty : s = ∅
    · simp [s_empty]
    simp_rw [← nonempty_iff_ne_empty] at s_empty
    simp [s_empty]
  | succ n hn =>
    have obs : ((fun x ↦ x ^ (n + 1)) '' s) ⊆ ((fun x ↦ x ^ n) '' s) * s := by
      intro x hx
      simp only [mem_image] at hx
      obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
      rw [← ypow_eq_x, pow_succ y n]
      apply Set.mul_mem_mul _ y_in_s
      use y
    exact (isBounded_mul hn s_bdd).subset obs
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_2
inst : Bornology R
inst_1 : Monoid R
inst_2 : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
n : ℕ
zero : Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)
have succ : ∀ (n : ℕ) (hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)),
  Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ (n + 1)) '' s)
Tactic: induction n with
  | zero =>
    by_cases s_empty : s = ∅
    · simp [s_empty]
    simp_rw [← nonempty_iff_ne_empty] at s_empty
    simp [s_empty]
  | succ n hn =>
    have obs : ((fun x ↦ x ^ (n + 1)) '' s) ⊆ ((fun x ↦ x ^ n) '' s) * s := by
      intro x hx
      simp only [mem_image] at hx
      obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
      rw [← ypow_eq_x, pow_succ y n]
      apply Set.mul_mem_mul _ y_in_s
      use y
    exact (isBounded_mul hn s_bdd).subset obs
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
X : Type u_2
inst : PseudoMetricSpace R
inst_1 : Mul R
inst_2 : BoundedMul R
f g : X → R
f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
have obtain : ∀ (C : ℝ) (hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C),
  ∃ (C : ℝ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
Tactic: obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <|
    isBounded_mul (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
X : Type u_2
inst : PseudoMetricSpace R
inst_1 : Mul R
inst_2 : BoundedMul R
f g : X → R
f_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (f x) (f y) ≤ C
g_bdd : ∃ (C : ℝ), ∀ (x y : X), dist (g x) (g y) ≤ C
C : ℝ
hC : ∀ ⦃x : R⦄, x ∈ range f * range g → ∀ ⦃y : R⦄, y ∈ range f * range g → dist x y ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
have h : ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
Tactic: use C
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_1
inst : PseudoMetricSpace R
inst_1 : Monoid R
inst_2 : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
⊢ Bornology.IsBounded (s * t)
have bdd : Bornology.IsBounded (s ×ˢ t)
Tactic: have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd