awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set (↑(Icc a b) : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑(Icc a b) : Type)) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑(Icc a b) : Type)), Membership.mem (γ := Set (↑(Icc a b) : Type)) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ (t : ℕ → (↑(Icc a b) : Type)),
    (↑(t 0) : ℝ) = a ∧
      Monotone t ∧ (∃ (m : ℕ), ∀ n ≥ m, (↑(t n) : ℝ) = b) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
have refine : ∀ (n : ℕ), ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
Tactic: refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
a b : ℝ
h : a ≤ b
c : ι → Set (↑(Icc a b) : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑(Icc a b) : Type)) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑(Icc a b) : Type)), Membership.mem (γ := Set (↑(Icc a b) : Type)) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
n : ℕ
⊢ ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
have obtain : ∀ (i : ι) (hsub : Metric.ball (addNSMul h (δ / 2) n) δ ⊆ c i),
  ∃ (i : ι), Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ⊆ c i
Tactic: obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n) trivial
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
c : ι → Set (↑I : Type)
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set (↑I : Type)) univ (⋃ (i : ι), c i)
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧ Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
have simp_rw : ∃ (t : ℕ → (↑I : Type)),
  (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
    Monotone t ∧ (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧ ∀ (n : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ⊆ c i
Tactic: simp_rw [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
have obtain : ∀ (δ : ℝ) (δ_pos : δ > 0)
  (ball_subset :
    ∀ (x : (↑I : Type) × (↑I : Type)),
      Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i),
  ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
Tactic: obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
have hδ : 0 < δ / 2
Tactic: have hδ := half_pos δ_pos
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ (t : ℕ → (↑I : Type)),
    t 0 = 0 ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
have simp_rw : ∃ (t : ℕ → (↑I : Type)),
  (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
    Monotone t ∧
      (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
        ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
Tactic: simp_rw [Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (hypothesis)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
          ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
have h : LE.le (α := ℝ) 0 1
Tactic: have h : (0 : ℝ) ≤ 1 := zero_le_one
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
⊢ ∃ (t : ℕ → (↑I : Type)),
    (↑(t 0) : ℝ) = (↑0 : ℝ) ∧
      Monotone t ∧
        (∃ (n : ℕ), ∀ m ≥ n, (↑(t m) : ℝ) = (↑1 : ℝ)) ∧
          ∀ (n m : ℕ), ∃ (i : ι), Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
have refine : ∀ (n m : ℕ),
  ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i
Tactic: refine ⟨addNSMul h (δ/2), addNSMul_zero h,
    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
ι : Sort u_1
c : ι → Set ((↑I : Type) × (↑I : Type))
hc₁ : ∀ (i : ι), IsOpen (c i)
hc₂ : Subset (α := Set ((↑I : Type) × (↑I : Type))) univ (⋃ (i : ι), c i)
δ : ℝ
δ_pos : δ > 0
ball_subset :
  ∀ (x : (↑I : Type) × (↑I : Type)),
    Membership.mem (γ := Set ((↑I : Type) × (↑I : Type))) univ x → ∃ (i : ι), Metric.ball x δ ⊆ c i
hδ : 0 < δ / 2
h : LE.le (α := ℝ) 0 1
n m : ℕ
⊢ ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i
have obtain : ∀ (i : ι) (hsub : Metric.ball (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) δ ⊆ c i),
  ∃ (i : ι),
    Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆
      c i
Tactic: obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
⊢ (↑(Icc a b) : Type u_1) ≃ₜ (↑(Icc 0 1) : Type u_1)
have refine : (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a sorry) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) ≃ₜ (↑(Icc a b) : Type u_1)
Tactic: refine (e.trans ?_).symm
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
⊢ (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) ≃ₜ (↑(Icc a b) : Type u_1)
have h₁ : image (α := 𝕜) (⇑(affineHomeomorph (b - a) a sorry) : (a : 𝕜) → 𝕜) (Icc 0 1) = Icc a b
Tactic: apply Homeomorph.setCongr
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : IsTopologicalRing 𝕜
a b : 𝕜
h : a < b
e : (↑(Icc 0 1) : Type u_1) ≃ₜ
  (↑(image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1)) : Type u_1) :=
  Homeomorph.image (affineHomeomorph (b - a) a ⋯) (Icc 0 1)
⊢ image (α := 𝕜) (⇑(affineHomeomorph (b - a) a ⋯) : (a : 𝕜) → 𝕜) (Icc 0 1) = Icc a b
have h₁ : Icc a (b - a + a) = Icc a b
Tactic: rw [affineHomeomorph_image_I _ _ (sub_pos.2 h)]
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : (↑I : Type)
⊢ toNNReal x + toNNReal (σ x) = 1
have a : (↑(toNNReal x + toNNReal (σ x)) : ℝ) = (↑1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UnitInterval (goal)
Goal:
x : (↑I : Type)
⊢ toNNReal (σ x) + toNNReal x = 1
have a : (↑(toNNReal (σ x) + toNNReal x) : ℝ) = (↑1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UrysohnsBounded (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
⊢ a ≤ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x
have dsimp : a ≤ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.UrysohnsBounded (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
⊢ a ≤ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)
have nlinarith : a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) < a →
  a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) - a +
      (0 - (a - b) * HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)) =
    0
Tactic: nlinarith [(hf01 x).1]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsBounded (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
⊢ (BoundedContinuousFunction.const X a + (b - a) • f : (a : X) → ℝ) x ≤ b
have dsimp : a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) ≤ b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.UrysohnsBounded (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 s
hft : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 t
hf01 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
x : X
⊢ a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) ≤ b
have nlinarith : b < a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ) →
  b - (a + HMul.hMul (β := ℝ) (b - a) ((f : (a : X) → ℝ) x : ℝ)) +
      (0 - (a - b) * HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)) =
    0
Tactic: nlinarith [(hf01 x).2]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 0
have succ : x ∈ c.right (P := P).C (P := P)
Tactic: rw [ihn, ihn, midpoint_self]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0
c : CU P
hx : x ∈ c.C (P := P)
succ : x ∈ c.right (P := P).C (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 0
have succ₁ : x ∈ c.left (P := P).C (P := P)
Tactic: rw [ihn, ihn, midpoint_self]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C (P := P)
⊢ approx (P := P) n c x = 0
have zero : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) 0 c x = 0
Tactic: induction n generalizing c with
  | zero => exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]
Cleared hypotheses: c, n, hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∈ c.C (P := P)
zero : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) 0 c x = 0
⊢ approx (P := P) n c x = 0
have succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P) (hx : x ∈ c.C (P := P)), approx (P := P) n c x = 0) (c : CU P) (hx : x ∈ c.C (P := P)),
  approx (P := P) (n + 1) c x = 0
