awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬y ≤ x
inr :
  ∀ (U : Set α) (hU : IsClopen U) (hU' : IsLowerSet U) (hy : y ∉ U) (hx : x ∈ U),
    ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h

Premises used: exists_isClopen_lower_of_not_le
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : y ∉ U
hx : x ∈ U
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
⟨U, hU, Or.inr hU', hx, hy⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Topology.Order.Priestley
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : PriestleySpace α
x y : α
h_1 : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : y ∉ U
hx : x ∈ U
⊢ ∃ (U : Set α), IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
exact ⟨U, hU, Or.inr hU', hx, hy⟩
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
a b : α
h : a ≤ b
f : γ → (↑(Icc a b) : Type u_1) → β
la : Filter α
lb : Filter β
lc : Filter γ
hf : Tendsto (↿f) (lc ×ˢ map (projIcc a b h) la) lb
⊢ Tendsto (↿(IccExtend h ∘ f)) (lc ×ˢ la) lb

Tactic:
hf.comp <| tendsto_id.prodMap tendsto_map

Premises used: Filter.tendsto_id, Set.projIcc, Filter.tendsto_map, Set.IccExtend, Filter.Tendsto.comp, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
⊢ Continuous[inst_1, inst_1] fun (x : α) ↦ max a (min b x)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set (↑(Icc a b) : Type u_1)
hs : IsOpen[inst_1] (projIcc a b h ⁻¹' s)
h₁ :
  ∀ (x : { x : α // x ∈ Icc a b }),
    Membership.mem (γ := Set { x : α // x ∈ Icc a b })
        (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) ⁻¹' projIcc a b h ⁻¹' s) x ↔
      x ∈ s
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) ⁻¹' projIcc a b h ⁻¹' s = s

Tactic:
ext
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set (↑(Icc a b) : Type u_1)
hs : IsOpen[inst_1] (projIcc a b h ⁻¹' s)
x : { x : α // x ∈ Icc a b }
⊢ Membership.mem (γ := Set { x : α // x ∈ Icc a b })
      (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) ⁻¹' projIcc a b h ⁻¹' s) x ↔
    x ∈ s

Tactic:
simp
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
f : (↑(Icc a b) : Type u_1) → β
⊢ Continuous[inst_1, inst_3] (IccExtend h f) ↔ Continuous[instTopologicalSpaceSubtype, inst_3] f

Tactic:
isQuotientMap_projIcc.continuous_iff.symm

Premises used: isQuotientMap_projIcc, Set.IccExtend, Topology.IsQuotientMap.continuous_iff, Iff.symm
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
f : γ → (↑(Icc a b) : Type u_1) → β
g : γ → α
hf : Continuous[instTopologicalSpaceProd, inst_3] ↿f
hg : Continuous[inst_4, inst_1] g
⊢ Continuous[inst_4, inst_3] fun (a_1 : γ) ↦ IccExtend h (f a_1) (g a_1)

Tactic:
show Continuous (↿f ∘ fun x => (x, projIcc a b h (g x)))
  from hf.comp <| continuous_id.prodMk <| continuous_projIcc.comp hg

Premises used: Continuous.comp, Set.projIcc, continuous_id, continuous_projIcc, Set.IccExtend, Continuous.prodMk
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
f : (↑(Icc a b) : Type u_1) → β
hf : Continuous[instTopologicalSpaceSubtype, inst_3] f
⊢ Continuous[inst_1, inst_3] (IccExtend h f)

Tactic:
hf.comp continuous_projIcc

Premises used: Continuous.comp, continuous_projIcc, Set.IccExtend
-- Module: Mathlib.Topology.Order.ProjIcc
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LinearOrder α
a b : α
h : a ≤ b
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : TopologicalSpace γ
x : γ
f : γ → (↑(Icc a b) : Type u_1) → β
g : γ → α
hf : ContinuousAt ↿f (x, projIcc a b h (g x))
hg : ContinuousAt g x
⊢ ContinuousAt.{u_3, u_2} (Y := β) (fun (a_1 : γ) ↦ Set.IccExtend h (f a_1) (g a_1)) x

Tactic:
show ContinuousAt (↿f ∘ fun x => (x, projIcc a b h (g x))) x from
    ContinuousAt.comp hf <| continuousAt_id.prodMk <| continuous_projIcc.continuousAt.comp hg

Premises used: Set.projIcc, Continuous.continuousAt, continuous_projIcc, ContinuousAt.comp, Set.IccExtend, ContinuousAt.prodMk, continuousAt_id
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ OrderTopology EReal

Tactic:
⟨rfl⟩

Premises used: OrderTopology.mk, rfl
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ T5Space EReal

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ T2Space EReal

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ DenseRange (X := EReal) fun (r : ℚ) ↦ (↑(↑r : ℝ) : EReal)

Tactic:
dense_of_exists_between fun _ _ h => exists_range_iff.2 <| exists_rat_btwn_of_lt h

Premises used: Iff.mpr, Set.exists_range_iff, DenseRange, EReal.exists_rat_btwn_of_lt, dense_of_exists_between
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ OrderTopology ℝ≥0∞

Tactic:
⟨rfl⟩

Premises used: OrderTopology.mk, rfl
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ T2Space ℝ≥0∞

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ T5Space ℝ≥0∞

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Real
Goal:
⊢ T4Space ℝ≥0∞

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ (Icc a b).Nonempty

Tactic:
have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
⊢ ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x

Tactic:
isCompact_Icc.exists_isMinOn ne hfc

Premises used: Set.Mem, Filter.Eventually, setOf, IsMinFilter, IsMinOn, CompactIccSpace.isCompact_Icc, Set.Subset, IsCompact.exists_isMinOn
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
obtain : ∀ (c : X) (cmem : c ∈ Icc a b) (cle : ∀ x ∈ Icc a b, f c ≤ f x), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
    isCompact_Icc.exists_isMinOn ne hfc

Premises used: CompactIccSpace.isCompact_Icc, Set.Icc, IsCompact.exists_isMinOn
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C

Tactic:
isCompact_Icc.exists_isMaxOn ne hfc

Premises used: Set.Mem, IsMaxOn, Filter.Eventually, setOf, CompactIccSpace.isCompact_Icc, Set.Subset, IsCompact.exists_isMaxOn, IsMaxFilter
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
obtain : ∀ (C : X) (Cmem : C ∈ Icc a b) (Cge : ∀ x ∈ Icc a b, f x ≤ f C), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
    isCompact_Icc.exists_isMaxOn ne hfc

Premises used: CompactIccSpace.isCompact_Icc, Set.Icc, IsCompact.exists_isMaxOn
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
pos : ∀ (hc : f c = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
neg : ∀ (hc : ¬f c = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
by_cases hc : f c = f a
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
pos : ∀ (hC : f C = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
neg : ∀ (hC : ¬f C = f a), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
by_cases hC : f C = f a
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
pos : ∀ (c' : X) (hc' : c' ∈ Ioo a b), ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩

Premises used: Iff.mpr, Set.nonempty_Ioo
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
⟨c', hc', Or.inl fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
pos : ∀ (x : X) (hx : x ∈ Icc a b), Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f c' ≤ f x) x} x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : X
hc' : c' ∈ Ioo a b
x : X
hx : x ∈ Icc a b
⊢ Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f c' ≤ f x) x} x

Tactic:
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]

Premises used: Set.Ioo_subset_Icc_self, le_rfl, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩

Premises used: mt, And.right, And.left, And.intro, Exists.intro, Or.inr, lt_of_le_of_ne
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
neg : a = C → f C = f a
neg₁ : C = b → f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
refine ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : a = C
rw rw₁ : f C = f C
⊢ f C = f a

Tactic:
rw [h]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : C = b
rw : f b = f a
rw₁ rw₂ : f b = f b
⊢ f C = f a

Tactic:
rw [h, hfI]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩

Premises used: mt, And.right, And.left, And.intro, Exists.intro, Or.inl, lt_of_le_of_ne
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
neg : a = c → f c = f a
neg₁ : c = b → f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
h : a = c
rw rw₁ : f c = f c
⊢ f c = f a

Tactic:
rw [h]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
h : c = b
rw : f b = f a
rw₁ rw₂ : f b = f b
⊢ f c = f a

Tactic:
rw [h, hfI]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsLocalExtr f c

Tactic:
let ⟨c, cmem, hc⟩ := exists_Ioo_extr_on_Icc hab hfc hfI
  ⟨c, cmem, hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2⟩

Premises used: _private.0.exists_isLocalExtr_Ioo.match_1, IsLocalExtr, Membership.mem, Exists, IsExtrOn.isLocalExtr, exists_Ioo_extr_on_Icc, And, And.right, And.left, And.intro, Exists.intro, Set.Ioo, Icc_mem_nhds
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
⊢ EqOn (extendFrom (Ioo a b) f) f (Ioo a b)

Tactic:
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
⊢ ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c

Tactic:
exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hfc ha hb)
      ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)

Premises used: continuousOn_Icc_extendFrom_Ioo, exists_Ioo_extr_on_Icc, eq_lim_at_right_extendFrom_Ioo, eq_lim_at_left_extendFrom_Ioo, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Order.Rolle
Goal:
X : Type u_1
Y : Type u_2
inst : ConditionallyCompleteLinearOrder X
inst_1 : DenselyOrdered X
inst_2 : TopologicalSpace X
inst_3 : OrderTopology X
inst_4 : LinearOrder Y
inst_5 : TopologicalSpace Y
inst_6 : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[>] a) (𝓝 l)
hb : Tendsto f (𝓝[<] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
obtain :
  ∀ (c : X) (hc : c ∈ Ioo a b) (hfc : IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c),
    ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c

Tactic:
obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hfc ha hb)
      ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)

Premises used: continuousOn_Icc_extendFrom_Ioo, exists_Ioo_extr_on_Icc, eq_lim_at_right_extendFrom_Ioo, eq_lim_at_left_extendFrom_Ioo, Eq.symm, Set.Ioo, Eq.trans