awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal (variationOnFromTo f s b c)
have inr : eVariationOn (naturalParameterization f s a ∘ variationOnFromTo f s a) (s ∩ Icc b c) =
  ENNReal.ofReal (variationOnFromTo f s b c)
Tactic: rw [←
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn (naturalParameterization f s a) _
        (variationOnFromTo.monotoneOn hf as) bs cs]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn (naturalParameterization f s a ∘ variationOnFromTo f s a) (s ∩ Icc b c) =
    ENNReal.ofReal (variationOnFromTo f s b c)
have inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)
Tactic: rw [@eVariationOn.eq_of_edist_zero_on _ _ _ _ _ f]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)
⊢ eVariationOn (naturalParameterization f s a ∘ variationOnFromTo f s a) (s ∩ Icc b c) =
    ENNReal.ofReal (variationOnFromTo f s b c)
have inr₁ : ∀ ⦃x : α⦄, x ∈ s ∩ Icc b c → edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0
Tactic: rw [@eVariationOn.eq_of_edist_zero_on _ _ _ _ _ f]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)
have inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (eVariationOn f (s ∩ Icc b c)).toReal
Tactic: rw [variationOnFromTo.eq_of_le _ _ bc, ENNReal.ofReal_toReal (hf b c bs cs)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (eVariationOn f (s ∩ Icc b c)).toReal
⊢ eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)
have inr₁ : eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc b c)
Tactic: rw [variationOnFromTo.eq_of_le _ _ bc, ENNReal.ofReal_toReal (hf b c bs cs)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : Membership.mem (γ := Set F) univ x
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)
have rw : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponent x) : Set F) (univ : Set F)
Tactic: rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : Membership.mem (γ := Set F) univ x
rw : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponent x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)
have rw₁ : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) univ : Set F) (univ : Set F)
Tactic: rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
h : Membership.mem (γ := Set F) univ x
rw : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponent x) : Set F) (univ : Set F)
rw₁ : Eq.{u_2 + 1} (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) univ : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)
have rw₂ : Eq.{u_2 + 1} (α := Set F) univ univ
Tactic: rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inl : ∀ (h : x ∈ s),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inr : ∀ (h : x ∈ t),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (hypothesis)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
Tactic: have hx := hs x h
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (hypothesis)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
Tactic: have hx := ht x h
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inl : ∀ (h : x ∈ s)
  (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inr : ∀ (h : x ∈ t)
  (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inl : Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
  ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
Tactic: rw [← Set.univ_subset_iff, ← hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inr : Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
  ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
Tactic: rw [← Set.univ_subset_iff, ← hx]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
⊢ Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
have inl : connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
Tactic: apply convexHull_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
⊢ Subset (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F)
    ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F)
have inr : connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
Tactic: apply convexHull_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)
⊢ connectedComponentIn s x ⊆ connectedComponentIn (s ∪ t) x
have inl : s ⊆ s ∪ t
Tactic: apply connectedComponentIn_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)
⊢ connectedComponentIn t x ⊆ connectedComponentIn (s ∪ t) x
have inr : t ⊆ s ∪ t
Tactic: apply connectedComponentIn_mono
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inl : ∀ (h : x ∈ s),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono <;>
  [apply subset_union_left; apply subset_union_right]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inr : ∀ (h : x ∈ t),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono <;>
  [apply subset_union_left; apply subset_union_right]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₁ :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₁ :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inl₂ : ∀ (h : x ∈ s)
  (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono <;>
  [apply subset_union_left; apply subset_union_right]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
inl :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₁ :
  ∀ (h : x ∈ s),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inr₁ :
  ∀ (h : x ∈ t),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
inl₂ :
  ∀ (h : x ∈ s)
    (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn s x) : Set F) (univ : Set F)),
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
have inr₂ : ∀ (h : x ∈ t)
  (hx : Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn t x) : Set F) (univ : Set F)),
  Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (s ∪ t) x) : Set F) (univ : Set F)
