Theorem: centroid_mem_combiInterior (LeanCamCombi/SimplicialComplex/Simplex.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ Finset.centroid 𝕜 s id ∈ combiInterior 𝕜 s
Tactic:
rw [Finset.centroid_def]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Tactic:
have hsweights := s.sum_centroidWeights_eq_one_of_nonempty 𝕜 hs'
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Tactic:
rw [affineCombination_eq_centerMass hsweights]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈ combiInterior 𝕜 s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈ combiInterior 𝕜 s
Tactic:
rw [combiInterior_eq hs]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' ⟨_, fun y _ => _, hsweights, rfl⟩
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
y : E
x✝ : y ∈ s
⊢ 0 < Finset.centroidWeights 𝕜 s y

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
y : E
x✝ : y ∈ s
⊢ 0 < Finset.centroidWeights 𝕜 s y
Tactic:
simpa using hs'.card_pos
State after:
no goals