-- Mathlib/Analysis/Convex/Combination.lean
theorem Set.Finite.convexHull_eq_image {s : Set E} (hs : s.Finite) : convexHull R s =
    haveI := hs.fintype
    (⇑(∑ x : s, (@LinearMap.proj R s _ (fun _ => R) _ _ x).smulRight x.1)) '' stdSimplex R s

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
⊢ (convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

Tactic:
letI := hs.fintype

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ (convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

Proof state:
case h.e'_3.h.e'_3.h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
x✝ : ↑s
⊢ ((∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x✝ = j then 1 else 0) = ↑x✝

Tactic:
simp [LinearMap.sum_apply, ite_smul, Finset.filter_eq, Finset.mem_univ]

Result:
no goals

Proof state:
case h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ s = range (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) ∘ fun i j => if i = j then 1 else 0)

Tactic:
simp_rw [Function.comp_def]

Result:
case h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ s = range fun x => (∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x = j then 1 else 0

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
⊢ (convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

Tactic:
classical
letI := hs.fintype
rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]
apply congr_arg
simp_rw [Function.comp_def]
convert Subtype.range_coe.symm
simp [LinearMap.sum_apply, ite_smul, Finset.filter_eq, Finset.mem_univ]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ (convexHull R) s = ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex R ↑s

Tactic:
rw [← convexHull_basis_eq_stdSimplex, LinearMap.image_convexHull, ← Set.range_comp]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ (convexHull R) s =
    (convexHull R) (range (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) ∘ fun i j => if i = j then 1 else 0))

Proof state:
case h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ s = range fun x => (∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x = j then 1 else 0

Tactic:
convert Subtype.range_coe.symm

Result:
case h.e'_3.h.e'_3.h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
x✝ : ↑s
⊢ ((∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) fun j => if x✝ = j then 1 else 0) = ↑x✝

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ (convexHull R) s =
    (convexHull R) (range (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) ∘ fun i j => if i = j then 1 else 0))

Tactic:
apply congr_arg

Result:
case h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := hs.fintype
⊢ s = range (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) ∘ fun i j => if i = j then 1 else 0)