awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
I : Set 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₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∉ Simplex.setInterior I (s.map f hf)

Tactic:
fun h ↦ hp (Set.mem_of_mem_of_subset h (s.map f hf).setInterior_subset_affineSpan)

Premises used: Set.mem_of_mem_of_subset, Affine.Simplex.setInterior_subset_affineSpan, Not
-- 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₂
I : Set 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₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
⊢ p ∉ Simplex.setInterior I (s.map f hf)

Tactic:
exact fun h ↦ hp (Set.mem_of_mem_of_subset h (s.map f hf).setInterior_subset_affineSpan)

Premises used: Set.mem_of_mem_of_subset, Affine.Simplex.setInterior_subset_affineSpan
-- 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₂
I : Set 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₂)
p : P₂
hp : p ∉ affineSpan k (Set.range (s.map f hf).points)
neg :
  ∀ (hp : ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p),
    Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
⊢ ¬∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p

Tactic:
contrapose hp
-- 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₂
I : Set 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₂)
p : P₂
hp : ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
neg :
  ∀ (q : P) (hq : q ∈ Simplex.setInterior I s) (hqp : (f : (a : P) → P₂) q = p),
    Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p
⊢ Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p

Tactic:
obtain ⟨q, hq, hqp⟩ := hp
-- 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₂
I : Set 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₂)
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : (f : (a : P) → P₂) q = p
neg :
  ∃ (y : P), Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) y ∧ (f : (a : P) → P₂) y = p
⊢ Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p

Tactic:
rw [s.map_points, Set.range_comp, ← AffineSubspace.map_span, AffineSubspace.mem_map]

Premises used: Set.range_comp, AffineSubspace.mem_map, AffineSubspace.map_span, Affine.Simplex.map_points
-- 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₂
I : Set 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₂)
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : (f : (a : P) → P₂) q = p
⊢ ∃ (y : P), Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) y ∧ (f : (a : P) → P₂) y = p

Tactic:
⟨q, (Set.mem_of_mem_of_subset hq s.setInterior_subset_affineSpan), hqp⟩

Premises used: Set.mem_of_mem_of_subset, And.intro, Exists.intro, Affine.Simplex.setInterior_subset_affineSpan
-- 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₂
I : Set 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₂)
p : P₂
q : P
hq : q ∈ Simplex.setInterior I s
hqp : (f : (a : P) → P₂) q = p
⊢ ∃ (y : P), Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range s.points)) y ∧ (f : (a : P) → P₂) y = p

Tactic:
exact ⟨q, (Set.mem_of_mem_of_subset hq s.setInterior_subset_affineSpan), hqp⟩
-- 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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_4 + 1} ↥S := ⋯
⊢ (↑(affineSpan k (Set.range s.points)) : Set P) ⊆ Set.range (ι := ↥S) (⇑S.subtype : (a : ↥S) → P)

Tactic:
simpa using 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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_4 + 1} ↥S := ⋯
rw : Simplex.setInterior I ((s.restrict S hS).map S.subtype ⋯) = Simplex.setInterior I s
⊢ Simplex.setInterior I (s.restrict S hS) = (⇑S.subtype : (a : ↥S) → P) ⁻¹' Simplex.setInterior I s

Tactic:
rw [← S.subtype_injective.image_injective.eq_iff,
    Set.image_preimage_eq_of_subset (s.setInterior_subset_affineSpan.trans (by simpa using hS)),
    ← (s.restrict S hS).setInterior_map I S.subtype_injective]

Premises used: Function.Injective.eq_iff, HasSubset.Subset.trans, AffineSubspace.subtype_injective, Set.image_preimage_eq_of_subset, Affine.Simplex.setInterior_map, Affine.Simplex.setInterior_subset_affineSpan, Affine.Simplex.restrict, Function.Injective.image_injective
-- 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
I : Set k
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
this : Nonempty.{u_4 + 1} ↥S := ⋯
⊢ Simplex.setInterior I ((s.restrict S hS).map S.subtype ⋯) = Simplex.setInterior I s

Tactic:
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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).interior = s.interior

Tactic:
s.setInterior_reindex _ _

Premises used: Affine.Simplex.interior, Affine.Simplex.setInterior_reindex
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ Membership.mem (α := P) s.interior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)

Tactic:
affineCombination_mem_setInterior_iff hw

Premises used: Affine.Simplex.interior, Set.Mem, Affine.Simplex.affineCombination_mem_setInterior_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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).closedInterior = s.closedInterior

Tactic:
s.setInterior_reindex _ _

Premises used: Affine.Simplex.closedInterior, Affine.Simplex.setInterior_reindex
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
⊢ Membership.mem (α := P) s.closedInterior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)