Tactic: induction n generalizing c with
  | zero => exact indicator_of_notMem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]
Cleared hypotheses: c, n, hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
hx : x ∉ c.U (P := P)
⊢ approx (P := P) 0 c x = 1
have hx₁ : x ∈ (c.U (P := P))ᶜ
Tactic: rw [← mem_compl_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 1
have succ : x ∉ c.right (P := P).U (P := P)
Tactic: rw [ihn, ihn, midpoint_self]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1
c : CU P
hx : x ∉ c.U (P := P)
succ : x ∉ c.right (P := P).U (P := P)
⊢ midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) = 1
have succ₁ : x ∉ c.left (P := P).U (P := P)
Tactic: rw [ihn, ihn, midpoint_self]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U (P := P)
⊢ approx (P := P) n c x = 1
have zero : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) 0 c x = 1
Tactic: induction n generalizing c with
  | zero =>
    rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]
Cleared hypotheses: c, n, hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U (P := P)
zero : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) 0 c x = 1
⊢ approx (P := P) n c x = 1
have succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P) (hx : x ∉ c.U (P := P)), approx (P := P) n c x = 1) (c : CU P) (hx : x ∉ c.U (P := P)),
  approx (P := P) (n + 1) c x = 1
Tactic: induction n generalizing c with
  | zero =>
    rw [← mem_compl_iff] at hx
    exact indicator_of_mem hx _
  | succ n ihn =>
    simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]
Cleared hypotheses: c, n, hx
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
⊢ 0 ≤ approx (P := P) (n + 1) c x
have succ : 0 ≤
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)
Tactic: simp only [approx, midpoint_eq_smul_add]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
⊢ 0 ≤
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)
have succ : 0 ≤ approx (P := P) n (c.left (P := P)) x
Tactic: refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x
c : CU P
succ : 0 ≤ approx (P := P) n (c.left (P := P)) x
⊢ 0 ≤
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x)
have succ₁ : 0 ≤ approx (P := P) n (c.right (P := P)) x
Tactic: refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ 0 ≤ approx (P := P) n c x
have zero : ∀ (c : CU P), 0 ≤ approx (P := P) 0 c x
Tactic: induction n generalizing c with
  | zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero : ∀ (c : CU P), 0 ≤ approx (P := P) 0 c x
