awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' closure[inst_2] s =
    closure[inst_2] t
have a : (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s =
  HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s))
Tactic: calc
      (fun a ↦ y + h (-x + a)) '' closure s = y +ᵥ h '' closure (-x +ᵥ s) := by
        simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
      _ = _ := by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.GaugeRescale (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : T1Space E
s t : Set E
hsc : Convex ℝ s
hsb : IsVonNBounded ℝ s
hst : Convex ℝ t
htb : IsVonNBounded ℝ t
x : E
hx : x ∈ interior s
y : E
hy : y ∈ interior t
h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
a :
  (fun (a : E) ↦ HAdd.hAdd (β := E) y ((h : (a : E) → E) (-x + a) : E)) '' closure[inst_2] s =
    HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s))
⊢ (⇑(Homeomorph.trans (Homeomorph.addLeft (-x)) (h.trans (Homeomorph.addLeft y))) : (a : E) → E) '' closure[inst_2] s =
    closure[inst_2] t
have a₁ : HVAdd.hVAdd (β := Set E) y ((⇑h : (a : E) → E) '' closure[inst_2] (-x +ᵥ s)) = closure[inst_2] t
Tactic: calc
      (fun a ↦ y + h (-x + a)) '' closure s = y +ᵥ h '' closure (-x +ᵥ s) := by
        simp_rw [closure_vadd, ← image_vadd, image_image, vadd_eq_add]
      _ = _ := by rw [image_gaugeRescaleHomeomorph_closure, closure_vadd, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) x ↔
    ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
have simp_rw : Membership.mem (γ := Set E) (⋂ (t : Set E), ⋂ (_ : s ⊆ t), ⋂ (_ : Convex 𝕜 t), t) x ↔
  ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
Tactic: simp_rw [convexHull_eq_iInter, mem_iInter]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅
have mp : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
mp : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) → s = ∅
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ s = ∅
have mpr : s = ∅ → Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
h : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E)
⊢ s = ∅
have mp : s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s
Tactic: rw [← Set.subset_empty_iff, ← h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
⊢ Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) s) ↔ s.Nonempty
have rw : ¬Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) (∅ : Set E) ↔ ¬s = ∅
Tactic: rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
⊢ s = {x}
have rw : s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s
Tactic: rw [← Set.Nonempty.subset_singleton_iff, ← hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
rw : s ⊆ (convexHull 𝕜 : (a : Set E) → Set E) s
⊢ s = {x}
have rw₁ : s.Nonempty
Tactic: rw [← Set.Nonempty.subset_singleton_iff, ← hs]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
x : E
hs : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E) ({x} : Set E)
⊢ s.Nonempty
have by_contra! : ∀ (hs : s = ∅), False
Tactic: by_contra! hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
⊢ (convexHull 𝕜 : (a : Set E) → Set E) {x, y} = segment 𝕜 x y
have refine : {x, y} ⊆ segment 𝕜 x y
Tactic: refine (convexHull_min ?_ <| convex_segment _ _).antisymm
    (segment_subset_convexHull (mem_insert _ _) <| subset_insert _ _ <| mem_singleton _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : E
⊢ {x, y} ⊆ segment 𝕜 x y
have rw : x ∈ segment 𝕜 x y ∧ y ∈ segment 𝕜 x y
Tactic: rw [insert_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
⊢ Convex 𝕜 (s \ {x}) ↔ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
have mp : Convex 𝕜 (s \ {x}) → x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
mp : Convex 𝕜 (s \ {x}) → x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
⊢ Convex 𝕜 (s \ {x}) ↔ x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
have mpr : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) → Convex 𝕜 (s \ {x})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hsx : Convex 𝕜 (s \ {x})
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E) x
⊢ False
have hx₁ : x ∈ s \ {x}
Tactic: rw [hsx.convexHull_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
h : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
⊢ Convex 𝕜 (s \ {x})
have rw : Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (s \ {x}) : Set E)
⊢ Convex 𝕜 (s \ {x})
have mpr : s \ {x} = (convexHull 𝕜 : (a : Set E) → Set E) (s \ {x})
Tactic: suffices h : s \ {x} = convexHull 𝕜 (s \ {x}) by
    rw [h]
    exact convex_convexHull 𝕜 _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Eq.{u_3 + 1} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
have h₁ : Subset.{u_3} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
  ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
h₁ :
  Subset.{u_3} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
⊢ Eq.{u_3 + 1} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
have h₂ : Subset.{u_3} (α := Set F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s) : Set F)
  (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s) : Set F)
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset.{u_3} (α := Set F) (image.{u_2, u_3} (α := E) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
have h₁ : Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
  (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s)) :
    Set E)
Tactic: rw [Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ Subset (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    (preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s)) :
      Set E)
