awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
⊢ Bornology.IsBounded (s * t)
have obtain : ∀ (C : ℝ≥0) (mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2), Bornology.IsBounded (s * t)
Tactic: obtain ⟨C, mul_lip⟩ := ‹LipschitzMul R›.lipschitz_mul
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2
⊢ Bornology.IsBounded (s * t)
have h : s * t = (fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t
Tactic: convert! mul_lip.isBounded_image bdd
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2
⊢ s * t = (fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t
have h : ∀ (p : R), p ∈ s * t ↔ Membership.mem (γ := Set R) ((fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2
p : R
⊢ p ∈ s * t ↔ Membership.mem (γ := Set R) ((fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t) p
have h : p ∈ s * t ↔ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p
Tactic: simp only [Set.mem_image, Set.mem_prod, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2
p : R
⊢ p ∈ s * t ↔ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p
have h : p ∈ s * t → ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
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
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2
p : R
h : p ∈ s * t → ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p
⊢ p ∈ s * t ↔ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p
have h₁ : (∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p) → p ∈ s * t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
⊢ LipschitzWith (β := R) 2 fun (p : R × R) ↦ p.1 - p.2
have h : 2 = HAdd.hAdd (α := ℝ≥0) 1 1
Tactic: convert! LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
⊢ Membership.mem (γ := Filter R) (map (fun (x_1 : R) ↦ x_1 + x) (cobounded R)) s
have rw : (fun (x_1 : R) ↦ x_1 + x) ⁻¹' s ∈ cobounded R
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
⊢ (fun (x_1 : R) ↦ x_1 + x) ⁻¹' s ∈ cobounded R
have rw : ∀ (hs : Bornology.IsBounded sᶜ), Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' s)ᶜ
Tactic: rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' s)ᶜ
have rw : Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ)
Tactic: rw [← Set.preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ)
have h : (fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ = sᶜ - {x}
Tactic: convert! isBounded_sub hs (t := { x }) isBounded_singleton using 1
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ (fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ = sᶜ - {x}
have h : ∀ (y : R), Membership.mem (γ := Set R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ) y ↔ y ∈ sᶜ - {x}
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
⊢ Membership.mem (γ := Filter R) (map (fun (x_1 : R) ↦ x + x_1) (cobounded R)) s
have rw : (fun (x_1 : R) ↦ x + x_1) ⁻¹' s ∈ cobounded R
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
⊢ (fun (x_1 : R) ↦ x + x_1) ⁻¹' s ∈ cobounded R
have rw : ∀ (hs : Bornology.IsBounded sᶜ), Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' s)ᶜ
Tactic: rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' s)ᶜ
have rw : Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ)
Tactic: rw [← Set.preimage_compl]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ)
have h : (fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ = {-x} + sᶜ
Tactic: convert! isBounded_add isBounded_singleton (s := {-x}) hs using 1
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ (fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ = {-x} + sᶜ
have h : ∀ (y : R), Membership.mem (γ := Set R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ) y ↔ y ∈ {-x} + sᶜ
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
⊢ Bornology.IsBounded (s * t)
have obtain : ∀ (Af : ℝ) (hAf : s ⊆ Metric.closedBall 0 Af), Bornology.IsBounded (s * t)
Tactic: obtain ⟨Af, hAf⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp hs
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
⊢ Bornology.IsBounded (s * t)
have obtain : ∀ (Ag : ℝ) (hAg : t ⊆ Metric.closedBall 0 Ag), Bornology.IsBounded (s * t)
Tactic: obtain ⟨Ag, hAg⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp ht
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
⊢ Bornology.IsBounded (s * t)
have rw : ∀ (hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C)
  (ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C) (Af : ℝ) (hAf : s ⊆ Metric.closedBall 0 Af)
  (Ag : ℝ) (hAg : t ⊆ Metric.closedBall 0 Ag), ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ C
Tactic: rw [Metric.isBounded_iff] at hs ht ⊢
Cleared hypotheses: hs, ht, Af, hAf, Ag, hAg
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
⊢ ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ C
have h : ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ 2 * Af * Ag
Tactic: use 2 * Af * Ag
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
⊢ dist z w ≤ 2 * Af * Ag
have h : ∀ (x₁ : R) (hx₁ : x₁ ∈ s) (y₁ : R) (hy₁ : y₁ ∈ t) (z_eq : x₁ * y₁ = z), dist z w ≤ 2 * Af * Ag
Tactic: obtain ⟨x₁, hx₁, y₁, hy₁, z_eq⟩ := Set.mem_mul.mp hz
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
⊢ dist z w ≤ 2 * Af * Ag
have h : ∀ (x₂ : R) (hx₂ : x₂ ∈ s) (y₂ : R) (hy₂ : y₂ ∈ t) (w_eq : x₂ * y₂ = w), dist z w ≤ 2 * Af * Ag
Tactic: obtain ⟨x₂, hx₂, y₂, hy₂, w_eq⟩ := Set.mem_mul.mp hw
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ dist z w ≤ 2 * Af * Ag
have h : ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
Tactic: rw [← w_eq, ← z_eq, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
have hAf' : 0 ≤ Af
Tactic: have hAf' : 0 ≤ Af := Metric.nonempty_closedBall.mp ⟨_, hAf hx₁⟩
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
x y : R
x_in_s : x ∈ s
y_in_t : y ∈ t
⊢ ‖x * y‖ ≤ Af * Ag
have apply : ‖x‖ ≤ Af
Tactic: apply (norm_mul_le _ _).trans (mul_le_mul _ _ (norm_nonneg _) hAf')
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
x y : R
x_in_s : x ∈ s
y_in_t : y ∈ t
apply : ‖x‖ ≤ Af
⊢ ‖x * y‖ ≤ Af * Ag
have apply₁ : ‖y‖ ≤ Ag
Tactic: apply (norm_mul_le _ _).trans (mul_le_mul _ _ (norm_nonneg _) hAf')
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
have aux : ∀ {x y : R}, x ∈ s → y ∈ t → ‖x * y‖ ≤ Af * Ag
Tactic: have aux : ∀ {x y}, x ∈ s → y ∈ t → ‖x * y‖ ≤ Af * Ag := by
      intro x y x_in_s y_in_t
      apply (norm_mul_le _ _).trans (mul_le_mul _ _ (norm_nonneg _) hAf')
      · exact mem_closedBall_zero_iff.mp (hAf x_in_s)
      · exact mem_closedBall_zero_iff.mp (hAg y_in_t)
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
hz : z ∈ s * t
w : R
hw : w ∈ s * t
x₁ : R
hx₁ : x₁ ∈ s
y₁ : R
hy₁ : y₁ ∈ t
z_eq : x₁ * y₁ = z
x₂ : R
hx₂ : x₂ ∈ s
y₂ : R
hy₂ : y₂ ∈ t
w_eq : x₂ * y₂ = w
hAf' : 0 ≤ Af
aux : ∀ {x y : R}, x ∈ s → y ∈ t → ‖x * y‖ ≤ Af * Ag
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
have calc : Af * Ag + Af * Ag = 2 * Af * Ag
Tactic: calc ‖x₁ * y₁ - x₂ * y₂‖
     _ ≤ ‖x₁ * y₁‖ + ‖x₂ * y₂‖ := norm_sub_le _ _
     _ ≤ Af * Ag + Af * Ag     := add_le_add (aux hx₁ hy₁) (aux hx₂ hy₂)
     _ = 2 * Af * Ag           := by simp [← two_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
⊢ Bornology.IsBounded (s * t)
have obtain : ∀ (Af : ℝ) (hAf : s ⊆ closedBall 0 Af), Bornology.IsBounded (s * t)
Tactic: obtain ⟨Af, hAf⟩ := (isBounded_iff_subset_closedBall 0).mp hs
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
⊢ Bornology.IsBounded (s * t)
have obtain : ∀ (Ag : ℝ) (hAg : t ⊆ closedBall 0 Ag), Bornology.IsBounded (s * t)
Tactic: obtain ⟨Ag, hAg⟩ := (isBounded_iff_subset_closedBall 0).mp ht
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (hypothesis)
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
⊢ Bornology.IsBounded (s * t)
have key : IsCompact (SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag))
Tactic: have key : IsCompact (closedBall (0 : ℝ≥0) Af ×ˢ closedBall (0 : ℝ≥0) Ag) :=
      IsCompact.prod (isCompact_closedBall _ _) (isCompact_closedBall _ _)
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag))
⊢ Bornology.IsBounded (s * t)
have apply : s * t ⊆
  (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 * p.2) '' SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag)
Tactic: apply Bornology.IsBounded.subset (key.image continuous_mul).isBounded
-- Lean 4 proof step from Mathlib.Topology.Bornology.BoundedOperation (goal)
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag))
a : ℝ≥0
⊢ a ∈ s * t →
    Membership.mem (γ := Set ℝ≥0)
      ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 * p.2) ''
        SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag))
      a
have this : ∀ (x : ℝ≥0) (x_in_s : x ∈ s) (y : ℝ≥0) (y_in_t : y ∈ t) (xy_eq : (fun (x1 x2 : ℝ≥0) ↦ x1 * x2) x y = a),
  Membership.mem (γ := Set ℝ≥0)
    ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 * p.2) '' SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag))
    a
