awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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 + (↑(K' (↑z : α) ⋯) : ENNReal) * edist (↑z : α) y ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y)
have bc : edist (↑z : α) y ≤ edist x (↑z : α) + edist x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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 + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x (↑z : α) + edist x y) ≤
    (↑(K (↑z : α) ⋯) : ENNReal) * edist x y + (↑(K' (↑z : α) ⋯) : ENNReal) * (edist x y + edist x y)
have simp_rw : (↑(K (↑z : α) sorry) : ENNReal) * ENNReal.ofReal (dist x (↑z : α)) +
    (↑(K' (↑z : α) sorry) : ENNReal) * (ENNReal.ofReal (dist x (↑z : α)) + ENNReal.ofReal (dist x y)) ≤
  (↑(K (↑z : α) sorry) : ENNReal) * ENNReal.ofReal (dist x y) +
    (↑(K' (↑z : α) sorry) : ENNReal) * (ENNReal.ofReal (dist x y) + ENNReal.ofReal (dist x y))
Tactic: simp_rw [edist_dist, dist_comm _ x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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) * 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))
have h₁ : dist x (↑z : α) ≤ dist x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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 : α) ⋯)
⊢ dist x (↑z : α) ≤ dist x y
have linarith : dist x y < dist x (↑z : α) → 2 / 2 = 1
Tactic: linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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
⊢ dist x (↑z : α) ≤ dist x y
have linarith₁ : dist x y < dist x (↑z : α) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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
⊢ dist x (↑z : α) ≤ dist x y
have linarith₂ : dist x y < dist x (↑z : α) → GT.gt (α := ℝ) 2 0
Tactic: linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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
⊢ dist x (↑z : α) ≤ dist x y
have linarith₃ : dist x y < dist x (↑z : α) →
  dist x y - dist x (↑z : α) + (2 * dist x (↑z : α) - 1 * ε (↑z : α) sorry) + (ε (↑z : α) sorry - dist y (↑z : α)) +
      (dist y (↑z : α) - (dist x y + dist x (↑z : α))) =
    0
Tactic: linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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 : α) ⋯) : ENNReal) * edist x y ≤
    (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have bc : K (↑z : α) sorry + 2 * K' (↑z : α) sorry ≤ t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have calc : (↑(K (↑z : α) sorry) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) sorry) : ENNReal) * edist (↑z : α) y ≤
  (↑(K (↑z : α) sorry) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) sorry) : ENNReal) * (edist x (↑z : α) + 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have calc₁ : (↑(K (↑z : α) sorry) : ENNReal) * edist (↑z : α) x + (↑(K' (↑z : α) sorry) : ENNReal) * (edist x (↑z : α) + edist x y) ≤
  (↑(K (↑z : α) sorry) : ENNReal) * edist x y + (↑(K' (↑z : α) sorry) : ENNReal) * (edist x y + 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have calc₂ : (↑(K (↑z : α) sorry) : ENNReal) * edist x y + (↑(K' (↑z : α) sorry) : ENNReal) * (edist x y + edist x y) =
  (↑(K (↑z : α) sorry + 2 * K' (↑z : α) sorry) : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
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
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have calc₃ : (↑(K (↑z : α) sorry + 2 * K' (↑z : α) sorry) : ENNReal) * edist x y ≤
  (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) : 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)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M [⋀^ι]→L[R] N
⊢ (fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M'))
      ((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M)) f) =
    f
have H : ∀ (x : ι → M),
  Eq.{u_4 + 1} (α := N)
    (((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M'))
            ((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M)) f) :
          (a : ι → M) → N)
        x :
      N)
    ((f : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : M ≃L[R] M'
f : M' [⋀^ι]→L[R] N
⊢ (fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M))
      ((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M')) f) =
    f
have H : ∀ (x : ι → M'),
  Eq.{u_4 + 1} (α := N)
    (((fun (f : M [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e.symm : M' →L[R] M))
            ((fun (f : M' [⋀^ι]→L[R] N) ↦ f.compContinuousLinearMap (↑e : M →L[R] M')) f) :
          (a : ι → M') → N)
        x :
      N)
    ((f : (a : ι → M') → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
⊢ (↑e.symm : N' →L[R] N).compContinuousAlternatingMap ((↑e : N →L[R] N').compContinuousAlternatingMap f) = f
have H : ∀ (x : ι → M),
  Eq.{u_4 + 1} (α := N)
    (((↑e.symm : N' →L[R] N).compContinuousAlternatingMap ((↑e : N →L[R] N').compContinuousAlternatingMap f) :
          (a : ι → M) → N)
        x :
      N)
    ((f : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : AddCommMonoid N'
inst_11 : Module R N'
inst_12 : TopologicalSpace N'
n : ℕ
f_1 g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
⊢ (↑e : N →L[R] N').compContinuousAlternatingMap ((↑e.symm : N' →L[R] N).compContinuousAlternatingMap f) = f
have H : ∀ (x : ι → M),
  Eq.{u_5 + 1} (α := N')
    (((↑e : N →L[R] N').compContinuousAlternatingMap ((↑e.symm : N' →L[R] N).compContinuousAlternatingMap f) :
          (a : ι → M) → N')
        x :
      N')
    ((f : (a : ι → M) → N') x : N')
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
x y : M
v : Fin n → M
⊢ (f : (a : Fin (n + 1) → M) → N) (vecCons (x - y) v) =
    HSub.hSub (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x v) : N)
      ((f : (a : Fin (n + 1) → M) → N) (vecCons y v) : N)
have rw : HSub.hSub (α := N) (β := N)
    ((f : (a : Fin (n + 1) → M) → N)
        (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 x) :
      N)
    ((f : (a : Fin (n + 1) → M) → N)
        (update (β := fun (a : Fin (n + 1)) ↦ M) (Fin.cons (α := fun (a : Fin n.succ) ↦ M) 0 v) 0 y) :
      N) =
  HSub.hSub (α := N) (β := N) ((f : (a : Fin (n + 1) → M) → N) (vecCons x v) : N)
    ((f : (a : Fin (n + 1) → M) → N) (vecCons y v) : N)
Tactic: rw [vecCons, ← Fin.update_cons_zero 0, map_update_sub]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Alternating.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
inst_6 : TopologicalSpace M'
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : TopologicalSpace N
inst_10 : ContinuousAdd N
inst_11 : ContinuousConstSMul R N
inst_12 : AddCommMonoid N'
inst_13 : Module R N'
inst_14 : TopologicalSpace N'
inst_15 : ContinuousAdd N'
inst_16 : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M' [⋀^ι]→L[R] N
⊢ (g + g').compContinuousLinearMap f = g.compContinuousLinearMap f + g'.compContinuousLinearMap f
have H : ∀ (x : ι → M),
  Eq.{u_4 + 1} (α := N) (((g + g').compContinuousLinearMap f : (a : ι → M) → N) x : N)
    ((g.compContinuousLinearMap f + g'.compContinuousLinearMap f : (a : ι → M) → N) x : N)
Tactic: ext