have h₁ : s ⊆ preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
Tactic: refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ s ⊆ preimage.{u_2, u_3} (β := F) (⇑f : (a : E) → F) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
have h₁ : Subset.{u_3} (α := Set F) ((⇑f : (a : E) → F) '' s) ((convexHull 𝕜 : (a : Set F) → Set F) ((⇑f : (a : E) → F) '' s))
Tactic: rw [← Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)
have refine : LE.le (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)
Tactic: refine le_antisymm ?_ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ LE.le (α := AffineSubspace 𝕜 E) (affineSpan 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s)) (affineSpan 𝕜 s)
have rw : (convexHull 𝕜 : (a : Set E) → Set E) s ⊆ (↑(affineSpan 𝕜 s) : Set E)
Tactic: rw [affineSpan_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Hull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (-s) : Set E) (-(convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
have simp_rw : Eq (α := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : E) ↦ -x) '' s) : Set E)
  ((fun (x : E) ↦ -x) '' (convexHull 𝕜 : (a : Set E) → Set E) s : Set E)
Tactic: simp_rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
⊢ x ∈ s
have this : Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s))
Tactic: have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p x)
this : Set.Nonempty.{u_2} (α := E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s))
⊢ x ∈ s
have this₁ : s.Nonempty
Tactic: rw [convexHull_nonempty_iff, Set.image_nonempty] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p
have refine : ∀ (i j : ι) (hij : p i = p j),
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' {j}) : Set E) (p i)
Tactic: refine fun i j hij => hc {j} i ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' {j}) : Set E) (p i)
have rw : Membership.mem (γ := Set E) {p j} (p j)
Tactic: rw [hij, Set.image_singleton, convexHull_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p ∘ (⇑f : (a : ι') → ι) '' s) : Set E)
    ((p ∘ (⇑f : (a : ι') → ι)) x)
⊢ x ∈ s
have rw : Membership.mem.{u_3, u_3} (α := ι) (γ := Set ι) ((⇑f : (a : ι') → ι) '' s) ((f : (a : ι') → ι) x : ι)
Tactic: rw [← f.injective.mem_set_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
ι' : Type u_4
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx :
  Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p ∘ (⇑f : (a : ι') → ι) '' s) : Set E)
    ((p ∘ (⇑f : (a : ι') → ι)) x)
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (⇑f : (a : ι') → ι) '' s) : Set E)
    (p ((f : (a : ι') → ι) x))
have rwa : Membership.mem (γ := Set E)
  ((convexHull 𝕜 : (a : Set E) → Set E) ((fun (x : ι') ↦ p ((f : (a : ι') → ι) x)) '' s) : Set E)
  (p ((f : (a : ι') → ι) x))
Tactic: rwa [Set.image_image]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range p })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
have hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
Tactic: have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
⊢ ConvexIndependent.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ Set.range p })
    (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
have h : Eq (α := { x : E // x ∈ Set.range p } → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
  (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι))
Tactic: convert! hc.comp_embedding fe
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
⊢ Eq (α := { x : E // x ∈ Set.range p } → E) (Subtype.val (p := fun (x : E) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι))
have h : ∀ (x : { x : E // x ∈ Set.range p }), (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
x : { x : E // x ∈ Set.range p }
⊢ (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x
have h : (↑x : E) = (p ∘ f) x
Tactic: rw [Embedding.coeFn_mk, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
x : { x : E // x ∈ Set.range p }
h : (↑x : E) = (p ∘ f) x
⊢ (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x
have h₁ : (↑x : E) = p (f x)
Tactic: rw [Embedding.coeFn_mk, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
f : (↑(Set.range p) : Type u_2) → ι :=
  fun (x : (↑(Set.range p) : Type u_2)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : E)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_2)), p (f x) = (↑x : E)
fe : Embedding.{u_2 + 1, u_3 + 1} (↑(Set.range p) : Type u_2) ι := { toFun := f, inj' := ⋯ }
x : { x : E // x ∈ Set.range p }
h : (↑x : E) = (p ∘ f) x
h₁ : (↑x : E) = p (f x)
⊢ (↑x : E) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_2)) → ι)) x
have h₂ : (↑x : E) = (↑x : E)
Tactic: rw [Embedding.coeFn_mk, comp_apply, hf]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
have refine_1 : ∀ (hc : ConvexIndependent 𝕜 p) (i : ι) (s : Set ι)
  (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)), False
Tactic: refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
refine_1 :
  ∀ (hc : ConvexIndependent 𝕜 p) (i : ι) (s : Set ι)
    (h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)), False
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
have refine_2 : ∀ (h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)) (s : Set ι) (i : ι)
  (hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)), i ∈ s
Tactic: refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)
⊢ False
have h₁ : i ∈ s \ {i}
Tactic: rw [hc.mem_convexHull_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
⊢ i ∈ s
have refine_2 : ∀ (H : i ∉ s), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Independent (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E)
s : Set ι
i : ι
hi : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' s) : Set E) (p i)
H : i ∉ s
⊢ False
have refine_2 : Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) (p '' (s \ {i})) : Set E) (p i)
Tactic: refine h i s ?_