awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
x x_1 : X
⊢ (ker (g ∘ f) : X → X → Prop) x x_1 ↔ (ker f : X → X → Prop) x x_1

Tactic:
simp [g_emb.injective.eq_iff]

Premises used: Function.Injective.eq_iff, Topology.IsEmbedding.injective
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
⊢ g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)

Tactic:
have key : g ∘ kerLift f ∘ Φ = kerLift (g ∘ f) :=
    funext <| Quotient.ind fun _ ↦ rfl
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)
simp_rw :
  IsEmbedding (g ∘ kerLift f) ↔
    IsEmbedding (X := Quotient (ker (g ∘ f))) (g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)))
⊢ IsStrictMap f ↔ IsStrictMap (g ∘ f)

Tactic:
simp_rw [isStrictMap_iff_isEmbedding_kerLift, ← g_emb.of_comp_iff, ← key]

Premises used: Topology.isStrictMap_iff_isEmbedding_kerLift, Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)
H : IsEmbedding (X := Quotient (ker (g ∘ f))) (g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)))
⊢ IsEmbedding (g ∘ kerLift f)

Tactic:
simpa [comp_assoc] using H.comp Φ.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Homeomorph.symm, Function.comp_assoc
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)) = kerLift (g ∘ f)
⊢ IsEmbedding (g ∘ kerLift f) ↔
    IsEmbedding (X := Quotient (ker (g ∘ f))) (g ∘ kerLift f ∘ (⇑Φ : (a : Quotient (ker (g ∘ f))) → Quotient (ker f)))

Tactic:
exact ⟨fun H ↦ H.comp Φ.isEmbedding,
    fun H ↦ by simpa [comp_assoc] using H.comp Φ.symm.isEmbedding⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_emb : IsEmbedding f
⊢ IsStrictMap f

Tactic:
f_emb.isStrictMap_iff.mp .id

Premises used: Topology.IsStrictMap.id, Topology.IsEmbedding.isStrictMap_iff, Iff.mp
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap f ↔ IsStrictMap f ∧ Surjective f

Tactic:
⟨fun H ↦ ⟨H.isStrictMap, H.surjective⟩, fun ⟨f_strict, f_surj⟩ ↦ ?_⟩

Premises used: _private.0.Topology.isQuotientMap_iff_isStrictMap_surjective.match_1, Topology.IsQuotientMap.surjective, And.intro, Iff.intro, Topology.IsQuotientMap, Topology.IsQuotientMap.isStrictMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
refine : IsStrictMap f ∧ Surjective f → ∀ (f_strict : IsStrictMap f) (f_surj : Surjective f), IsQuotientMap f
⊢ IsQuotientMap f ↔ IsStrictMap f ∧ Surjective f

Tactic:
refine ⟨fun H ↦ ⟨H.isStrictMap, H.surjective⟩, fun ⟨f_strict, f_surj⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Surjective f
f_strict : IsStrictMap f
f_surj : Surjective f
⊢ IsQuotientMap (rangeFactorization f)

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at f_strict

Premises used: Topology.isStrictMap_iff_isQuotientMap_rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Surjective f
f_strict : IsStrictMap f
f_surj : Surjective f
f_strict₁ : IsQuotientMap (rangeFactorization f)
⊢ Surjective f

Tactic:
rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at f_strict

Premises used: Topology.isStrictMap_iff_isQuotientMap_rangeFactorization
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Surjective f
f_strict : IsQuotientMap (rangeFactorization f)
f_surj : Surjective f
Φ : (↑(range f) : Type u_2) ≃ₜ Y :=
  Homeomorph.trans (Homeomorph.setCongr (s := range f) (t := univ) ⋯) (Homeomorph.Set.univ Y)
⊢ IsQuotientMap f

Tactic:
Φ.isQuotientMap.comp f_strict

Premises used: Topology.IsQuotientMap.comp, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Surjective f
f_strict : IsQuotientMap (rangeFactorization f)
f_surj : Surjective f
Φ : (↑(range f) : Type u_2) ≃ₜ Y :=
  Homeomorph.trans (Homeomorph.setCongr (s := range f) (t := univ) ⋯) (Homeomorph.Set.univ Y)