Tactic: ⟨x, x_in_s, y, y_in_t, xy_eq⟩
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
have inl : IsBounded (SProd.sprod (α := Set α) ∅ t) ↔
  Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ t = ∅ ∨ IsBounded.{u_1} (α := α) ∅ ∧ IsBounded t
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
inl :
  IsBounded (SProd.sprod (α := Set α) ∅ t) ↔
    Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ t = ∅ ∨ IsBounded.{u_1} (α := α) ∅ ∧ IsBounded t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
have inr : ∀ (hs : s.Nonempty), IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
have inr : IsBounded (SProd.sprod (β := Set β) s ∅) ↔
  s = ∅ ∨ Eq.{u_2 + 1} (α := Set β) ∅ ∅ ∨ IsBounded s ∧ IsBounded.{u_2} (α := β) ∅
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
inr :
  IsBounded (SProd.sprod (β := Set β) s ∅) ↔
    s = ∅ ∨ Eq.{u_2 + 1} (α := Set β) ∅ ∅ ∨ IsBounded s ∧ IsBounded.{u_2} (α := β) ∅
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
have inr₁ : ∀ (ht : t.Nonempty), IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Tactic: rcases t.eq_empty_or_nonempty with (rfl | ht)
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
inst : Bornology α
s : Set α
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
have inl : IsBounded (SProd.sprod (α := Set α) (β := Set α) ∅ ∅) ↔ IsBounded.{u_1} (α := α) ∅
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
inst : Bornology α
s : Set α
inl : IsBounded (SProd.sprod (α := Set α) (β := Set α) ∅ ∅) ↔ IsBounded.{u_1} (α := α) ∅
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
have inr : ∀ (hs : s.Nonempty), IsBounded (s ×ˢ s) ↔ IsBounded s
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
have pos : ∀ (hne : ∃ (i : ι), S i = ∅), IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
Tactic: by_cases hne : ∃ i, S i = ∅
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
pos :
  ∀ (hne : ∃ (i : ι), S i = ∅), IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
