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_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
this_1 : Subsingleton V
this : Subsingleton P
⊢ (s.points '' {i}ᶜ).Nonempty

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
this_1 : Subsingleton V
this : Subsingleton P
refine_2 :
  Membership.mem.{u_5, u_5} (α := P) (γ := AffineSubspace k P) ⊤
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (by simp)]

Premises used: Iff.mpr, affineSpan_eq_top_iff_nonempty_of_subsingleton
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h : w i = 0
hk : Subsingleton k
this_1 : Subsingleton V
this : Subsingleton P
⊢ Membership.mem.{u_5, u_5} (α := P) (γ := AffineSubspace k P) ⊤
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h : w i = 0
hk : Nontrivial k
⊢ ∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) univ i_1 → i_1 ∉ {i}ᶜ → w i_1 = 0

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h : w i = 0
hk : Nontrivial k
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
exact affineCombination_mem_affineSpan_image hw (by simpa using h) s.points

Premises used: Affine.Simplex.points, affineCombination_mem_affineSpan_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
⊢ s.map (AffineMap.id k P) ⋯ = s

Tactic:
ext fun _ => rfl

Premises used: Affine.Simplex.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V P
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ P₃
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
g : P₂ →ᵃ[k] P₃
hg : Injective.{u_6 + 1, u_7 + 1} (α := P₂) (β := P₃) (⇑g : (a : P₂) → P₃)
⊢ s.map (g.comp f) ⋯ = (s.map f hf).map g hg

Tactic:
ext fun _ => rfl

Premises used: Affine.Simplex.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_5
P₂ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : Module k V
inst_4 : Module k V₂
inst_5 : AffineSpace V P
inst_6 : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ (s.map f hf).face h = (s.face h).map f hf

Tactic:
rfl

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

Tactic:
rfl

Premises used: Affine.Simplex.face, Affine.Simplex.map, Affine.Simplex.faceOpposite, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_5
P₂ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : Module k V
inst_4 : Module k V₂
inst_5 : AffineSpace V P
inst_6 : AffineSpace V₂ P₂
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
p : P
⊢ map (mkOfPoint k p) f hf = mkOfPoint k ((f : (a : P) → P₂) p)

Tactic:
rfl

Premises used: Affine.Simplex.mkOfPoint, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
⊢ s.reindex (Equiv.refl (Fin (n + 1))) = s

Tactic:
ext fun _ => rfl

Premises used: Affine.Simplex.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n₁ n₂ n₃ : ℕ
e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)
e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1)
s : Simplex k P n₁
⊢ s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃

Tactic:
rfl

Premises used: Affine.Simplex.reindex, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
rw : s.reindex (e.trans e.symm) = s
rw₁ : s.reindex (Equiv.refl (Fin (m + 1))) = s
rw₂ rw₃ : s = s
⊢ (s.reindex e).reindex e.symm = s

Tactic:
rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]

Premises used: Affine.Simplex.reindex_trans, Equiv.self_trans_symm, Affine.Simplex.reindex_refl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (n + 1) ≃ Fin (m + 1)
rw : s.reindex (e.symm.trans e) = s
rw₁ : s.reindex (Equiv.refl (Fin (m + 1))) = s
rw₂ rw₃ : s = s
⊢ (s.reindex e.symm).reindex e = s

Tactic:
rw [← reindex_trans, Equiv.symm_trans_self, reindex_refl]

Premises used: Affine.Simplex.reindex_trans, Affine.Simplex.reindex_refl, Equiv.symm_trans_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
rw :
  Set.range
      { points := s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)), independent := ⋯ : Simplex k P n }.points =
    Set.range s.points
rw₁ : s.points '' Set.range (ι := Fin (n + 1)) (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)) = Set.range s.points
rw₂ : s.points '' Set.univ = Set.range s.points
rw₃ rw₄ : Set.range s.points = Set.range s.points
⊢ Set.range (s.reindex e).points = Set.range s.points

Tactic:
rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]

Premises used: Set.range_comp, Set.image_univ, Affine.Simplex.reindex, Equiv.range_eq_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_5
P₂ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : Module k V
inst_4 : Module k V₂
inst_5 : AffineSpace V P
inst_6 : AffineSpace V₂ P₂
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ (s.map f hf).reindex e = (s.reindex e).map f hf

Tactic:
rfl

Premises used: Affine.Simplex.map, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
fs : Finset (Fin (n + 1))
n' : ℕ
h : #fs = n' + 1
simp :
  s.points '' (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)) '' (↑fs : Set (Fin (n + 1))) =
    s.points '' (↑(Finset.map e.symm.toEmbedding fs) : Set (Fin (m + 1)))
