awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ U
V : Set β
h : ∀ x ∈ V, ∀ x' ∈ V, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
fun x hx x' hx' i => hεU (h _ hx _ hx' i)
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ U
V : Set β
h : ∀ x ∈ V, ∀ x' ∈ V, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ ε > 0, ∀ᶠ (xy : β × β) in 𝓤 β, ∀ (i : ι), dist (F i xy.1) (F i xy.2) < ε

Tactic:
uniformity_basis_dist.uniformEquicontinuous_iff_right

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.uniformEquicontinuous_iff_right
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
F : ι → β → α
⊢ UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

Tactic:
uniformity_basis_dist.uniformEquicontinuous_iff uniformity_basis_dist

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.uniformEquicontinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
rw : ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
⊢ EquicontinuousAt F x₀

Tactic:
rw [Metric.equicontinuousAt_iff_right]

Premises used: Metric.equicontinuousAt_iff_right
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ a ∈ b ⁻¹' Set.Iio ε, (∀ (i : ι), dist (F i x₀) (F i a) ≤ b a) → ∀ (i : ι), dist (F i x₀) (F i a) < ε

Tactic:
fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁

Premises used: LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        x ∈ b ⁻¹' Set.Iio ε →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) < ε) x} x}
            x}
      a
h₁ : ∀ a ∈ b ⁻¹' Set.Iio ε, (∀ (i : ι), dist (F i x₀) (F i a) ≤ b a) → ∀ (i : ι), dist (F i x₀) (F i a) < ε
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁

Premises used: Iio_mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
rw : ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
⊢ UniformEquicontinuous F

Tactic:
rw [Metric.uniformEquicontinuous_iff]

Premises used: Metric.uniformEquicontinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
rcases :
  ∀ (δ : ℝ) (δ0 : δ > 0) (hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε),
    ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
⊢ ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

Tactic:
rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩

Premises used: Metric.tendsto_nhds_nhds, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
⊢ ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

Tactic:
⟨δ, δ0, fun x y hxy i => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
refine : ∀ (x y : β) (hxy : dist x y < δ) (i : ι), dist (F i x) (F i y) < ε
⊢ ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε

Tactic:
refine ⟨δ, δ0, fun x y hxy i => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (F i x) (F i y) ≤ b (dist x y)

Tactic:
H x y i
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ b (dist x y) ≤ |b (dist x y)|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ |b (dist x y)| = dist (b (dist x y)) 0

Tactic:
simp [Real.dist_eq]

Premises used: Real.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (dist x y) 0 < δ

Tactic:
simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy

Premises used: tsub_zero, Real.dist_eq, abs_dist
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), Dist.dist (F i x) (F i y) ≤ b (Dist.dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, Dist.dist x 0 < δ → Dist.dist (b x) 0 < ε
x y : β
hxy : Dist.dist x y < δ
i : ι
dist : |b (Dist.dist x y)| = Dist.dist (b (Dist.dist x y)) 0
⊢ Dist.dist (F i x) (F i y) < ε

Tactic:
calc
    dist (F i x) (F i y) ≤ b (dist x y) := H x y i
    _ ≤ |b (dist x y)| := le_abs_self _
    _ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
    _ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)

Premises used: le_abs_self, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ Equicontinuous F

Tactic:
(uniformEquicontinuous_of_continuity_modulus b b_lim F H).equicontinuous

Premises used: UniformEquicontinuous.equicontinuous, Metric.uniformEquicontinuous_of_continuity_modulus
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p x : Z
⊢ 0 ≤ dist (Φ p) (Φ x) + dist (Ψ p) (Ψ x)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)

Tactic:
have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0

Tactic:
le_antisymm ?_ (le_ciInf A)

Premises used: le_ciInf, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
refine : LE.le (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
⊢ Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0

Tactic:
refine le_antisymm ?_ (le_ciInf A)

Premises used: le_ciInf, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)

Tactic:
have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
rw : ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ LE.le (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0

Tactic:
rw [this]
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)

Tactic:
ciInf_le ⟨0, forall_mem_range.2 A⟩ p

Premises used: Iff.mpr, Set.forall_mem_range, ciInf_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)

Tactic:
exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p

Premises used: Iff.mpr, Set.forall_mem_range, ciInf_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0

Tactic:
have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 := by
    have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
    refine le_antisymm ?_ (le_ciInf A)
    have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
    rw [this]
    exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
this : Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε

Tactic:
simp only [glueDist, this, zero_add]

Premises used: zero_add, Metric.glueDist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val : X
val_1 : Y
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inl val)) (Sum.swap (Sum.inr val_1)) = glueDist Φ Ψ ε (Sum.inl val) (Sum.inr val_1)

Tactic:
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, add_comm]

Premises used: Sum.swap_inr, add_comm, Metric.glueDist, Sum.swap_inl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val : Y
val_1 : X
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr val)) (Sum.swap (Sum.inl val_1)) = glueDist Φ Ψ ε (Sum.inr val) (Sum.inl val_1)

Tactic:
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, add_comm]

Premises used: Sum.swap_inr, add_comm, Metric.glueDist, Sum.swap_inl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y : Y
x_1 : Z
⊢ 0 ≤ dist x (Φ x_1) + dist y (Ψ x_1)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inl y) (Sum.inr x)

Tactic:
apply le_glueDist_inl_inr

Premises used: Metric.le_glueDist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
simp : (⨅ (p : Z), dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)

Tactic:
simp only [glueDist]

Premises used: Metric.glueDist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
rw : ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z
⊢ (⨅ (p : Z), dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ε + dist y z

Tactic:
rw [add_right_comm, add_le_add_iff_right]

Premises used: add_right_comm, add_le_add_iff_right
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z

Tactic:
le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_

Premises used: ciInf_le_of_le, Exists.intro, OfNat.ofNat, le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
refine_1 : ∀ (p : Z), Membership.mem (γ := Set ℝ) (lowerBounds (range fun (p : Z) ↦ dist x (Φ p) + dist z (Ψ p))) 0
refine_2 : ∀ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
⊢ ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z

Tactic:
refine le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_

Premises used: ciInf_le_of_le, Exists.intro, OfNat.ofNat, le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p x_1 : Z
⊢ 0 ≤ dist x (Φ x_1) + dist z (Ψ x_1)

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ Membership.mem (γ := Set ℝ) (lowerBounds (range fun (p : Z) ↦ dist x (Φ p) + dist z (Ψ p))) 0

Tactic:
exact forall_mem_range.2 fun _ => by positivity

Premises used: Iff.mpr, Set.forall_mem_range
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
linarith :
  dist x (Φ p) + dist y (Ψ p) + dist y z < dist x (Φ p) + dist z (Ψ p) →
    dist x (Φ p) + dist y (Ψ p) + dist y z - (dist x (Φ p) + dist z (Ψ p)) +
        (dist z (Ψ p) - (dist y z + dist y (Ψ p))) =
      0
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z

Tactic:
linarith [dist_triangle_left z (Ψ p) y]

Premises used: dist_triangle_left
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
simp_rw : dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)

Tactic:
simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]

Premises used: add_assoc, Metric.glueDist, add_add_add_comm
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))

Tactic:
le_ciInf_add fun p => ?_

Premises used: le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
refine : ∀ (p : Z), dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))

Tactic:
refine le_ciInf_add fun p => ?_

Premises used: le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
rw : dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))

Tactic:
rw [add_left_comm, add_assoc, ← two_mul]

Premises used: add_left_comm, add_assoc, two_mul
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
le_ciInf_add fun q => ?_

Premises used: le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
refine : ∀ (q : Z), dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
refine le_ciInf_add fun q => ?_

Premises used: le_ciInf_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
rw : dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
rw [dist_comm z]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
linarith :
  dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε)) < dist x z →
    dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε)) - dist x z +
            (dist x z - (dist x (Φ p) + dist (Φ p) (Φ q) + dist (Φ q) z)) +
          (dist (Ψ p) (Ψ q) - (dist y (Ψ p) + dist y (Ψ q))) +
        (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q) - 2 * ε) =
      0
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))

Tactic:
linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]

Premises used: abs_le, dist_triangle4, dist_triangle_left, And.right, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y z : X
simp :
  glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl z)) ≤
    glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
      glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inl z))
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inl z)

Tactic:
simp only [← glueDist_swap Φ]

Premises used: Metric.glueDist_swap
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y z : X
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl z)) ≤
    glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
      glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inl z))

Tactic:
apply glueDist_triangle_inl_inr_inr

Premises used: _private.0.Metric.glueDist_triangle_inl_inr_inr