⊢ IsQuotientMap f

Tactic:
exact Φ.isQuotientMap.comp f_strict

Premises used: Topology.IsQuotientMap.comp, Homeomorph.isQuotientMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f

Tactic:
⟨fun H ↦ ⟨H.isStrictMap, H.injective⟩, fun ⟨f_strict, f_inj⟩ ↦ ?_⟩

Premises used: And.intro, Iff.intro, Topology.IsEmbedding.injective, Topology.IsEmbedding, _private.0.Topology.isEmbedding_iff_isStrictMap_injective.match_1, Topology.IsEmbedding.isStrictMap
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
refine : IsStrictMap f ∧ Injective f → ∀ (f_strict : IsStrictMap f) (f_inj : Injective f), IsEmbedding f
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f

Tactic:
refine ⟨fun H ↦ ⟨H.isStrictMap, H.injective⟩, fun ⟨f_strict, f_inj⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsStrictMap f
f_inj : Injective f
⊢ IsEmbedding (kerLift f)

Tactic:
rw [isStrictMap_iff_isEmbedding_kerLift] at f_strict

Premises used: Topology.isStrictMap_iff_isEmbedding_kerLift
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsStrictMap f
f_inj : Injective f
f_strict₁ : IsEmbedding (kerLift f)
⊢ Injective f

Tactic:
rw [isStrictMap_iff_isEmbedding_kerLift] at f_strict

Premises used: Topology.isStrictMap_iff_isEmbedding_kerLift
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsEmbedding (kerLift f)
f_inj : Injective f
⊢ ∀ (x₁ x₂ : X), (ker f : X → X → Prop) x₁ x₂ ↔ (⊥ : X → X → Prop) x₁ x₂