⊢ Set.range ((s.reindex e).face h).points =
    Set.range (ι := Fin (n' + 1)) (points (s.face (fs := Finset.map e.symm.toEmbedding fs) ⋯))

Tactic:
simp only [range_face_points, reindex_points, Set.image_comp]

Premises used: Affine.Simplex.range_face_points, Affine.Simplex.reindex_points, Set.image_comp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
fs : Finset (Fin (n + 1))
n' : ℕ
h : #fs = n' + 1
⊢ s.points '' (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)) '' (↑fs : Set (Fin (n + 1))) =
    s.points '' (↑(Finset.map e.symm.toEmbedding fs) : Set (Fin (m + 1)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
rw :
  Set.range (ι := Fin (n - 1 + 1)) (points (s.face (fs := Finset.map e.symm.toEmbedding {i}ᶜ) ⋯)) =
    Set.range (s.faceOpposite ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i)).points
⊢ Set.range ((s.reindex e).faceOpposite i).points =
    Set.range (s.faceOpposite ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i)).points

Tactic:
rw [faceOpposite, range_face_reindex]

Premises used: Affine.Simplex.range_face_reindex, Affine.Simplex.faceOpposite
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
i : Fin (n + 1)
⊢ Set.range (ι := Fin (n - 1 + 1)) (points (s.face (fs := Finset.map e.symm.toEmbedding {i}ᶜ) ⋯)) =
    Set.range (s.faceOpposite ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i)).points

Tactic:
simp [Equiv.image_compl]

Premises used: Equiv.image_compl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
S₁ S₂ : AffineSubspace k P
hS₁ : affineSpan k (Set.range s.points) ≤ S₁
hS₂ : S₁ ≤ S₂
⊢ (s.restrict S₁ hS₁).map (AffineSubspace.inclusion hS₂) ⋯ = s.restrict S₂ ⋯

Tactic:
rfl

Premises used: Affine.Simplex.map, Affine.Simplex.restrict, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V P
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ P₃
n : ℕ
S : AffineSubspace k P
inst_10 : Nonempty.{u_5 + 1} ↥S
s : Simplex k (↥S) n
y : Fin (n + 1)
⊢ (s.map S.subtype ⋯).points y ∈ (↑S : Set P)

Tactic:
Subtype.prop _

Premises used: Set.Mem, Subtype.prop
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V P
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ P₃
n : ℕ
S : AffineSubspace k P
inst_10 : Nonempty.{u_5 + 1} ↥S
s : Simplex k (↥S) n
y : Fin (n + 1)
⊢ (s.map S.subtype ⋯).points y ∈ (↑S : Set P)

Tactic:
exact Subtype.prop _

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
S : AffineSubspace k P
inst_4 : Nonempty.{u_5 + 1} ↥S
s : Simplex k (↥S) n
⊢ (s.map S.subtype ⋯).restrict S ⋯ = s

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
V₃ : Type u_4
P : Type u_5
P₂ : Type u_6
P₃ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : Module k V
inst_5 : Module k V₂
inst_6 : Module k V₃
inst_7 : AffineSpace V P
inst_8 : AffineSpace V₂ P₂
inst_9 : AffineSpace V₃ P₃
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
S₁ : AffineSubspace k P
S₂ : AffineSubspace k P₂
hS₁ : affineSpan k (Set.range s.points) ≤ S₁
hfS : AffineSubspace.map f S₁ ≤ S₂
this_1 : Nonempty.{u_5 + 1} ↥S₁ := ⋯
this : Nonempty.{u_6 + 1} ↥S₂ := ⋯
⊢ affineSpan k (Set.range (s.map f hf).points) = AffineSubspace.map f (affineSpan k (Set.range s.points))

Tactic:
simp [AffineSubspace.map_span, Set.range_comp]

