awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (f x) (f y) ≤ edist (f (↑z : α)) (f x) + edist (f (↑z : α)) (f y)

Tactic:
edist_triangle_left _ _ _

Premises used: edist_triangle_left
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (f (↑z : α)) (f x) + edist (f (↑z : α)) (f y) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + edist (f (↑z : α)) (f y)

Tactic:
add_le_add_left
        (hf _ z.2 ⟨mem_ball_self <| hε _ z.2, z.2⟩ ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩) _

Premises used: half_lt_self, Metric.mem_ball_self, add_le_add_left, And.intro, LT.lt.trans, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + edist (f (↑z : α)) (f y) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * edist (↑z : α) y

Tactic:
add_le_add_right (hK' _ z.2 _ ⟨hy, hy'⟩) _

Premises used: add_le_add_right, And.intro, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
bc : edist (↑z : α) y ≤ edist x (↑z : α) + edist x y
⊢ (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * edist (↑z : α) y ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (↑z : α) y ≤ edist x (↑z : α) + edist x y

Tactic:
edist_triangle_left z.1 y x

Premises used: edist_triangle_left, Subtype.val
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (↑z : α) y ≤ edist x (↑z : α) + edist x y

Tactic:
exact edist_triangle_left z.1 y x

Premises used: edist_triangle_left, Subtype.val
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
simp_rw :
  (↑(K (↑z : α) ⋯) : ENNReal) * ENNReal.ofReal (dist x (↑z : α)) +
      (↑(K' (↑z : α) ⋯) : ENNReal) * (ENNReal.ofReal (dist x (↑z : α)) + ENNReal.ofReal (dist x y)) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * ENNReal.ofReal (dist x y) +
      (↑(K' (↑z : α) ⋯) : ENNReal) * (ENNReal.ofReal (dist x y) + ENNReal.ofReal (dist x y))
⊢ (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist x y + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x y + edist x y)

Tactic:
simp_rw [edist_dist, dist_comm _ x]

Premises used: dist_comm, edist_dist
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
h₁ h₂ : dist x (↑z : α) ≤ dist x y
⊢ (↑(K (↑z : α) ⋯) : ENNReal) * ENNReal.ofReal (dist x (↑z : α)) +
      (↑(K' (↑z : α) ⋯) : ENNReal) * (ENNReal.ofReal (dist x (↑z : α)) + ENNReal.ofReal (dist x y)) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * ENNReal.ofReal (dist x y) +
      (↑(K' (↑z : α) ⋯) : ENNReal) * (ENNReal.ofReal (dist x y) + ENNReal.ofReal (dist x y))

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
linarith : dist x y < dist x (↑z : α) → 2 / 2 = 1
linarith₁ : dist x y < dist x (↑z : α) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : dist x y < dist x (↑z : α) → GT.gt (α := ℝ) 2 0
linarith₃ :
  dist x y < dist x (↑z : α) →
    dist x y - dist x (↑z : α) + (2 * dist x (↑z : α) - 1 * ε (↑z : α) ⋯) + (ε (↑z : α) ⋯ - dist y (↑z : α)) +
        (dist y (↑z : α) - (dist x y + dist x (↑z : α))) =
      0
⊢ dist x (↑z : α) ≤ dist x y

Tactic:
linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]

Premises used: dist_triangle_left, Metric.mem_ball, not_lt, And.right, Iff.mp, Subtype.val
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ (↑(K (↑z : α) ⋯) : ENNReal) * edist x y + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x y + edist x y) =
    ((↑(K (↑z : α) ⋯) : ENNReal) + 2 * (↑(K' (↑z : α) ⋯) : ENNReal)) * edist x y

Tactic:
ring
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
bc : K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯ ≤ t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯
⊢ (↑(K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯) : ENNReal) * edist x y ≤
    (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯ ≤ K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯ ≤ t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯

Tactic:
exact .trans (by rfl) (t.le_sup hz)
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)
calc :
  (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * edist (↑z : α) y ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y)
calc₁ :
  (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist x y + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x y + edist x y)
calc₂ :
  (↑(K (↑z : α) ⋯) : ENNReal) * edist x y + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x y + edist x y) =
    (↑(K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯) : ENNReal) * edist x y
calc₃ :
  (↑(K (↑z : α) ⋯ + 2 * K' (↑z : α) ⋯) : ENNReal) * edist x y ≤
    (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
calc edist (f x) (f y)
      _ ≤ edist (f z) (f x) + edist (f z) (f y) := edist_triangle_left _ _ _
      _ ≤ (K _ z.2) * edist z.1 x + edist (f z) (f y) := add_le_add_left
        (hf _ z.2 ⟨mem_ball_self <| hε _ z.2, z.2⟩ ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * edist z.1 y :=
        add_le_add_right (hK' _ z.2 _ ⟨hy, hy'⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * (edist x z.1 + edist x y) := by
        gcongr; exact edist_triangle_left z.1 y x
      _ ≤ (K _ z.2) * edist x y + (K' _ z.2) * (edist x y + edist x y) := by
        simp_rw [edist_dist, dist_comm _ x]
        gcongr <;> linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
      _ = ↑(K _ z.2 + 2 * K' _ z.2) * edist x y := by push_cast; ring
      _ ≤ _ := by gcongr; exact .trans (by rfl) (t.le_sup hz)

Premises used: half_lt_self, HMul.hMul, Metric.mem_ball_self, add_le_add_left, add_le_add_right, HAdd.hAdd, And.intro, LT.lt.trans, EDist.edist, edist_triangle_left, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
⊢ Eq (α := Set (ContinuousMultilinearMap.{u_1, u_6, u_2, u_4} R (fun (x : ι) ↦ M) N))
    (Set.range toContinuousMultilinearMap)
    {f : ContinuousMultilinearMap.{u_1, u_6, u_2, u_4} R (fun (x : ι) ↦ M) N |
      ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → Eq.{u_4 + 1} (α := N) ((f : (a : (i : ι) → M) → N) v : N) (0 : N)}

Tactic:
Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.2, fun h => ⟨⟨f, h⟩, rfl⟩⟩

Premises used: Set.ext, ContinuousAlternatingMap.mk, setOf, Membership.mem, Eq.rec, ContinuousAlternatingMap.map_eq_zero_of_eq', Iff.intro, Exists.intro, _private.0.ContinuousAlternatingMap.range_toContinuousMultilinearMap.match_1, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
⊢ Continuous (X := ι → M) (Y := N) (⇑f : (a : ι → M) → N)

Tactic:
f.cont

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.cont
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
⊢ Eq (α := (a : (i : ι) → M) → N) (⇑f.toContinuousMultilinearMap : (a : (i : ι) → M) → N) (⇑f : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : ContinuousMultilinearMap.{u_1, u_6, u_2, u_4} R (fun (x : ι) ↦ M) N
h :
  ∀ (v : ι → M) (i j : ι),
    v i = v j → i ≠ j → f.toMultilinearMap (M₁ := fun (x : ι) ↦ M).toFun (M₁ := fun (x : ι) ↦ M) v = 0
⊢ Eq (α := (a : ι → M) → N)
    (⇑{ toContinuousMultilinearMap := f, map_eq_zero_of_eq' := h : M [⋀^ι]→L[R] N } : (a : ι → M) → N)
    (⇑f : (a : (i : ι) → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
⊢ Eq (α := (a : ι → M) → N) (⇑f.toAlternatingMap : (a : ι → M) → N) (⇑f : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
H : ∀ (x : ι → M), Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) x : N) ((g : (a : ι → M) → N) x : N)
⊢ f = g

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
h : f.toAlternatingMap = g.toAlternatingMap
⊢ Eq (α := (a : ι → M) → N) (⇑f.toAlternatingMap : (a : ι → M) → N) (⇑g.toAlternatingMap : (a : ι → M) → N)

Tactic:
DFunLike.ext'_iff.1 h

Premises used: DFunLike.ext'_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f g : M [⋀^ι]→L[R] N
h : f.toAlternatingMap = g.toAlternatingMap
⊢ Eq (α := (a : ι → M) → N) (⇑f : (a : ι → M) → N) (⇑g : (a : ι → M) → N)

Tactic:
convert! DFunLike.ext'_iff.1 h

Premises used: DFunLike.ext'_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
⊢ Eq (α := Set (M [⋀^ι]→ₗ[R] N)) (Set.range (ι := M [⋀^ι]→L[R] N) toAlternatingMap)
    {f : M [⋀^ι]→ₗ[R] N | Continuous (X := ι → M) (Y := N) (⇑f : (a : ι → M) → N)}

Tactic:
Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.cont, fun h => ⟨{ f with cont := h }, DFunLike.ext' rfl⟩⟩

Premises used: Set.ext, Continuous, ContinuousAlternatingMap.mk, AlternatingMap.map_eq_zero_of_eq', setOf, Membership.mem, Eq.rec, _private.0.ContinuousAlternatingMap.range_toAlternatingMap.match_1, AlternatingMap.toMultilinearMap, ContinuousMultilinearMap.mk, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.cont, Iff.intro, Exists.intro, DFunLike.ext', DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
m : ι → M
i : ι
x y : M
⊢ (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i (x + y)) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i x) : N)
      ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i y) : N)

Tactic:
f.map_update_add' m i x y

Premises used: MultilinearMap.map_update_add', ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
m : ι → M
i : ι
c : R
x : M
⊢ (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i (c • x)) =
    HSMul.hSMul (β := N) c ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i x) : N)

Tactic:
f.map_update_smul' m i c x

Premises used: MultilinearMap.map_update_smul', ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
m : ι → M
i : ι
h : m i = 0
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) m : N) (0 : N)

Tactic:
f.toMultilinearMap.map_coord_zero i h

Premises used: ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap, MultilinearMap.map_coord_zero
-- Module: Mathlib.Topology.Algebra.Module.Alternating.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : TopologicalSpace N
f : M [⋀^ι]→L[R] N
inst_7 : DecidableEq ι
m : ι → M
i : ι
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i 0) : N) (0 : N)

Tactic:
f.toMultilinearMap.map_update_zero m i

Premises used: MultilinearMap.map_update_zero, ContinuousAlternatingMap.toContinuousMultilinearMap, ContinuousMultilinearMap.toMultilinearMap