Tactic:
simp [f_inj.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsEmbedding (kerLift f)
f_inj : Injective f
Φ : Quotient (ker f) ≃ₜ X := Homeomorph.trans (Homeomorph.Quotient.congrRight ⋯) Homeomorph.quotientBot
⊢ IsEmbedding f

Tactic:
f_strict.comp Φ.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, Setoid.kerLift, Topology.IsEmbedding.comp, Homeomorph.symm
-- Module: Mathlib.Topology.Maps.Strict.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsStrictMap f ∧ Injective f
f_strict : IsEmbedding (kerLift f)
f_inj : Injective f
Φ : Quotient (ker f) ≃ₜ X := Homeomorph.trans (Homeomorph.Quotient.congrRight ⋯) Homeomorph.quotientBot
⊢ IsEmbedding f

Tactic:
exact f_strict.comp Φ.symm.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, Homeomorph.symm
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : Monoid β
_i : LipschitzMul β
⊢ LipschitzWith (β := β) (LipschitzMul.C β) fun (p : β × β) ↦ p.1 * p.2

Tactic:
Classical.choose_spec _i.lipschitz_mul

Premises used: LipschitzMul.lipschitz_mul, Classical.choose_spec, LipschitzMul.C
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : Monoid β
inst_2 : LipschitzMul β
rw : LipschitzWith (β := β) (LipschitzMul.C β) fun (p : β × β) ↦ p.1 * p.2
⊢ ∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ (↑(LipschitzMul.C β) : ℝ) * dist p q

Tactic:
rw [← lipschitzWith_iff_dist_le_mul]

Premises used: lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : Monoid β
inst_2 : LipschitzMul β
⊢ LipschitzWith (β := β) (LipschitzMul.C β) fun (p : β × β) ↦ p.1 * p.2

Tactic:
lipschitzWith_lipschitz_const_mul_edist

Premises used: lipschitzWith_lipschitz_const_mul_edist
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : Monoid β
inst_2 : LipschitzMul β
⊢ LipschitzWith (β := β) (LipschitzMul.C β) fun (p : β × β) ↦ p.1 * p.2

Tactic:
exact lipschitzWith_lipschitz_const_mul_edist

Premises used: lipschitzWith_lipschitz_const_mul_edist
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
⊢ ContinuousMul β

Tactic:
⟨lipschitzWith_lipschitz_const_mul_edist.continuous⟩

Premises used: lipschitzWith_lipschitz_const_mul_edist, ContinuousMul.mk, LipschitzWith.continuous
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
s : Submonoid β
x₁ x₂ y₁ y₂ : ↥s
⊢ edist.{u_2} (α := β) ((fun (p : β × β) ↦ p.1 * p.2) ((↑x₁ : β), (↑x₂ : β)))
      ((fun (p : β × β) ↦ p.1 * p.2) ((↑y₁ : β), (↑y₂ : β))) ≤
    (↑(LipschitzMul.C β) : ENNReal) * edist ((↑x₁ : β), (↑x₂ : β)) ((↑y₁ : β), (↑y₂ : β))

Tactic:
lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩

Premises used: lipschitzWith_lipschitz_const_mul_edist, Prod.mk, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
s : Submonoid β
x₁ x₂ y₁ y₂ : ↥s
⊢ edist.{u_2} (α := ↥s) ((fun (p : ↥s × ↥s) ↦ p.1 * p.2) (x₁, x₂)) ((fun (p : ↥s × ↥s) ↦ p.1 * p.2) (y₁, y₂)) ≤
    (↑(LipschitzMul.C β) : ENNReal) * edist (x₁, x₂) (y₁, y₂)

Tactic:
convert! lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩ using 1

Premises used: lipschitzWith_lipschitz_const_mul_edist, Prod.mk, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
simp : |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
⊢ dist (p.1 + p.2) (q.1 + q.2) ≤ (↑2 : ℝ) * dist p q

Tactic:
simp only [Real.dist_eq, Prod.dist_eq, NNReal.coe_ofNat,
      add_sub_add_comm, two_mul]

Premises used: two_mul, Prod.dist_eq, Real.dist_eq, NNReal.coe_ofNat, add_sub_add_comm
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|

Tactic:
le_trans (abs_add_le (p.1 - q.1) (p.2 - q.2)) ?_

Premises used: HSub.hSub, Prod.fst, abs_add_le, Prod.snd, le_trans
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
refine : |p.1 - q.1| + |p.2 - q.2| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
⊢ |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|

Tactic:
refine le_trans (abs_add_le (p.1 - q.1) (p.2 - q.2)) ?_

Premises used: HSub.hSub, Prod.fst, abs_add_le, Prod.snd, le_trans
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1| + |p.2 - q.2| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|

Tactic:
add_le_add (le_max_left _ _) (le_max_right _ _)

Premises used: le_max_right, add_le_add, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1| + |p.2 - q.2| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|

Tactic:
exact add_le_add (le_max_left _ _) (le_max_right _ _)

Premises used: le_max_right, add_le_add, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist (α := ℝ≥0) ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 + p.2) (x₁, x₂)) ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 + p.2) (y₁, y₂)) ≤
    (↑(LipschitzAdd.C ℝ) : ENNReal) * edist (x₁, x₂) (y₁, y₂)

Tactic:
lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩

Premises used: lipschitzWith_lipschitz_const_add_edist, Prod.mk, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist (α := ℝ≥0) ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 + p.2) (x₁, x₂)) ((fun (p : ℝ≥0 × ℝ≥0) ↦ p.1 + p.2) (y₁, y₂)) ≤
    (↑(LipschitzAdd.C ℝ) : ENNReal) * edist (x₁, x₂) (y₁, y₂)

Tactic:
exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩

Premises used: lipschitzWith_lipschitz_const_add_edist, Prod.mk, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α
y₁ y₂ : β
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
IsBoundedSMul.dist_smul_pair' x y₁ y₂

Premises used: IsBoundedSMul.dist_smul_pair'
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x₁ x₂ : α
y : β
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
IsBoundedSMul.dist_pair_smul' x₁ x₂ y

Premises used: IsBoundedSMul.dist_pair_smul'
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
rcases :
  ∀ (C : ℝ) (hC₀ : 0 < C) (hC : s ⊆ Metric.ball 0 C),
    UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s
⊢ UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s

Tactic:
rcases hs.subset_ball_lt 0 0 with ⟨C, hC₀, hC⟩