Tactic: rcases hx with (h | h) <;>
  -- The connected component of `x ∈ s` in `s ∪ t` contains the connected component of `x` in `s`,
  -- hence is also full; similarly for `t`.
  [have hx := hs x h; have hx := ht x h] <;>
  rw [← Set.univ_subset_iff, ← hx] <;>
  apply convexHull_mono <;>
  apply connectedComponentIn_mono <;>
  [apply subset_union_left; apply subset_union_right]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
⊢ Eq.{u_1 + 1} (α := Set F)
    (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) ((convexHull ℝ : (a : Set E) → Set E) (connectedComponentIn s x)))
    univ
have rw : Eq.{u_1 + 1} (α := Set F) (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) univ) univ
Tactic: rw [h x hx, image_univ, L.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
rw : Eq.{u_1 + 1} (α := Set F) (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) univ) univ
⊢ Eq.{u_1 + 1} (α := Set F)
    (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) ((convexHull ℝ : (a : Set E) → Set E) (connectedComponentIn s x)))
    univ
have rw₁ : Eq.{u_1 + 1} (α := Set F) (range.{u_1, u_2 + 1} (ι := E) (⇑L : (a : E) → F)) univ
Tactic: rw [h x hx, image_univ, L.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
rw : Eq.{u_1 + 1} (α := Set F) (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) univ) univ
rw₁ : Eq.{u_1 + 1} (α := Set F) (range.{u_1, u_2 + 1} (ι := E) (⇑L : (a : E) → F)) univ
⊢ Eq.{u_1 + 1} (α := Set F)
    (Set.image.{u_2, u_1} (α := E) (⇑L : (a : E) → F) ((convexHull ℝ : (a : Set E) → Set E) (connectedComponentIn s x)))
    univ
have rw₂ : Eq.{u_1 + 1} (α := Set F) univ univ
Tactic: rw [h x hx, image_univ, L.surjective.range_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
E : Type u_2
inst_3 : AddCommGroup E
inst_4 : Module ℝ E
inst_5 : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet.{u_2} (F := E) ((⇑L : (a : E) → F) ⁻¹' s)
have rw : AmpleSet.{u_2} (F := E) ((⇑L.symm : (a : F) → E) '' s)
Tactic: rw [← L.image_symm_eq_preimage]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
⊢ Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn (↑E : Set F)ᶜ x) : Set F) (univ : Set F)
have rw : ∀ (x : F), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) x
Tactic: rw [E.connectedComponentIn_eq_self_of_one_lt_codim hcodim hx, eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
have pos : ∀ (h : y ∈ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
Tactic: by_cases h : y ∈ E
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
pos : ∀ (h : y ∈ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
have neg : ∀ (h : y ∉ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
Tactic: by_cases h : y ∈ E
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
⊢ ∃ (z : F), z ∉ E
have rw : ¬E = ⊤
Tactic: rw [← not_forall, ← Submodule.eq_top_iff']
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
have pos : ∀ (z : F) (hz : z ∉ E), Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
Tactic: obtain ⟨z, hz⟩ : ∃ z, z ∉ E := by
      rw [← not_forall, ← Submodule.eq_top_iff']
      rintro rfl
      simp at hcodim
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
have pos : y - z ∈ (↑E : Set F)ᶜ
Tactic: refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z)
-- Lean 4 proof step from Mathlib.Analysis.Convex.AmpleSet (goal)
Goal:
F : Type u_1
inst : AddCommGroup F
inst_1 : Module ℝ F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E : Set F)ᶜ
y : F
h : y ∈ E
z : F
hz : z ∉ E
pos : y - z ∈ (↑E : Set F)ᶜ
⊢ Membership.mem (γ := Set F) ((convexHull ℝ : (a : Set F) → Set F) (↑E : Set F)ᶜ : Set F) y
have pos₁ : y + z ∈ (↑E : Set F)ᶜ
Tactic: refine segment_subset_convexHull ?_ ?_ (mem_segment_sub_add y z)