have neg : ∀ (hne : ¬∃ (i : ι), S i = ∅), IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
Tactic: by_cases hne : ∃ i, S i = ∅
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ (i : ι), S i = ∅
⊢ IsBounded (Set.pi (α := X) univ S) ↔ (∃ (i : ι), S i = ∅) ∨ ∀ (i : ι), IsBounded (S i)
have neg : IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)
Tactic: simp only [hne, false_or]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (hypothesis)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → Bornology (X i)
S : (i : ι) → Set (X i)
hne : ¬∃ (i : ι), S i = ∅
⊢ IsBounded (Set.pi (α := X) univ S) ↔ ∀ (i : ι), IsBounded (S i)
have hne₁ : (Set.pi (α := X) univ S).Nonempty
Tactic: simp only [not_exists, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Bornology β
f : α → β
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)
have rw : Bornology.IsBounded.{u_5} (α := α) univ ↔ Bornology.IsBounded (range f)
Tactic: rw [← @isBounded_univ, isBounded_induced, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Bornology β
f : α → β
rw : Bornology.IsBounded.{u_5} (α := α) univ ↔ Bornology.IsBounded (range f)
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)
have rw₁ : Bornology.IsBounded (f '' univ) ↔ Bornology.IsBounded (range f)
Tactic: rw [← @isBounded_univ, isBounded_induced, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_5
β : Type u_6
inst : Bornology β
f : α → β
rw : Bornology.IsBounded.{u_5} (α := α) univ ↔ Bornology.IsBounded (range f)
rw₁ : Bornology.IsBounded (f '' univ) ↔ Bornology.IsBounded (range f)
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)
have rw₂ : Bornology.IsBounded (range f) ↔ Bornology.IsBounded (range f)
Tactic: rw [← @isBounded_univ, isBounded_induced, image_univ]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
inst : Bornology α
p : α → Prop
⊢ BoundedSpace.{u_1} (Subtype p) ↔ Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
have rw : Bornology.IsBounded.{u_1} (α := α) (range (ι := Subtype p) (Subtype.val (p := p))) ↔
  Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
Tactic: rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.Topology.Bornology.Constructions (goal)
Goal:
α : Type u_1
inst : Bornology α
p : α → Prop
rw :
  Bornology.IsBounded.{u_1} (α := α) (range (ι := Subtype p) (Subtype.val (p := p))) ↔
    Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
⊢ BoundedSpace.{u_1} (Subtype p) ↔ Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
have rw₁ : Bornology.IsBounded.{u_1} (α := α) {x : α | p x} ↔ Bornology.IsBounded.{u_1} (α := α) {x : α | p x}
Tactic: rw [boundedSpace_induced_iff, Subtype.range_coe_subtype]