awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
rw : Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ)
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' s)ᶜ

Tactic:
rw [← Set.preimage_compl]

Premises used: Set.preimage_compl
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded ({-x} + sᶜ)

Tactic:
isBounded_add isBounded_singleton (s := {-x}) hs

Premises used: isBounded_add, Bornology.isBounded_singleton
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
h : (fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ = {-x} + sᶜ
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ)

Tactic:
convert! isBounded_add isBounded_singleton (s := {-x}) hs using 1

Premises used: isBounded_add, Bornology.isBounded_singleton
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
h : ∀ (y : R), Membership.mem (γ := Set R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ) y ↔ y ∈ {-x} + sᶜ
⊢ (fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ = {-x} + sᶜ

Tactic:
ext y
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
y : R
⊢ Membership.mem (γ := Set R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' sᶜ) y ↔ y ∈ {-x} + sᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun (x_1 : R) ↦ x_1 - x) (cobounded R) (cobounded R)

Tactic:
simpa only [sub_eq_add_neg] using tendsto_add_const_cobounded (-x)

Premises used: sub_eq_add_neg, tendsto_add_const_cobounded, Neg.neg
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun (x_1 : R) ↦ x - x_1) (cobounded R) (cobounded R)

Tactic:
simpa only [sub_eq_add_neg] using (tendsto_const_add_cobounded x).comp tendsto_neg_cobounded

Premises used: tendsto_const_add_cobounded, sub_eq_add_neg, Filter.Tendsto.comp, Filter.tendsto_neg_cobounded
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : NonUnitalSeminormedRing R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
obtain : ∀ (Af : ℝ) (hAf : s ⊆ Metric.closedBall 0 Af), Bornology.IsBounded (s * t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨Af, hAf⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp hs

Premises used: Iff.mp, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
obtain : ∀ (Ag : ℝ) (hAg : t ⊆ Metric.closedBall 0 Ag), Bornology.IsBounded (s * t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨Ag, hAg⟩ := (Metric.isBounded_iff_subset_closedBall 0).mp ht

Premises used: Iff.mp, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
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
⊢ Bornology.IsBounded (s * t)

Tactic:
rw [Metric.isBounded_iff] at hs ht ⊢

Premises used: Metric.isBounded_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ 2 * Af * Ag
⊢ ∃ (C : ℝ), ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ C

Tactic:
use 2 * Af * Ag
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ (x₁ : R) (hx₁ : x₁ ∈ s) (y₁ : R) (hy₁ : y₁ ∈ t) (z_eq : x₁ * y₁ = z), dist z w ≤ 2 * Af * Ag
⊢ dist z w ≤ 2 * Af * Ag

Tactic:
obtain ⟨x₁, hx₁, y₁, hy₁, z_eq⟩ := Set.mem_mul.mp hz

Premises used: Iff.mp, Set.mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ (x₂ : R) (hx₂ : x₂ ∈ s) (y₂ : R) (hy₂ : y₂ ∈ t) (w_eq : x₂ * y₂ = w), dist z w ≤ 2 * Af * Ag
⊢ dist z w ≤ 2 * Af * Ag

Tactic:
obtain ⟨x₂, hx₂, y₂, hy₂, w_eq⟩ := Set.mem_mul.mp hw

Premises used: Iff.mp, Set.mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ‖x₁ * y₁ - x₂ * y₂‖ ≤ 2 * Af * Ag
⊢ dist z w ≤ 2 * Af * Ag

Tactic:
rw [← w_eq, ← z_eq, dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
⊢ 0 ≤ Af

Tactic:
have hAf' : 0 ≤ Af := Metric.nonempty_closedBall.mp ⟨_, hAf hx₁⟩
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
apply₁ : ‖y‖ ≤ Ag
⊢ ‖x * y‖ ≤ Af * Ag

Tactic:
apply (norm_mul_le _ _).trans (mul_le_mul _ _ (norm_nonneg _) hAf')

Premises used: mul_le_mul, LE.le.trans, norm_mul_le
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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‖ ≤ Af

Tactic:
mem_closedBall_zero_iff.mp (hAf x_in_s)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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‖ ≤ Af

Tactic:
exact mem_closedBall_zero_iff.mp (hAf x_in_s)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
⊢ ‖y‖ ≤ Ag

Tactic:
mem_closedBall_zero_iff.mp (hAg y_in_t)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
⊢ ‖y‖ ≤ Ag

Tactic:
exact mem_closedBall_zero_iff.mp (hAg y_in_t)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 ∈ 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)
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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₂‖ ≤ ‖x₁ * y₁‖ + ‖x₂ * y₂‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_le
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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₂‖ ≤ Af * Ag + Af * Ag

Tactic:
add_le_add (aux hx₁ hy₁) (aux hx₂ hy₂)

Premises used: add_le_add
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
⊢ Af * Ag + Af * Ag = 2 * Af * Ag

Tactic:
simp [← two_mul, mul_assoc]

Premises used: mul_assoc, two_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
calc : Af * Ag + Af * Ag = 2 * Af * Ag
⊢ ‖x₁ * y₁ - x₂ * y₂‖ ≤ 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]

Premises used: norm_sub_le, add_le_add
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
⊢ BoundedSub ℝ≥0

Tactic:
boundedSub_of_lipschitzWith_sub NNReal.lipschitzWith_sub

Premises used: boundedSub_of_lipschitzWith_sub, NNReal.lipschitzWith_sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
obtain : ∀ (Af : ℝ) (hAf : s ⊆ closedBall 0 Af), Bornology.IsBounded (s * t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨Af, hAf⟩ := (isBounded_iff_subset_closedBall 0).mp hs

Premises used: Iff.mp, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
obtain : ∀ (Ag : ℝ) (hAg : t ⊆ closedBall 0 Ag), Bornology.IsBounded (s * t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨Ag, hAg⟩ := (isBounded_iff_subset_closedBall 0).mp ht

Premises used: Iff.mp, OfNat.ofNat, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
⊢ 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 _ _)
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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))
apply :
  s * t ⊆
    (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 * p.2) '' SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag)
⊢ Bornology.IsBounded (s * t)

Tactic:
apply Bornology.IsBounded.subset (key.image continuous_mul).isBounded

Premises used: IsCompact.isBounded, continuous_mul, Bornology.IsBounded.subset, IsCompact.image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
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
⊢ 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

Tactic:
⟨x, x_in_s, y, y_in_t, xy_eq⟩
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 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
⊢ (x, y) ∈ SProd.sprod (α := Set ℝ≥0) (β := Set ℝ≥0) (closedBall 0 Af) (closedBall 0 Ag) ∧
    (fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 * p.2) (x, y) = a

Tactic:
simpa only [Set.mem_prod] using ⟨⟨hAf x_in_s, hAg y_in_t⟩, xy_eq⟩

Premises used: Set.mem_prod
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 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:
exact ⟨⟨x, y⟩, by simpa only [Set.mem_prod] using ⟨⟨hAf x_in_s, hAg y_in_t⟩, xy_eq⟩⟩
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
⊢ cobounded (α × β) = (cobounded α).coprod (cobounded β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set (α × β)
⊢ IsBounded (Prod.fst '' s) ∧ IsBounded (Prod.snd '' s) ↔ IsBounded s

Tactic:
compl_mem_coprod.symm

Premises used: Set.Mem, setOf, Bornology.IsBounded, Filter.compl_mem_coprod, Bornology.IsCobounded, Iff.symm
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set (α × β)
hs : IsBounded s
⊢ IsBounded (Prod.fst '' s)

Tactic:
(isBounded_image_fst_and_snd.2 hs).1

Premises used: Iff.mpr, Bornology.isBounded_image_fst_and_snd, And.left
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set (α × β)
hs : IsBounded s
⊢ IsBounded (Prod.snd '' s)

Tactic:
(isBounded_image_fst_and_snd.2 hs).2

Premises used: Iff.mpr, Bornology.isBounded_image_fst_and_snd, And.right
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
h : IsBounded (s ×ˢ t)
ht : t.Nonempty
⊢ IsBounded s

Tactic:
fst_image_prod s ht ▸ h.image_fst

Premises used: Eq.rec, Set.fst_image_prod, Bornology.IsBounded.image_fst
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
h : IsBounded (s ×ˢ t)
hs : s.Nonempty
⊢ IsBounded t

Tactic:
snd_image_prod hs t ▸ h.image_snd

Premises used: Bornology.IsBounded.image_snd, Eq.rec, Set.snd_image_prod
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s ×ˢ t)

Tactic:
isBounded_image_fst_and_snd.1
    ⟨hs.subset <| fst_image_prod_subset _ _, ht.subset <| snd_image_prod_subset _ _⟩

Premises used: Set.snd_image_prod_subset, Set.fst_image_prod_subset, Bornology.isBounded_image_fst_and_snd, Bornology.IsBounded.subset, And.intro, Iff.mp
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
hne : (s ×ˢ t).Nonempty
⊢ IsBounded (s ×ˢ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
⟨fun h => ⟨h.fst_of_prod hne.snd, h.snd_of_prod hne.fst⟩, fun h => h.1.prod h.2⟩

Premises used: Set.Nonempty.snd, Bornology.IsBounded.prod, And.right, And.left, And.intro, Iff.intro, Bornology.IsBounded.fst_of_prod, Set.Nonempty.fst, Bornology.IsBounded.snd_of_prod
-- Module: Mathlib.Topology.Bornology.Constructions
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
inr : ∀ (hs : s.Nonempty), IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
t : Set β
⊢ IsBounded (SProd.sprod (α := Set α) ∅ t) ↔
    Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ t = ∅ ∨ IsBounded.{u_1} (α := α) ∅ ∧ IsBounded t

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.Constructions
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} (α := β) ∅
inr₁ : ∀ (ht : t.Nonempty), IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
hs : s.Nonempty
⊢ IsBounded (SProd.sprod (β := Set β) s ∅) ↔
    s = ∅ ∨ Eq.{u_2 + 1} (α := Set β) ∅ ∅ ∨ IsBounded s ∧ IsBounded.{u_2} (α := β) ∅

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Bornology α
inst_1 : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
simp only [hs.ne_empty, ht.ne_empty, isBounded_prod_of_nonempty (hs.prod ht), false_or]

Premises used: Set.Nonempty.ne_empty, false_or, Set.Nonempty.prod, Bornology.isBounded_prod_of_nonempty
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
s : Set α
inl : IsBounded (SProd.sprod (α := Set α) (β := Set α) ∅ ∅) ↔ IsBounded.{u_1} (α := α) ∅
inr : ∀ (hs : s.Nonempty), IsBounded (s ×ˢ s) ↔ IsBounded s
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
⊢ IsBounded (SProd.sprod (α := Set α) (β := Set α) ∅ ∅) ↔ IsBounded.{u_1} (α := α) ∅

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
(isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

Premises used: Set.Nonempty.prod, Iff.trans, and_self_iff, Bornology.isBounded_prod_of_nonempty
-- Module: Mathlib.Topology.Bornology.Constructions
Goal:
α : Type u_1
inst : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

Premises used: Set.Nonempty.prod, Iff.trans, and_self_iff, Bornology.isBounded_prod_of_nonempty