⊢ 0 ≤ approx (P := P) n c x
have succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P), 0 ≤ approx (P := P) n c x) (c : CU P), 0 ≤ approx (P := P) (n + 1) c x
Tactic: induction n generalizing c with
  | zero => exact indicator_nonneg (fun _ _ => zero_le_one) _
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add]
    refine mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg ?_ ?_) <;> apply ihn
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
⊢ approx (P := P) (n + 1) c x ≤ 1
have succ : (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1
Tactic: simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
⊢ (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1
have this : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ HAdd.hAdd (α := ℝ) 1 1
Tactic: have := add_le_add (ihn (left c)) (ihn (right c))
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1
c : CU P
this : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ HAdd.hAdd (α := ℝ) 1 1
⊢ (approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x) / 2 ≤ 1
have this₁ : approx (P := P) n (c.left (P := P)) x + approx (P := P) n (c.right (P := P)) x ≤ 2
Tactic: norm_num at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx (P := P) n c x ≤ 1
have zero : ∀ (c : CU P), approx (P := P) 0 c x ≤ 1
Tactic: induction n generalizing c with
  | zero => exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
    have := add_le_add (ihn (left c)) (ihn (right c))
    norm_num at this
    exact Iff.mpr (div_le_one zero_lt_two) this
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c : CU P
n : ℕ
x : X
zero : ∀ (c : CU P), approx (P := P) 0 c x ≤ 1
⊢ approx (P := P) n c x ≤ 1
have succ : ∀ (n : ℕ) (ihn : ∀ (c : CU P), approx (P := P) n c x ≤ 1) (c : CU P), approx (P := P) (n + 1) c x ≤ 1
Tactic: induction n generalizing c with
  | zero => exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
  | succ n ihn =>
    simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
    have := add_le_add (ihn (left c)) (ihn (right c))
    norm_num at this
    exact Iff.mpr (div_le_one zero_lt_two) this
Cleared hypotheses: c, n
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
⊢ approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
have pos : ∀ (hx : x ∈ c₁.U (P := P)), approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
Tactic: by_cases hx : x ∈ c₁.U
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
c₁ c₂ : CU P
h : c₁.U (P := P) ⊆ c₂.C (P := P)
n₁ n₂ : ℕ
x : X
pos : ∀ (hx : x ∈ c₁.U (P := P)), approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
⊢ approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
have neg : ∀ (hx : x ∉ c₁.U (P := P)), approx (P := P) n₂ c₂ x ≤ approx (P := P) n₁ c₁ x
Tactic: by_cases hx : x ∈ c₁.U
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ Membership.mem (γ := Set ℝ)
    (Icc ((c.right (P := P).U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x))
    ((c.U (P := P))ᶜ.indicator 1 x)
have zero : LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)
Tactic: refine ⟨le_rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
c : CU P
⊢ LE.le (α := ℝ) ((c.U (P := P))ᶜ.indicator 1 x) ((c.left (P := P).U (P := P))ᶜ.indicator 1 x)
have h₂ : LE.le (α := ℝ) 0 (1 x)
Tactic: grw [left_U_subset]
-- Lean 4 proof step from Mathlib.Topology.UrysohnsLemma (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn :
  ∀ (c : CU P),
    approx (P := P) n c x ∈ Icc (approx (P := P) n (c.right (P := P)) x) (approx (P := P) n (c.left (P := P)) x)
c : CU P
⊢ midpoint ℝ (approx (P := P) n (c.right (P := P).left (P := P)) x)
        (approx (P := P) n (c.right (P := P).right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ∧
    midpoint ℝ (approx (P := P) n (c.left (P := P)) x) (approx (P := P) n (c.right (P := P)) x) ≤
      midpoint ℝ (approx (P := P) n (c.left (P := P).left (P := P)) x)
        (approx (P := P) n (c.left (P := P).right (P := P)) x)
have succ : approx (P := P) n (c.right (P := P).left (P := P)) x ≤ approx (P := P) n (c.left (P := P)) x
Tactic: refine ⟨midpoint_le_midpoint ?_ (ihn _).1, midpoint_le_midpoint (ihn _).2 ?_⟩