awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.TietzeExtension
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
inhabit :
  ∀ (inhabited_h : Inhabited X),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
inhabit X
-- Module: Mathlib.Topology.TietzeExtension
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 : ℝ), IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a

Tactic:
⟨_, isGLB_ciInf f.isBounded_range.bddBelow⟩

Premises used: Bornology.IsBounded.bddBelow, isGLB_ciInf, BoundedContinuousFunction.isBounded_range, Exists.intro
-- Module: Mathlib.Topology.TietzeExtension
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
obtain :
  ∀ (a : ℝ) (ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := ⟨_, isGLB_ciInf f.isBounded_range.bddBelow⟩
-- Module: Mathlib.Topology.TietzeExtension
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 : ℝ), IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b

Tactic:
⟨_, isLUB_ciSup f.isBounded_range.bddAbove⟩

Premises used: isLUB_ciSup, BoundedContinuousFunction.isBounded_range, Exists.intro, Bornology.IsBounded.bddAbove
-- Module: Mathlib.Topology.TietzeExtension
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
obtain :
  ∀ (b : ℝ) (hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
obtain ⟨b, hb⟩ : ∃ b, IsLUB (range f) b := ⟨_, isLUB_ciSup f.isBounded_range.bddAbove⟩
-- Module: Mathlib.Topology.TietzeExtension
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
⊢ ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
have hmem : ∀ x, f x ∈ Icc a b := fun x => ⟨ha.1 ⟨x, rfl⟩, hb.1 ⟨x, rfl⟩⟩
-- Module: Mathlib.Topology.TietzeExtension
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 : ℝ)
⊢ a ≤ b

Tactic:
have hle : a ≤ b := (hmem default).1.trans (hmem default).2
-- Module: Mathlib.Topology.TietzeExtension
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
inl :
  ∀ (hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a)
    (hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)) (hle : a ≤ a),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
inr :
  ∀ (hlt : a < b),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
rcases hle.eq_or_lt with (rfl | hlt)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.TietzeExtension
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
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
⊢ ∀ (x : X), (f : (a : X) → ℝ) x = a

Tactic:
simpa using hmem
-- Module: Mathlib.Topology.TietzeExtension
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
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
⊢ ∀ (x : X), (f : (a : X) → ℝ) x = a

Tactic:
have : ∀ x, f x = a := by simpa using hmem
-- Module: Mathlib.Topology.TietzeExtension
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
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
this : ∀ (x : X), (f : (a : X) → ℝ) x = a
h :
  (∀ (y : Y),
      ∃ (x₁ : X) (x₂ : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
          ((const Y a : (a : Y) → ℝ) y : ℝ)) ∧
    Eq (α := X → ℝ) ((⇑(const Y a) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
use const Y a

Premises used: BoundedContinuousFunction.const
-- Module: Mathlib.Topology.TietzeExtension
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
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) a
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a a) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ a
this : ∀ (x : X), (f : (a : X) → ℝ) x = a
⊢ (∀ (y : Y),
      ∃ (x₁ : X) (x₂ : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
          ((const Y a : (a : Y) → ℝ) y : ℝ)) ∧
    Eq (α := X → ℝ) ((⇑(const Y a) : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
simp [this, funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Topology.TietzeExtension
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
⊢ a < c

Tactic:
have hac : a < c := left_lt_add_div_two.2 hlt
-- Module: Mathlib.Topology.TietzeExtension
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
⊢ c < b

Tactic:
have hcb : c < b := add_div_two_lt_right.2 hlt
-- Module: Mathlib.Topology.TietzeExtension
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
simp : (a + b) / 2 - a = b - (a + b) / 2
⊢ c - a = b - c

Tactic:
simp [c]
-- Module: Mathlib.Topology.TietzeExtension
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
⊢ (a + b) / 2 - a = b - (a + b) / 2

Tactic:
ring
-- Module: Mathlib.Topology.TietzeExtension
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
⊢ c - a = b - c

Tactic:
have hsub : c - a = b - c := by
    simp [c]
    ring
-- Module: Mathlib.Topology.TietzeExtension
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
rcases :
  ∀ (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) → ℝ)
⊢ ∃ (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_extension_forall_mem_Icc_of_isClosedEmbedding f hmem hle he with ⟨g, hg_mem, hgf⟩

Premises used: BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding
-- Module: Mathlib.Topology.TietzeExtension
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) → ℝ)
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) → ℝ)
⊢ ∃ (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')

Premises used: Exists, em, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Topology.TietzeExtension
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 : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
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:
⟨g, fun y => ⟨x, hg_mem _⟩, hgf⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.TietzeExtension
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 : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
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:
exact ⟨g, fun y => ⟨x, hg_mem _⟩, hgf⟩
-- Module: Mathlib.Topology.TietzeExtension
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})

Tactic:
disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩

Premises used: Iff.mpr, And.intro, Disjoint.preimage, Set.disjoint_union_left
-- Module: Mathlib.Topology.TietzeExtension
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})
refine_2 : Disjoint (Ici c) {a}
⊢ Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})

Tactic:
refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩

Premises used: Iff.mpr, And.intro, Disjoint.preimage, Set.disjoint_union_left
-- Module: Mathlib.Topology.TietzeExtension
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 : ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a}
⊢ Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Topology.TietzeExtension
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 : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
x : X
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hmem :
  ∀ (x_1 : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) (e x)) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : (g : (a : Y) → ℝ) (e x) ≤ b
hlt : (g : (a : Y) → ℝ) (e x) < b
c : ℝ := HAdd.hAdd (α := ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ) b / 2
hac : (g : (a : Y) → ℝ) (e x) < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) (e x) : ℝ) = b - c
hg_mem :
  ∀ (y : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) (e x)) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x_1 : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x_1 : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
⊢ False

Tactic:
ha' ⟨x, (congr_fun hgf x).symm⟩

Premises used: Exists.intro, congr_fun, Eq.symm
-- Module: Mathlib.Topology.TietzeExtension
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 : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
x : X
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hmem :
  ∀ (x_1 : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) (e x)) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : (g : (a : Y) → ℝ) (e x) ≤ b
hlt : (g : (a : Y) → ℝ) (e x) < b
c : ℝ := HAdd.hAdd (α := ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ) b / 2
hac : (g : (a : Y) → ℝ) (e x) < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((g : (a : Y) → ℝ) (e x) : ℝ) = b - c
hg_mem :
  ∀ (y : Y), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((g : (a : Y) → ℝ) (e x)) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x_1 : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x_1 : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
⊢ False

Tactic:
exact ha' ⟨x, (congr_fun hgf x).symm⟩

Premises used: Exists.intro, congr_fun, Eq.symm
-- Module: Mathlib.Topology.TietzeExtension
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 (Ici c) {a}

Tactic:
Set.disjoint_singleton_right.2 hac.not_ge

Premises used: Iff.mpr, Set.disjoint_singleton_right, LT.lt.not_ge