awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
inst_1 : BoundedSpace α
s : Set α
⊢ IsCobounded s

Tactic:
compl_compl s ▸ IsBounded.all sᶜ

Premises used: Bornology.IsBounded.all, compl_compl, Compl.compl, Eq.rec
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
inst_1 : BoundedSpace α
⊢ cobounded α = ⊥

Tactic:
cobounded_eq_bot_iff.2 ‹_›

Premises used: Iff.mpr, Bornology.cobounded_eq_bot_iff
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
s : Set α
⊢ Bornology.IsCobounded (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ Bornology.IsCobounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
s : Set αᵒᵈ
⊢ Bornology.IsCobounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ Bornology.IsCobounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
s : Set α
⊢ Bornology.IsBounded (α := αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔ Bornology.IsBounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
s : Set αᵒᵈ
⊢ Bornology.IsBounded (α := α) ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) ↔ Bornology.IsBounded s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, OrderDual
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : Bornology R
inst_1 : Sub R
inst_2 : BoundedSub R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
⊢ Bornology.IsBounded (s - t)

Tactic:
BoundedSub.isBounded_sub hs ht

Premises used: BoundedSub.isBounded_sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
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
⊢ ∃ (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)

Premises used: Iff.mpr, Metric.isBounded_iff, isBounded_sub, Iff.mp, Metric.isBounded_range_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C

Tactic:
use C
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
x y : X
⊢ dist ((f - g) x) ((f - g) y) ≤ C

Tactic:
hC (Set.sub_mem_sub (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
           (Set.sub_mem_sub (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Premises used: Set.mem_range_self, Set.sub_mem_sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
x y : X
⊢ dist ((f - g) x) ((f - g) y) ≤ C

Tactic:
exact hC (Set.sub_mem_sub (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
           (Set.sub_mem_sub (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Premises used: Set.mem_range_self, Set.sub_mem_sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)

Tactic:
have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 (α := R) ((fun (p : R × R) ↦ p.1 - p.2) '' s ×ˢ t)

Tactic:
lip.isBounded_image bdd

Premises used: LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
h : s - t = (fun (p : R × R) ↦ p.1 - p.2) '' s ×ˢ t
⊢ Bornology.IsBounded (s - t)

Tactic:
convert! lip.isBounded_image bdd

Premises used: LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
⊢ s - t = (fun (p : R × R) ↦ p.1 - p.2) '' s ×ˢ t

Tactic:
simp
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : Bornology R
inst_1 : Mul R
inst_2 : BoundedMul R
s t : Set R
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
⊢ Bornology.IsBounded (s * t)

Tactic:
BoundedMul.isBounded_mul hs ht

Premises used: BoundedMul.isBounded_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
neg : ∀ (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)

Tactic:
by_cases s_empty : s = ∅
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)

Tactic:
simp [s_empty]
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 = ∅
⊢ s.Nonempty

Tactic:
simp_rw [← nonempty_iff_ne_empty] at s_empty

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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.Nonempty
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ HPow.hPow (β := ℕ) x 0) '' s)

Tactic:
simp [s_empty]
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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_1 ∈ s, x_1 ^ (n + 1) = x

Tactic:
simp only [mem_image] at hx

Premises used: Set.mem_image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
obtain : ∀ (y : R) (y_in_s : y ∈ s) (ypow_eq_x : y ^ (n + 1) = x), x ∈ (fun (x : R) ↦ x ^ n) '' s * s
⊢ x ∈ (fun (x : R) ↦ x ^ n) '' s * s

Tactic:
obtain ⟨y, y_in_s, ypow_eq_x⟩ := hx
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
rw : y ^ n * y ∈ (fun (x : R) ↦ x ^ n) '' s * s
⊢ x ∈ (fun (x : R) ↦ x ^ n) '' s * s

Tactic:
rw [← ypow_eq_x, pow_succ y n]

Premises used: pow_succ
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
apply : Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' s) (y ^ n)
⊢ y ^ n * y ∈ (fun (x : R) ↦ x ^ n) '' s * s

Tactic:
apply Set.mul_mem_mul _ y_in_s

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : y ∈ s ∧ (fun (x : R) ↦ x ^ n) y = y ^ n
⊢ Membership.mem (γ := Set R) ((fun (x : R) ↦ x ^ n) '' s) (y ^ n)

Tactic:
use y
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
⊢ (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
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
obs : (fun (x : R) ↦ x ^ (n + 1)) '' s ⊆ (fun (x : R) ↦ x ^ n) '' s * s
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ (n + 1)) '' s)

Tactic:
(isBounded_mul hn s_bdd).subset obs

Premises used: isBounded_mul, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
obs : (fun (x : R) ↦ x ^ (n + 1)) '' s ⊆ (fun (x : R) ↦ x ^ n) '' s * s
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ (n + 1)) '' s)

Tactic:
exact (isBounded_mul hn s_bdd).subset obs

Premises used: isBounded_mul, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
succ :
  ∀ (n : ℕ) (hn : Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' s)),
    Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ (n + 1)) '' s)
⊢ Bornology.IsBounded (α := R) ((fun (x : R) ↦ x ^ n) '' 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

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
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
⊢ ∃ (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)

Premises used: Iff.mpr, isBounded_mul, Metric.isBounded_iff, Iff.mp, Metric.isBounded_range_iff
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C
⊢ ∃ (C : ℝ), ∀ (x y : X), dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
use C
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
x y : X
⊢ dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
hC (Set.mul_mem_mul (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
           (Set.mul_mem_mul (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Premises used: Set.mem_range_self, Set.mul_mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
x y : X
⊢ dist ((f * g) x) ((f * g) y) ≤ C

Tactic:
exact hC (Set.mul_mem_mul (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
           (Set.mul_mem_mul (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))

Premises used: Set.mem_range_self, Set.mul_mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)

Tactic:
have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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)
obtain : ∀ (C : ℝ≥0) (mul_lip : LipschitzWith (β := R) C fun (p : R × R) ↦ p.1 * p.2), Bornology.IsBounded (s * t)
⊢ Bornology.IsBounded (s * t)

Tactic:
obtain ⟨C, mul_lip⟩ := ‹LipschitzMul R›.lipschitz_mul

Premises used: LipschitzMul.lipschitz_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 (α := R) ((fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t)

Tactic:
mul_lip.isBounded_image bdd

Premises used: LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : s * t = (fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t
⊢ Bornology.IsBounded (s * t)

Tactic:
convert! mul_lip.isBounded_image bdd

Premises used: LipschitzWith.isBounded_image
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h : ∀ (p : R), p ∈ s * t ↔ Membership.mem (γ := Set R) ((fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t) p
⊢ s * t = (fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t

Tactic:
ext p
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 ↔ Membership.mem (γ := Set R) ((fun (p : R × R) ↦ p.1 * p.2) '' s ×ˢ t) p

Tactic:
simp only [Set.mem_image, Set.mem_prod, Prod.exists]

Premises used: Set.mem_image, Set.mem_prod, Prod.exists
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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
h₁ : (∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p) → p ∈ s * t
⊢ p ∈ s * t ↔ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p

Tactic:
constructor
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 a : R
a_in_s : a ∈ s
b : R
b_in_t : b ∈ t
eq_p : (fun (x1 x2 : R) ↦ x1 * x2) a b = p
⊢ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p

Tactic:
⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 a : R
a_in_s : a ∈ s
b : R
b_in_t : b ∈ t
eq_p : (fun (x1 x2 : R) ↦ x1 * x2) a b = p
⊢ ∃ (a : R) (b : R), (a ∈ s ∧ b ∈ t) ∧ a * b = p

Tactic:
exact ⟨a, b, ⟨a_in_s, b_in_t⟩, eq_p⟩
-- Module: Mathlib.Topology.Bornology.BoundedOperation
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 a b : R
a_in_s : a ∈ s
b_in_t : b ∈ t
eq_p : a * b = p
⊢ p ∈ s * t

Tactic:
simpa [← eq_p] using Set.mul_mem_mul a_in_s b_in_t

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
⊢ LipschitzWith (β := R) (HAdd.hAdd (α := ℝ≥0) 1 1) fun (x : R × R) ↦ x.1 - x.2

Tactic:
LipschitzWith.prod_fst.sub LipschitzWith.prod_snd

Premises used: LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzWith.sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
h : 2 = HAdd.hAdd (α := ℝ≥0) 1 1
⊢ LipschitzWith (β := R) 2 fun (p : R × R) ↦ p.1 - p.2

Tactic:
convert! LipschitzWith.prod_fst.sub LipschitzWith.prod_snd

Premises used: LipschitzWith.prod_snd, LipschitzWith.prod_fst, LipschitzWith.sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
⊢ 2 = HAdd.hAdd (α := ℝ≥0) 1 1

Tactic:
norm_num
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
⊢ BoundedSub R

Tactic:
boundedSub_of_lipschitzWith_sub SeminormedAddCommGroup.lipschitzWith_sub

Premises used: boundedSub_of_lipschitzWith_sub, SeminormedAddCommGroup.lipschitzWith_sub
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
rw : (fun (x_1 : R) ↦ x_1 + x) ⁻¹' s ∈ cobounded R
⊢ Membership.mem (γ := Filter R) (map (fun (x_1 : R) ↦ x_1 + x) (cobounded R)) s

Tactic:
rw [mem_map]

Premises used: Filter.mem_map
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
rw : ∀ (hs : Bornology.IsBounded sᶜ), Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' s)ᶜ
⊢ (fun (x_1 : R) ↦ x_1 + x) ⁻¹' s ∈ cobounded R

Tactic:
rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢

Premises used: Bornology.isBounded_compl_iff, Bornology.isCobounded_def
-- 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_1 + x) ⁻¹' sᶜ)
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' 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 (sᶜ - {x})

Tactic:
isBounded_sub hs (t := { x }) isBounded_singleton

Premises used: isBounded_sub, 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_1 + x) ⁻¹' sᶜ = sᶜ - {x}
⊢ Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ)

Tactic:
convert! isBounded_sub hs (t := { x }) isBounded_singleton using 1

Premises used: isBounded_sub, 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_1 + x) ⁻¹' sᶜ) y ↔ y ∈ sᶜ - {x}
⊢ (fun (x_1 : R) ↦ x_1 + x) ⁻¹' sᶜ = sᶜ - {x}

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_1 + x) ⁻¹' sᶜ) y ↔ y ∈ sᶜ - {x}

Tactic:
simp [sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
rw : (fun (x_1 : R) ↦ x + x_1) ⁻¹' s ∈ cobounded R
⊢ Membership.mem (γ := Filter R) (map (fun (x_1 : R) ↦ x + x_1) (cobounded R)) s

Tactic:
rw [mem_map]

Premises used: Filter.mem_map
-- Module: Mathlib.Topology.Bornology.BoundedOperation
Goal:
R : Type u_1
inst : SeminormedAddCommGroup R
x : R
s : Set R
hs : s ∈ cobounded R
rw : ∀ (hs : Bornology.IsBounded sᶜ), Bornology.IsBounded (α := R) ((fun (x_1 : R) ↦ x + x_1) ⁻¹' s)ᶜ
⊢ (fun (x_1 : R) ↦ x + x_1) ⁻¹' s ∈ cobounded R

Tactic:
rw [← isCobounded_def, ← isBounded_compl_iff] at hs ⊢

Premises used: Bornology.isBounded_compl_iff, Bornology.isCobounded_def