Premises used: Bornology.IsBounded.subset_ball_lt, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
rw :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ x ∈ s,
        ∀ y ∈ s,
          dist x y ≤ δ →
            dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) x)
                (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) y) ≤
              ε
⊢ UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s

Tactic:
rw [Metric.uniformContinuousOn_iff_le]

Premises used: Metric.uniformContinuousOn_iff_le
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
⊢ ε / (2 * C) > 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
refine :
  ∀ (x x : α × β) (a : α) (b : β) (hab : (a, b) ∈ s) (x : α) (y : β) (hxy : (x, y) ∈ s)
    (h : dist (a, b) (x, y) ≤ ε / (2 * C)),
    dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
        (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
      ε
⊢ ∃ δ > 0,
    ∀ x ∈ s,
      ∀ y ∈ s,
        dist x y ≤ δ →
          dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) x)
              (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) y) ≤
            ε

Tactic:
refine ⟨ε / (2 * C), by positivity, fun ⟨a, b⟩ hab ⟨x, y⟩ hxy h ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : (a, b) ∈ s
x : α
y : β
hxy : (x, y) ∈ s
h : dist (a, b) (x, y) ≤ ε / (2 * C)
grw :
  ∀ (hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C) (x : α) (y : β)
    (hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C) (h : dist (a, b) (x, y) ≤ ε / (2 * C)),
    dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
        (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
      ε
⊢ dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε

Tactic:
grw [hC, Metric.mem_ball, Prod.dist_eq, max_lt_iff] at hab hxy

Premises used: Prod.dist_eq, max_lt_iff, Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (a, b).1 (x, y).1 ≤ ε / (2 * C) ∧ dist (a, b).2 (x, y).2 ≤ ε / (2 * C)

Tactic:
rw [Prod.dist_eq, max_le_iff] at h

Premises used: Prod.dist_eq, max_le_iff
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b).1 (x, y).1 ≤ ε / (2 * C) ∧ dist (a, b).2 (x, y).2 ≤ ε / (2 * C)
dsimp : dist (a • b) (x • y) ≤ ε
⊢ dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε

Tactic:
dsimp at hab hxy h ⊢
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
grw : C * (ε / (2 * C)) + ε / (2 * C) * C ≤ ε
⊢ dist (a • b) (x • y) ≤ ε

Tactic:
grw [dist_triangle _ (a • y), dist_pair_smul, dist_smul_pair, hab.1, hxy.2, h.2, h.1]

Premises used: dist_triangle, dist_pair_smul, And.right, And.left, HSMul.hSMul, dist_smul_pair
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
field_simp : HAdd.hAdd (α := ℝ) 1 1 ≤ 2
⊢ C * (ε / (2 * C)) + ε / (2 * C) * C ≤ ε

Tactic:
field_simp
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ HAdd.hAdd (α := ℝ) 1 1 ≤ 2

Tactic:
norm_num1
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
rw : ∀ (x : α × β), ContinuousAt (Y := β) (fun (p : α × β) ↦ p.1 • p.2) x
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × β) ↦ p.1 • p.2

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α × β
⊢ ContinuousAt (Y := β) (fun (p : α × β) ↦ p.1 • p.2) x

Tactic:
Metric.isBounded_ball (x := 0) (r := dist x 0 + 1) |>.uniformContinuousOn_smul
      |>.continuousOn |>.continuousAt ?_

Premises used: Bornology.IsBounded.uniformContinuousOn_smul, setOf, UniformContinuousOn.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.MetricSpace.Algebra
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α × β
refine : Metric.ball 0 (dist x 0 + 1) ∈ 𝓝 x
⊢ ContinuousAt (Y := β) (fun (p : α × β) ↦ p.1 • p.2) x

Tactic:
refine Metric.isBounded_ball (x := 0) (r := dist x 0 + 1) |>.uniformContinuousOn_smul
      |>.continuousOn |>.continuousAt ?_

Premises used: Bornology.IsBounded.uniformContinuousOn_smul, UniformContinuousOn.continuousOn, ContinuousOn.continuousAt