awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inl : ∀ (x : X) (ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ))
  (hmem :
    ∀ (x_1 : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ))
  (hle : (f : (a : X) → ℝ) x ≤ b) (hlt : (f : (a : X) → ℝ) x < b),
  let c := HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) b / 2;
  ∀ (hac : (f : (a : X) → ℝ) x < c) (hcb : c < b) (hsub : HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ) = b - c)
    (hg_mem :
      ∀ (y : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases em (∃ x, f x = a) with (⟨x, rfl⟩ | ha')
Cleared hypotheses: a, ha, hmem, hle, hlt, c, hac, hcb, hsub, hg_mem
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
inl :
  ∀ (x : X) (ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ))
    (hmem :
      ∀ (x_1 : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ))
    (hle : (f : (a : X) → ℝ) x ≤ b) (hlt : (f : (a : X) → ℝ) x < b),
    let c := HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) b / 2;
    ∀ (hac : (f : (a : X) → ℝ) x < c) (hcb : c < b) (hsub : HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ) = b - c)
      (hg_mem :
        ∀ (y : Y),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)),
      ∃ (g : Y →ᵇ ℝ),
        (∀ (y : Y),
            ∃ (x : X),
              Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
          Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases em (∃ x, f x = a) with (⟨x, rfl⟩ | ha')
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
⊢ Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
have refine_1 : Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
Tactic: refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
refine_1 : Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
⊢ Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
have refine_2 : Disjoint (Ici c) {a}
Tactic: refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
⊢ Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
have refine_1 : ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a}
Tactic: rw [Set.disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
Tactic: have hd : Disjoint (range e ∪ g ⁻¹' Ici c) (g ⁻¹' {a}) := by
      refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
      · rw [Set.disjoint_left]
        rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)
        exact ha' ⟨x, (congr_fun hgf x).symm⟩
      · exact Set.disjoint_singleton_right.2 hac.not_ge
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (dg : Y →ᵇ ℝ) (dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c))
  (dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a}))
  (dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases exists_bounded_mem_Icc_of_closed_of_le
        (he.isClosed_range.union <| isClosed_Ici.preimage g.continuous)
        (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hac.le) with
      ⟨dg, dg0, dga, dgmem⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hgf₁ : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: replace hgf : ∀ x, (g + dg) (e x) = f x := by
      intro x
      simp [dg0 (Or.inl <| mem_range_self _), ← hgf]
Cleared hypotheses: hgf
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (y : Y),
  ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
Tactic: refine ⟨g + dg, fun y => ?_, funext hgf⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
⊢ a < (g + dg : (a : Y) → ℝ) y
have inl : ∀ (ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ))
  (hmem :
    ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((f : (a : X) → ℝ) x : ℝ))
  (hle : (g : (a : Y) → ℝ) y ≤ b) (hlt : (g : (a : Y) → ℝ) y < b),
  let c := HAdd.hAdd (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) b / 2;
  ∀ (hac : (g : (a : Y) → ℝ) y < c) (hcb : c < b) (hsub : HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ) = b - c)
    (hg_mem :
      ∀ (y_1 : Y),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((g : (a : Y) → ℝ) y_1 : ℝ))
    (ha' : ¬∃ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : Y) → ℝ) y : ℝ))
    (hd :
      Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
        (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ))))
    (dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c))
    (dga :
      EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ)))
        (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ))))
    (dgmem :
      ∀ (x : Y),
        Membership.mem (α := ℝ) (Icc 0 (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ))) ((dg : (a : Y) → ℝ) x : ℝ)),
    LT.lt (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
Tactic: rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
Cleared hypotheses: a, ha, hmem, hle, hlt, c, hac, hcb, hsub, hg_mem, ha', hd, dg0, dga, dgmem
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
inl :
  ∀ (ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ))
    (hmem :
      ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((f : (a : X) → ℝ) x : ℝ))
    (hle : (g : (a : Y) → ℝ) y ≤ b) (hlt : (g : (a : Y) → ℝ) y < b),
    let c := HAdd.hAdd (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) b / 2;
    ∀ (hac : (g : (a : Y) → ℝ) y < c) (hcb : c < b) (hsub : HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ) = b - c)
      (hg_mem :
        ∀ (y_1 : Y),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((g : (a : Y) → ℝ) y_1 : ℝ))
      (ha' : ¬∃ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : Y) → ℝ) y : ℝ))
      (hd :
        Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
          (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ))))
      (dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c))
      (dga :
        EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ)))
          (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ))))
      (dgmem :
        ∀ (x : Y),
          Membership.mem (α := ℝ) (Icc 0 (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ))) ((dg : (a : Y) → ℝ) x : ℝ)),
      LT.lt (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
⊢ a < (g + dg : (a : Y) → ℝ) y
have inr : ∀ (hlt : a < (g : (a : Y) → ℝ) y), a < (g + dg : (a : Y) → ℝ) y
Tactic: rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
g dg : Y →ᵇ ℝ
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hmem : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hle : (g : (a : Y) → ℝ) y ≤ b
hlt : (g : (a : Y) → ℝ) y < b
c : ℝ := HAdd.hAdd (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) b / 2
hac : (g : (a : Y) → ℝ) y < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ) = b - c
hg_mem :
  ∀ (y_1 : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) y) b : Set ℝ) ((g : (a : Y) → ℝ) y_1 : ℝ)
ha' : ¬∃ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hd :
  Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
    (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ)))
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga :
  EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ)))
    (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ)))
dgmem :
  ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) y : ℝ))) ((dg : (a : Y) → ℝ) x : ℝ)
⊢ LT.lt (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
have inl : LT.lt (α := ℝ) (0 : ℝ) ((dg : (a : Y) → ℝ) y : ℝ)
Tactic: refine (lt_add_iff_pos_right _).2 ?_
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
⊢ ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
have hay : a < (g + dg : (a : Y) → ℝ) y
Tactic: have hay : a < (g + dg) y := by
      rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
      · refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm
      · exact hlt.trans_le (le_add_of_nonneg_right (dgmem y).1)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
⊢ ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
have inr : ∀ (x : X),
  a ≤ (f : (a : X) → ℝ) x →
    ∀ (hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)),
      ∃ (x : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
Tactic: rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