awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : (↑e : X → Y) x = (↑e : X → Y) y
refine_1 : x = (↑e.symm : Y → X) ((↑e : X → Y) y)
refine_1₁ : (↑e.symm : Y → X) ((↑e : X → Y) x) = (↑e.symm : Y → X) ((↑e : X → Y) y)
⊢ x = y
have refine_1₂ : (↑e.symm : Y → X) ((↑e : X → Y) y) = (↑e.symm : Y → X) ((↑e : X → Y) y)
Tactic: rw [← left_inv e hy, ← left_inv e (hs'' hx), h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
hs' : IsOpen[inst_1] ((↑e : X → Y) '' s)
hs'' : s ⊆ e.source
⊢ EqOn (↑((e.restr s).symm.trans e') : Y → Y) (↑((e.symm.trans e').restr ((↑e : X → Y) '' s)) : Y → Y)
    ((e.restr s).symm.trans e').source
have refine_2 : EqOn ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) ((↑e' : X → Y) ∘ (↑e.symm : Y → X)) ((e.restr s).symm.trans e').source
Tactic: simp_rw [coe_trans, restr_symm_apply, restr_apply, coe_trans]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
⊢ IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have rw : IsOpen[inst_1] ((↑e' : X → Y) '' (e'.source ∩ s))
Tactic: rw [← image_source_inter_eq']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (hypothesis)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: have ht : IsOpen (e'.target ∩ e'.symm ⁻¹' s) := by
    rw [← image_source_inter_eq']
    exact isOpen_image_source_inter e' hs
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1 : (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)).source
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)).source
⊢ e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_2 : EqOn (↑(e'.symm.trans (e.restr s)) : Y → Y) (↑((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)) : Y → Y)
  (e'.symm.trans (e.restr s)).source
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ (e'.symm.trans (e.restr s)).source = ((e'.symm.trans e).restr (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)).source
have refine_1 : e'.target ∩ ((↑e'.symm : Y → X) ⁻¹' e.source ∩ (↑e'.symm : Y → X) ⁻¹' interior s) =
  e'.target ∩ (↑e'.symm : Y → X) ⁻¹' e.source ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, coe_coe_symm, PartialEquiv.restr_source,
      preimage_inter]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ ((↑e'.symm : Y → X) ⁻¹' e.source ∩ (↑e'.symm : Y → X) ⁻¹' interior s) =
    e'.target ∩ (↑e'.symm : Y → X) ⁻¹' e.source ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1 : (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s) =
  (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
Tactic: rw [interior_eq_iff_isOpen.mpr hs,
      ← inter_assoc, inter_comm e'.target, inter_assoc, inter_assoc]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s) =
    (↑e'.symm : Y → X) ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
have refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: nth_rw 2 [← interior_eq_iff_isOpen.mpr e'.open_target]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
Tactic: rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1₁ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
refine_1₁ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1₂ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
Tactic: rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Composition (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst] s
ht : IsOpen[inst_1] (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1 : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s))
refine_1₁ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
refine_1₂ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
⊢ e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = interior e'.target ∩ interior (e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s)
have refine_1₃ : e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s = e'.target ∩ (↑e'.symm : Y → X) ⁻¹' s
Tactic: rw [← interior_inter, ← inter_assoc, inter_self, interior_eq_iff_isOpen.mpr ht]
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
have pos : ∀ (hab : a = b), ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
Tactic: by_cases! hab : a = b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
pos : ∀ (hab : a = b), ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
have neg : ∀ (hab : a ≠ b), ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
Tactic: by_cases! hab : a = b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
have neg : Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: apply continuousOn_extendFrom
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
neg : Icc a b ⊆ closure[inst] (Ioo a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
have neg₁ : ∀ x ∈ Icc a b, ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Tactic: apply continuousOn_extendFrom
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have neg : Icc a b ⊆ Icc a b
Tactic: rw [closure_Ioo hab]
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
have neg : ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x ≠ b) (x_in : x ∈ Icc x b),
  ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
Cleared hypotheses: a, hf, ha, hab, x_in
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
neg :
  ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x ≠ b) (x_in : x ∈ Icc x b),
    ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
have neg₁ : ∀ (hf : ContinuousOn f (Ioo a x)) (hb : Tendsto f (𝓝[<] x) (𝓝 lb)) (hab : a ≠ x) (x_in : x ∈ Icc a x),
  ∃ (y : β), Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
Cleared hypotheses: b, hf, hb, hab, x_in
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
hab : a ≠ b
x : α
x_in : x ∈ Icc a b
neg :
  ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x ≠ b) (x_in : x ∈ Icc x b),
    ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
neg₁ :
  ∀ (hf : ContinuousOn f (Ioo a x)) (hb : Tendsto f (𝓝[<] x) (𝓝 lb)) (hab : a ≠ x) (x_in : x ∈ Icc a x),
    ∃ (y : β), Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
have neg₂ : ∀ (h : x ∈ Ioo a b), ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have pos : ∀ (hab : a = b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Tactic: by_cases! hab : a = b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
pos : ∀ (hab : a = b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have neg : ∀ (hab : a ≠ b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Tactic: by_cases! hab : a = b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have neg : ∀ (hab' : a < b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Tactic: obtain hab' | hba' := hab.lt_or_gt
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
neg : ∀ (hab' : a < b), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have neg₁ : ∀ (hba' : b < a), ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
Tactic: obtain hab' | hba' := hab.lt_or_gt
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hab' : a < b
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have neg : ∀ (ha : Tendsto f (𝓝[>] a) (𝓝 la)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) (hf : ContinuousOn f (Ioo a b)),
  ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
Tactic: simp only [hab', uIoo_of_lt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_lt] at ha hb hf ⊢
Cleared hypotheses: hf, ha, hb
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (uIoo a b)
ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)
hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)
hab : a ≠ b
hba' : b < a
⊢ ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b)
have neg : ∀ (ha : Tendsto f (𝓝[<] a) (𝓝 la)) (hb : Tendsto f (𝓝[>] b) (𝓝 lb)) (hf : ContinuousOn f (Ioo b a)),
  ContinuousOn (extendFrom (Ioo b a) f) (Icc b a)
Tactic: simp only [hba', uIoo_of_gt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
      uIcc_of_gt] at ha hb hf ⊢
Cleared hypotheses: hf, ha, hb
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
have pos : ∀ (hab : a ≥ b), ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
Tactic: by_cases! hab : a ≥ b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
pos : ∀ (hab : a ≥ b), ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
have neg : ∀ (hab : a < b), ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
Tactic: by_cases! hab : a ≥ b
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
have neg : Ico a b ⊆ closure[inst] (Ioo a b)
Tactic: apply continuousOn_extendFrom
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
neg : Ico a b ⊆ closure[inst] (Ioo a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
have neg₁ : ∀ x ∈ Ico a b, ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Tactic: apply continuousOn_extendFrom
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
⊢ Ico a b ⊆ closure[inst] (Ioo a b)
have neg : Ico a b ⊆ Icc a b
Tactic: rw [closure_Ioo hab.ne]
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
have neg : ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x < b) (x_in : x ∈ Ico x b),
  ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
Tactic: rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)
Cleared hypotheses: a, hf, ha, hab, x_in
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
la : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 la)
hab : a < b
x : α
x_in : x ∈ Ico a b
neg :
  ∀ (hf : ContinuousOn f (Ioo x b)) (ha : Tendsto f (𝓝[>] x) (𝓝 la)) (hab : x < b) (x_in : x ∈ Ico x b),
    ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
have neg₁ : ∀ (h : x ∈ Ioo a b), ∃ (y : β), Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
Tactic: rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
b : α
la : β
inst_5 : RegularSpace β
x : α
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[>] x) (𝓝 la)
hab : x < b
x_in : x ∈ Ico x b
⊢ ∃ (y : β), Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
have h : Tendsto f (𝓝[Ioo x b] x) (𝓝 la)
Tactic: use la
-- Lean 4 proof step from Mathlib.Topology.Order.ExtendFrom (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
f : α → β
a b : α
lb : β
inst_5 : RegularSpace β
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
have this : ∀
  (hf :
    ContinuousOn (X := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
      (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ))
  (ha :
    Tendsto (α := αᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α) : αᵒᵈ → β)
      (𝓝[>] (OrderDual.toDual : (a : α) → αᵒᵈ) b : Filter αᵒᵈ) (𝓝 lb)),
  ContinuousOn (X := αᵒᵈ)
    (extendFrom (Ioo ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a))
        (f ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) :
      αᵒᵈ → β)
    (Ico ((OrderDual.toDual : (a : α) → αᵒᵈ) b) ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
Tactic: have := continuousOn_Ico_extendFrom_Ioo (f := f ∘ OrderDual.ofDual) (a := OrderDual.toDual b)
    (b := OrderDual.toDual a) (la := lb)