Premises used: Set.range_comp, AffineSubspace.map_span
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
V₂ : Type u_3
P : Type u_5
P₂ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : AddCommGroup V₂
inst_3 : Module k V
inst_4 : Module k V₂
inst_5 : AffineSpace V P
inst_6 : AffineSpace V₂ P₂
n : ℕ
s : Simplex k P n
f : P →ᵃ[k] P₂
hf : Injective.{u_5 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
S₁ : AffineSubspace k P
S₂ : AffineSubspace k P₂
hS₁ : affineSpan k (Set.range s.points) ≤ S₁
hfS : AffineSubspace.map f S₁ ≤ S₂
⊢ Eq (α := Simplex k (↥S₂) n) ((s.restrict S₁ hS₁).map (f.restrict hfS) ⋯ : Simplex k (↥S₂) n)
    ((s.map f hf).restrict S₂ ⋯ : Simplex k (↥S₂) n)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
⊢ (s.restrict (affineSpan k (Set.range s.points)) ⋯).map (AffineSubspace.subtype (affineSpan k (Set.range s.points)))
      ⋯ =
    s

Tactic:
rfl

Premises used: Affine.Simplex.map, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (s.reindex e).restrict S ⋯ = (s.restrict S hS).reindex e

Tactic:
rfl

Premises used: Affine.Simplex.reindex, Affine.Simplex.restrict, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty.{u_5 + 1} ↥S := ⋯
h₁ :
  ∀ (i : Fin (m + 1)),
    (↑(((s.restrict S hS).face h).points i) : P) = (↑(points ((s.face h).restrict S ⋯ : Simplex k (↥S) m) i) : P)
⊢ (s.restrict S hS).face h = (s.face h).restrict S ⋯

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty.{u_5 + 1} ↥S := ⋯
i : Fin (m + 1)
h₁ : (↑(((s.restrict S hS).face h).points i) : P) = (s.face h).points i
⊢ (↑(((s.restrict S hS).face h).points i) : P) = (↑(points ((s.face h).restrict S ⋯ : Simplex k (↥S) m) i) : P)

Tactic:
rw [restrict_points_coe]

Premises used: Affine.Simplex.restrict_points_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty.{u_5 + 1} ↥S := ⋯
i : Fin (m + 1)
h₁ :
  (↑((s.restrict S hS).points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i)) : P) =
    s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i)
⊢ (↑(((s.restrict S hS).face h).points i) : P) = (s.face h).points i

Tactic:
simp_rw [Affine.Simplex.face_points]

Premises used: Affine.Simplex.face_points
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
this : Nonempty.{u_5 + 1} ↥S := ⋯
i : Fin (m + 1)
⊢ (↑((s.restrict S hS).points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i)) : P) =
    s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Goal:
k : Type u_1
V : Type u_2
P : Type u_5
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ (s.restrict S hS).faceOpposite i = (s.faceOpposite i).restrict S ⋯

Tactic:
s.face_restrict hS _

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

Tactic:
⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩

Premises used: _private.0.Affine.Simplex.affineCombination_mem_setInterior_iff.match_1, And.intro, Iff.intro, Exists.intro, 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
I : Set 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
refine :
  Membership.mem (α := P) (Simplex.setInterior I s)
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) →
    ∀ (w' : Fin (n + 1) → k) (hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w' i) 1)
      (hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I)
      (hww' :
        Eq.{u_4 + 1} (α := P) ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w' : P)
          ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P))
      (i : Fin (n + 1)), w i ∈ I
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    ∀ (i : Fin (n + 1)), w i ∈ I

Tactic:
refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, 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
I : Set 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
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
w' : Fin (n + 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w' i) 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' :
  Eq.{u_4 + 1} (α := P) ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w' : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
simp_rw : ∀ (i : Fin (n + 1)), w' i ∈ I
⊢ ∀ (i : Fin (n + 1)), w i ∈ I

Tactic:
simp_rw [← (affineIndependent_iff_eq_of_fintype_affineCombination_eq k s.points).1
    s.independent w' w hw' hw hww']

Premises used: Affine.Simplex.points, affineIndependent_iff_eq_of_fintype_affineCombination_eq, Iff.mp, Affine.Simplex.independent
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
w' : Fin (n + 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w' i) 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' :
  Eq.{u_4 + 1} (α := P) ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w' : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ ∀ (i : Fin (n + 1)), w' i ∈ I

Tactic:
hw'01
-- 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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
w' : Fin (n + 1) → k
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w' i) 1
hw'01 : ∀ (i : Fin (n + 1)), w' i ∈ I
hww' :
  Eq.{u_4 + 1} (α := P) ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w' : P)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ ∀ (i : Fin (n + 1)), w' i ∈ I

Tactic:
exact hw'01
-- 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
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : ∀ (p : P), p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s
⊢ Simplex.setInterior I (s.reindex e) = Simplex.setInterior I s

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
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
⊢ p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s

Tactic:
⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩

Premises used: Affine.Simplex.setInterior, Affine.Simplex.reindex, Membership.mem, _private.0.Affine.Simplex.setInterior_reindex.match_1, _private.0.Affine.Simplex.setInterior_reindex.match_2, Iff.intro