Tactic:
affineCombination_mem_setInterior_iff hw

Premises used: Set.Mem, Affine.Simplex.closedInterior, Affine.Simplex.affineCombination_mem_setInterior_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
n : ℕ
s : Simplex k P n
⊢ s.interior ⊆ s.closedInterior

Tactic:
fun _ ⟨w, hw, hw01, hww⟩ ↦ ⟨w, hw, fun i ↦ ⟨(hw01 i).1.le, (hw01 i).2.le⟩, hww⟩

Premises used: _private.0.Affine.Simplex.interior_subset_closedInterior.match_1, Membership.mem, LT.lt.le, Set.Subset, And.right, Affine.Simplex.closedInterior, And.left, And.intro, Exists.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
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
rw : ∃ (x : Fin (n + 1)), (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 x : k) ∉ Set.Ioo 0 1
⊢ s.points i ∉ s.interior

Tactic:
rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_interior_iff (Fintype.sum_pi_single' _ _), not_forall]

Premises used: Finset.mem_univ, Affine.Simplex.points, Finset.univ, Affine.Simplex.affineCombination_mem_interior_iff, Finset.affineCombination_piSingle, Classical.not_forall, Fintype.sum_pi_single'
-- 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
i : Fin (n + 1)
⊢ (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 i : k) ∉ Set.Ioo 0 1

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
n : ℕ
s : Simplex k P n
i : Fin (n + 1)
⊢ ∃ (x : Fin (n + 1)), (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 x : k) ∉ Set.Ioo 0 1

Tactic:
exact ⟨i, 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
i : Fin (n + 1)
rw :
  ∀ (i_1 : Fin (n + 1)),
    Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1)
      (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 i_1 : k)
⊢ s.points i ∈ s.closedInterior

Tactic:
rw [← Finset.univ.affineCombination_piSingle k s.points (Finset.mem_univ i),
    affineCombination_mem_closedInterior_iff (Fintype.sum_pi_single' _ _)]

Premises used: Affine.Simplex.affineCombination_mem_closedInterior_iff, Finset.mem_univ, Affine.Simplex.points, Finset.univ, Finset.affineCombination_piSingle, Fintype.sum_pi_single'
-- 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
i j : Fin (n + 1)
inl :
  Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) j 1 j : k)
inr :
  ∀ (hj : j ≠ i),
    Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)
⊢ Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)

Tactic:
obtain rfl | hj := eq_or_ne j i

Premises used: eq_or_ne, 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
j : Fin (n + 1)
⊢ Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) j 1 j : k)

Tactic:
simp_all
-- 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
i j : Fin (n + 1)
hj : j ≠ i
⊢ Membership.mem.{u_1, u_1} (α := k) (γ := Set k) (Set.Icc 0 1) (Pi.single (M := fun (a : Fin (n + 1)) ↦ k) i 1 j : k)

Tactic:
simp_all
-- 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
rw : s.interior ⊆ s.closedInterior ∧ ∃ x ∈ s.closedInterior, x ∉ s.interior
⊢ s.interior ⊂ s.closedInterior

Tactic:
rw [Set.ssubset_iff_exists]

Premises used: Set.ssubset_iff_exists
-- 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
⊢ s.interior ⊆ s.closedInterior ∧ ∃ x ∈ s.closedInterior, x ∉ s.interior

Tactic:
⟨s.interior_subset_closedInterior, s.points 0, s.point_mem_closedInterior 0,
    s.point_notMem_interior 0⟩

Premises used: Affine.Simplex.interior_subset_closedInterior, Affine.Simplex.points, Affine.Simplex.point_notMem_interior, And.intro, Exists.intro, Affine.Simplex.point_mem_closedInterior, OfNat.ofNat
-- 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
⊢ s.interior ⊆ s.closedInterior ∧ ∃ x ∈ s.closedInterior, x ∉ s.interior

Tactic:
exact ⟨s.interior_subset_closedInterior, s.points 0, s.point_mem_closedInterior 0,
    s.point_notMem_interior 0⟩
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hi : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
affineCombination_mem_affineSpan_of_nonempty hw _

