awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) →
    (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
refine :
  ((∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0) →
    ∀ (hii : ∀ i ∈ fs, 0 < w i) (hi0 : ∀ i ∉ fs, w i = 0) (i : Fin (n + 1)) (hi : i ∈ fs), w i < 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
    (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
refine ⟨by grind, fun ⟨hii, hi0⟩ ↦ ⟨fun i hi ↦ ⟨hii i hi, ?_⟩, hi0⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
rw : w i < ∑ x ∈ fs, w x
⊢ w i < 1

Tactic:
rw [← hw, ← Finset.sum_subset (Finset.subset_univ fs) fun j _ ↦ hi0 j]

Premises used: Finset.sum_subset, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ 1 < #fs

Tactic:
grind [→ NeZero.ne]

Premises used: NeZero.ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
obtain : ∀ (j : Fin (n + 1)) (hj : j ∈ fs) (hji : j ≠ i), w i < ∑ x ∈ fs, w x
⊢ w i < ∑ x ∈ fs, w x

Tactic:
obtain ⟨j, hj, hji⟩ := fs.exists_mem_ne (by grind [→ NeZero.ne]) i

Premises used: Finset.exists_mem_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
j : Fin (n + 1)
hj : j ∈ fs
hji : j ≠ i
⊢ w i < ∑ x ∈ fs, w x

Tactic:
Finset.single_lt_sum hji hi hj (hii j hj) fun t ht _ ↦ (hii t ht).le

Premises used: LT.lt.le, Finset.single_lt_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
inst_6 : NeZero m
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 < w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
j : Fin (n + 1)
hj : j ∈ fs
hji : j ≠ i
⊢ w i < ∑ x ∈ fs, w x

Tactic:
exact Finset.single_lt_sum hji hi hj (hii j hj) fun t ht _ ↦ (hii t ht).le

Premises used: LT.lt.le, Finset.single_lt_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
rw :
  ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
⊢ Membership.mem (α := P) (s.face h).closedInterior
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
rw [s.affineCombination_mem_closedInterior_face_iff_mem_Icc h hw]

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) →
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
refine :
  ((∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0) →
    ∀ (hii : ∀ i ∈ fs, 0 ≤ w i) (hi0 : ∀ i ∉ fs, w i = 0) (i : Fin (n + 1)) (hi : i ∈ fs), w i ≤ 1
⊢ ((∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0) ↔
    (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0

Tactic:
refine ⟨by grind, fun ⟨hii, hi0⟩ ↦ ⟨fun i hi ↦ ⟨hii i hi, ?_⟩, hi0⟩⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 ≤ w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
rw : w i ≤ ∑ x ∈ fs, w x
⊢ w i ≤ 1

Tactic:
rw [← hw, ← Finset.sum_subset (Finset.subset_univ fs) fun j _ ↦ hi0 j]

Premises used: Finset.sum_subset, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 ≤ w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ≤ ∑ x ∈ fs, w x

Tactic:
Finset.single_le_sum (fun t ht ↦ (hii t ht)) hi

Premises used: Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : IsOrderedAddMonoid k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h_1 : (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0
hii : ∀ i ∈ fs, 0 ≤ w i
hi0 : ∀ i ∉ fs, w i = 0
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ≤ ∑ x ∈ fs, w x

Tactic:
exact Finset.single_le_sum (fun t ht ↦ (hii t ht)) hi

Premises used: Finset.single_le_sum
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : PartialOrder k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ (s.map f hf).interior = (⇑f : (a : P) → P₂) '' s.interior

Tactic:
s.setInterior_map _ hf

Premises used: Affine.Simplex.interior, Affine.Simplex.setInterior_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
inst_7 : PartialOrder k
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_4 + 1, u_5 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ (s.map f hf).closedInterior = (⇑f : (a : P) → P₂) '' s.closedInterior

Tactic:
s.setInterior_map _ hf

Premises used: Affine.Simplex.closedInterior, Affine.Simplex.setInterior_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (s.restrict S hS).interior = (⇑S.subtype : (a : ↥S) → P) ⁻¹' s.interior

Tactic:
s.setInterior_restrict _ hS

Premises used: Affine.Simplex.interior, Affine.Simplex.setInterior_restrict
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (s.restrict S hS).closedInterior = (⇑S.subtype : (a : ↥S) → P) ⁻¹' s.closedInterior

Tactic:
s.setInterior_restrict _ hS

Premises used: Affine.Simplex.closedInterior, Affine.Simplex.setInterior_restrict
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
p : P
hp : p ∈ (s.face h).closedInterior
⊢ Set.range (s.face h).points ⊆ Set.range s.points

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
p : P
hp : p ∈ (s.face h).closedInterior
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p

Tactic:
have hp' : p ∈ affineSpan k (Set.range s.points) :=
    Set.mem_of_mem_of_subset hp <|
      (s.face h).closedInterior_subset_affineSpan.trans <|
        affineSpan_mono k <| by simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
p : P
hp : p ∈ (s.face h).closedInterior
hp' : Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) p
obtain :
  ∀ (w : Fin (n + 1) → k) (hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1)
    (hp :
      Membership.mem (α := P) (s.face h).closedInterior
        ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P))
    (hp' :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
        ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)),
    Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ p ∈ s.closedInterior

Tactic:
obtain ⟨w, hw1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp'

Premises used: eq_affineCombination_of_mem_affineSpan_of_fintype, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (s.face h).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0

Tactic:
rw [affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1] at hp

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp :
  Membership.mem (α := P) (s.face h).closedInterior
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hp₁ : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [affineCombination_mem_closedInterior_face_iff_mem_Icc _ _ hw1] at hp

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
rw : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [affineCombination_mem_closedInterior_iff hw1]

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
pos : ∀ (hi : i ∈ fs), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
neg : ∀ (hi : i ∉ fs), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)

Tactic:
by_cases hi : i ∈ fs
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : i ∈ fs
⊢ Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hp : (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0
hp' :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range s.points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
i : Fin (n + 1)
hi : i ∉ fs
⊢ Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
⊢ s.points j ∈ (s.face h).closedInterior ↔ j ∈ fs

Tactic:
⟨fun hj ↦ ?_, fun hfs ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
refine_1 : ∀ (hj : s.points j ∈ (s.face h).closedInterior), j ∈ fs
refine_2 : ∀ (hfs : j ∈ fs), s.points j ∈ (s.face h).closedInterior
⊢ s.points j ∈ (s.face h).closedInterior ↔ j ∈ fs

Tactic:
refine ⟨fun hj ↦ ?_, fun hfs ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hj : s.points j ∈ (s.face h).closedInterior
this : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
⊢ j ∈ fs

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hj : s.points j ∈ (s.face h).closedInterior
refine_1 : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
⊢ j ∈ fs

Tactic:
suffices s.points j ∈ affineSpan k (s.points '' fs) by simpa
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
hj : s.points j ∈ (s.face h).closedInterior
refine_1 :
  ∀ (w : Fin (m + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1)
    (hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i))
    (hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j),
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)

Tactic:
obtain ⟨w, hw, hw', hs⟩ := hj
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j
refine_1 :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1)))))
    ((affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points j)

Tactic:
rw [← hs]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j
⊢ (↑(affineSpan k (Set.range (s.face h).points)) : Set P) ⊆
    (↑(affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) : Set P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
inst_4 : PartialOrder k
inst_5 : Nontrivial k
inst_6 : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
j : Fin (n + 1)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hw' : ∀ (i : Fin (m + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
hs : (affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w = s.points j
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1)))))
    ((affineCombination k univ (s.face h).points : (a : Fin (m + 1) → k) → P) w : P)

Tactic:
exact Set.mem_of_mem_of_subset (affineCombination_mem_affineSpan hw _) (by simp)

Premises used: affineCombination_mem_affineSpan, Set.mem_of_mem_of_subset