Premises used: Set.Mem, affineCombination_mem_affineSpan_of_nonempty
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hi : ∀ (i : Fin (n + 1)), Membership.mem (γ := Set k) (Set.Icc 0 1) (w i)
⊢ Membership.mem (α := P) (↑(affineSpan k (Set.range s.points)) : Set P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
exact affineCombination_mem_affineSpan_of_nonempty hw _

Premises used: affineCombination_mem_affineSpan_of_nonempty
-- 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
s : Simplex k P 0
h : ∀ (p : P), p ∈ s.interior ↔ Membership.mem (γ := Set P) ∅ p
⊢ s.interior = ∅

Tactic:
ext p
-- 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
s : Simplex k P 0
p : P
h :
  ∀ (x : Fin 1 → k),
    x 0 = 1 → (∀ (i : Fin 1), 0 < x i ∧ x i < 1) → ¬(affineCombination k {0} s.points : (a : Fin 1 → k) → P) x = p
⊢ p ∈ s.interior ↔ Membership.mem (γ := Set P) ∅ p

Tactic:
simp only [Simplex.interior, Simplex.setInterior, Nat.reduceAdd, univ_unique, Fin.default_eq_zero,
    Fin.isValue, sum_singleton, Set.mem_Ioo, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false,
    not_exists, not_and]

Premises used: Set.mem_Ioo, Affine.Simplex.interior, iff_false, Affine.Simplex.setInterior, not_exists, Finset.univ_unique, Nat.reduceAdd, Set.mem_setOf_eq, Finset.sum_singleton, Fin.isValue, Set.mem_empty_iff_false, Fin.default_eq_zero, not_and
-- 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
s : Simplex k P 0
p : P
w : Fin 1 → k
h : w 0 = 1
hi : ∀ (i : Fin 1), 0 < w i ∧ w i < 1
⊢ ¬(affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p

Tactic:
simpa [h] using hi 0

Premises used: OfNat.ofNat
-- 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
s : Simplex k P 0
h : ∀ (p : P), p ∈ s.closedInterior ↔ Membership.mem (γ := Set P) {s.points 0} p
⊢ s.closedInterior = {s.points 0}

Tactic:
ext p
-- 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
s : Simplex k P 0
p : P
h :
  (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) ↔
    p = s.points 0
⊢ p ∈ s.closedInterior ↔ Membership.mem (γ := Set P) {s.points 0} p

Tactic:
simp only [Simplex.closedInterior, Simplex.setInterior, Nat.reduceAdd, univ_unique,
    Fin.default_eq_zero, Fin.isValue, sum_singleton, Set.mem_Icc, Set.mem_setOf_eq,
    Set.mem_singleton_iff]

Premises used: Affine.Simplex.setInterior, Finset.univ_unique, Nat.reduceAdd, Set.mem_setOf_eq, Finset.sum_singleton, Set.mem_singleton_iff, Affine.Simplex.closedInterior, Fin.isValue, Set.mem_Icc, Fin.default_eq_zero
-- 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
s : Simplex k P 0
p : P
h :
  (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) →
    p = s.points 0
h₁ :
  p = s.points 0 →
    ∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p
⊢ (∃ (w : Fin 1 → k),
      w 0 = 1 ∧ (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = p) ↔
    p = s.points 0

Tactic:
constructor
-- 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
s : Simplex k P 0
w : Fin 1 → k
h0 : w 0 = 1
hi : ∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1
⊢ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = s.points 0

Tactic:
simp [affineCombination_apply, h0]

Premises used: Finset.affineCombination_apply
-- 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
s : Simplex k P 0
⊢ Eq.{u_1 + 1} (α := k) (1 0) 1 ∧
    (∀ (i : Fin 1), LE.le.{u_1} (α := k) 0 (1 i) ∧ LE.le.{u_1} (α := k) (1 i) 1) ∧
      (affineCombination k {0} s.points : (a : Fin 1 → k) → P) 1 = s.points 0

Tactic:
simp [affineCombination_apply]

Premises used: Finset.affineCombination_apply
-- 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
s : Simplex k P 0
⊢ ∃ (w : Fin 1 → k),
    w 0 = 1 ∧
      (∀ (i : Fin 1), 0 ≤ w i ∧ w i ≤ 1) ∧ (affineCombination k {0} s.points : (a : Fin 1 → k) → P) w = s.points 0

Tactic:
exact ⟨1, by simp [affineCombination_apply]⟩
-- 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
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
⊢ Membership.mem (α := P) (s.face h).interior ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    (∀ i ∈ fs, Membership.mem (γ := Set k) (Set.Ioo 0 1) (w i)) ∧ ∀ i ∉ fs, w i = 0

Tactic:
affineCombination_mem_setInterior_face_iff_mem _ _ _ hw

Premises used: Affine.Simplex.interior, Set.Mem, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem
-- 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
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
⊢ Membership.mem (α := P) (s.face h).closedInterior
      ((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:
affineCombination_mem_setInterior_face_iff_mem _ _ _ hw

Premises used: Set.Mem, Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem, Affine.Simplex.closedInterior
-- 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
rw :
  ((∀ 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
⊢ Membership.mem (α := P) (s.face h).interior ((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_interior_face_iff_mem_Ioo h hw]

Premises used: Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo