awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
h : AffineSubspace.map φ E = F
y : P₁
hy : y ∈ E
hx : Membership.mem (α := P₂) F ((φ : (a : P₁) → P₂) y : P₂)
⊢ ∃ (a : ↥E),
    Eq.{u_5 + 1} (α := ↥F) ((φ.restrict ⋯ : (a : ↥E) → ↥F) a : ↥F)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) y) hx : ↥F)

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Restrict
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
E : AffineSubspace k P₁
inst_7 : Nonempty.{u_3 + 1} ↥E
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
⊢ Function.Bijective.{u_3 + 1, u_5 + 1} (α := ↥E) (β := ↥(AffineSubspace.map φ E))
    (⇑(φ.restrict ⋯) : (a : ↥E) → ↥(AffineSubspace.map φ E))

Tactic:
⟨AffineMap.restrict.injective hφ _, AffineMap.restrict.surjective _ rfl⟩

Premises used: AffineMap.restrict.injective, AffineMap.restrict.surjective, And.intro, Function.Bijective, 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₃
p : P
⊢ Subsingleton (Fin 1)

Tactic:
infer_instance
-- 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
p : P
i : Fin 1
⊢ points (mkOfPoint k p) i = p

Tactic:
rfl

Premises used: 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₃
⊢ Nonempty.{u_5 + 1} (Simplex k P 0)

Tactic:
⟨mkOfPoint k <| AddTorsor.nonempty.some⟩

Premises used: AddTorsor.nonempty, Nonempty.some, Nonempty.intro, Affine.Simplex.mkOfPoint
-- 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
p : P
⊢ Set.range (points (mkOfPoint k p)) = {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 : ℕ
s1 s2 : Simplex k P n
h : ∀ (i : Fin (n + 1)), s1.points i = s2.points i
mk :
  ∀ (points : Fin (n + 1) → P) (independent : AffineIndependent k points)
    (h : ∀ (i : Fin (n + 1)), { points := points, independent := independent : Simplex k P n }.points i = s2.points i),
    { points := points, independent := independent : Simplex k P n } = s2
⊢ s1 = s2

Tactic:
cases s1
-- 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 : ℕ
s2 : Simplex k P n
points : Fin (n + 1) → P
independent : AffineIndependent k points
h : ∀ (i : Fin (n + 1)), { points := points, independent := independent : Simplex k P n }.points i = s2.points i
mk :
  ∀ (points_1 : Fin (n + 1) → P) (independent_1 : AffineIndependent k points_1)
    (h :
      ∀ (i : Fin (n + 1)),
        { points := points, independent := independent : Simplex k P n }.points i =
          { points := points_1, independent := independent_1 : Simplex k P n }.points i),
    { points := points, independent := independent : Simplex k P n } =
      { points := points_1, independent := independent_1 }
⊢ { points := points, independent := independent : Simplex k P n } = s2

Tactic:
cases s2
-- 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 : ℕ
points : Fin (n + 1) → P
independent : AffineIndependent k points
points_1 : Fin (n + 1) → P
independent_1 : AffineIndependent k points_1
h :
  ∀ (i : Fin (n + 1)),
    { points := points, independent := independent : Simplex k P n }.points i =
      { points := points_1, independent := independent_1 : Simplex k P n }.points i
mk : ∀ (i : Fin (n + 1)), points i = points_1 i
⊢ { points := points, independent := independent : Simplex k P n } =
    { points := points_1, independent := independent_1 }

Tactic:
congr with 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 : ℕ
points : Fin (n + 1) → P
independent : AffineIndependent k points
points_1 : Fin (n + 1) → P
independent_1 : AffineIndependent k points_1
h :
  ∀ (i : Fin (n + 1)),
    { points := points, independent := independent : Simplex k P n }.points i =
      { points := points_1, independent := independent_1 : Simplex k P n }.points i
i : Fin (n + 1)
⊢ points i = points_1 i

Tactic:
h 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 : ℕ
points : Fin (n + 1) → P
independent : AffineIndependent k points
points_1 : Fin (n + 1) → P
independent_1 : AffineIndependent k points_1
h :
  ∀ (i : Fin (n + 1)),
    { points := points, independent := independent : Simplex k P n }.points i =
      { points := points_1, independent := independent_1 : Simplex k P n }.points i
i : Fin (n + 1)
⊢ points i = points_1 i

Tactic:
exact h 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
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (m + 1)
⊢ (s.face h).points i = s.points ((fs.orderEmbOfFin h : (a : Fin (m + 1)) → Fin (n + 1)) i)

Tactic:
rfl

Premises used: 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
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ (s.face h).points = s.points ∘ (⇑(fs.orderEmbOfFin h) : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
rfl

Premises used: 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
i : Fin (n + 1)
h : ∀ (i_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)), (s.face ⋯).points i_1 = points (mkOfPoint k (s.points i)) i_1
⊢ s.face ⋯ = mkOfPoint k (s.points i)

Tactic:
ext
-- 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
i : Fin (n + 1)
i_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ (s.face ⋯).points i_1 = points (mkOfPoint k (s.points i)) i_1

Tactic:
simp [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton]

Premises used: Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton
-- 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
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
rw :
  Set.range (ι := Fin (m + 1)) (s.points ∘ (⇑(fs.orderEmbOfFin h) : (a : Fin (m + 1)) → Fin (n + 1))) =
    s.points '' (↑fs : Set (Fin (n + 1)))
rw₁ :
  s.points '' Set.range (ι := Fin (m + 1)) (⇑(fs.orderEmbOfFin h) : (a : Fin (m + 1)) → Fin (n + 1)) =
    s.points '' (↑fs : Set (Fin (n + 1)))
rw₂ rw₃ : s.points '' (↑fs : Set (Fin (n + 1))) = s.points '' (↑fs : Set (Fin (n + 1)))
⊢ Set.range (s.face h).points = s.points '' (↑fs : Set (Fin (n + 1)))

Tactic:
rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]

Premises used: Set.range_comp, Finset.range_orderEmbOfFin, 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
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ LE.le (α := AffineSubspace k P) (affineSpan k (Set.range (s.face h).points)) (affineSpan k (Set.range s.points))

Tactic:
affineSpan_mono k (s.range_face_points h ▸ Set.image_subset_range _ _)

Premises used: Eq.rec, Set.image_subset_range, Affine.Simplex.range_face_points, affineSpan_mono, Eq.symm
-- 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
inst_4 : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
rw :
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points i) ↔ i ∈ fs
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range (s.face h).points)) (s.points i) ↔ i ∈ fs

Tactic:
rw [range_face_points]

Premises used: Affine.Simplex.range_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
inst_4 : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points i) ↔ i ∈ fs

Tactic:
s.independent.mem_affineSpan_iff i fs

Premises used: AffineIndependent.mem_affineSpan_iff, SetLike.coe, Affine.Simplex.independent
-- 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
inst_4 : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points i) ↔ i ∈ fs

Tactic:
exact s.independent.mem_affineSpan_iff i fs

Premises used: AffineIndependent.mem_affineSpan_iff, SetLike.coe, Affine.Simplex.independent
-- 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 : ℕ
inst_10 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ card (α := Fin (n + 1)) {i}ᶜ = n - 1 + 1

Tactic:
simp [card_compl, NeZero.one_le]

Premises used: Finset.card_compl, NeZero.one_le
-- 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
i : Fin (n + 1)
⊢ Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ

Tactic:
simp [faceOpposite]

Premises used: 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
n : ℕ
inst_4 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ LE.le (α := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
    (affineSpan k (Set.range s.points))

Tactic:
s.affineSpan_face_le _

Premises used: Affine.Simplex.affineSpan_face_le, Set.Mem
-- 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
inst_4 : Nontrivial k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
rw : Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ j ↔ j ≠ i
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points)) (s.points j) ↔ j ≠ i

Tactic:
rw [faceOpposite, s.points_mem_affineSpan_face]

Premises used: Affine.Simplex.points_mem_affineSpan_face, 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
inst_4 : Nontrivial k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i j : Fin (n + 1)
⊢ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ j ↔ j ≠ 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
inst_4 : Nontrivial k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
rw : ¬i ≠ i
⊢ s.points i ∉ affineSpan k (Set.range (s.faceOpposite i).points)

Tactic:
rw [points_mem_affineSpan_faceOpposite]

Premises used: Affine.Simplex.points_mem_affineSpan_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
inst_4 : Nontrivial k
n : ℕ
inst_5 : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ ¬i ≠ 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
i : Fin (n + 1)
j : Fin (n - 1 + 1)
simp_rw : (s.face ⋯).points j = s.points (i.succAbove (Fin.cast ⋯ j))
simp_rw₁ :
  (s.points ∘ (⇑(orderEmbOfFin {i}ᶜ ⋯) : (a : Fin (n - 1 + 1)) → Fin (n + 1))) j = s.points (i.succAbove (Fin.cast ⋯ j))
simp_rw₂ :
  s.points ((orderEmbOfFin {i}ᶜ ⋯ : (a : Fin (n - 1 + 1)) → Fin (n + 1)) j) = s.points (i.succAbove (Fin.cast ⋯ j))
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))

Tactic:
simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]

Premises used: Affine.Simplex.face, Function.comp_apply, Affine.Simplex.faceOpposite, Finset.orderEmbOfFin_compl_singleton_apply
-- 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
s : Simplex k P 1
i : Fin 2
n : Fin 1
⊢ i.rev = i.succAbove n

Tactic:
decide +revert
-- 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
s : Simplex k P 1
i : Fin 2
n : Fin 1
⊢ i.rev = i.succAbove n

Tactic:
have h : i.rev = Fin.succAbove i n := by decide +revert
-- 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
s : Simplex k P 1
i : Fin 2
n : Fin 1
h : i.rev = i.succAbove n
⊢ (s.faceOpposite i).points n = s.points i.rev

Tactic:
simp [h, faceOpposite_point_eq_point_succAbove]

Premises used: Affine.Simplex.faceOpposite_point_eq_point_succAbove
-- 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
s : Simplex k P 1
n : Fin 1
⊢ (s.faceOpposite 0).points n = s.points 1

Tactic:
s.faceOpposite_point_eq_point_rev _ _

Premises used: Fin.ofNat, Affine.Simplex.faceOpposite_point_eq_point_rev
-- 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
s : Simplex k P 1
n : Fin 1
⊢ (s.faceOpposite 1).points n = s.points 0

Tactic:
s.faceOpposite_point_eq_point_rev _ _

Premises used: Fin.ofNat, Affine.Simplex.faceOpposite_point_eq_point_rev
-- 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₃
α : Type u_8
inst_10 : Nontrivial α
i : α
⊢ Nonempty.{u_8 + 1} (↑{i}ᶜ : Type u_8)

Tactic:
(Set.nonempty_compl_of_nontrivial i).to_subtype

Premises used: Set.nonempty_compl_of_nontrivial, Set.Nonempty.to_subtype
-- 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
inst_4 : Nontrivial k
n : ℕ
s : Simplex k P n
fs : Set (Fin (n + 1))
i : Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' fs)) (s.points i) ↔ i ∈ fs

Tactic:
s.independent.mem_affineSpan_iff _ _

Premises used: AffineIndependent.mem_affineSpan_iff, Affine.Simplex.independent
-- 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)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    w i = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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)
refine_1 :
  ∀
    (h :
      Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
        ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)),
    w i = 0
refine_2 :
  ∀ (h : w i = 0),
    Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
      ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) ↔
    w i = 0

Tactic:
refine ⟨fun h ↦ ?_, fun 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 :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
    ((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 [range_faceOpposite_points] at h

Premises used: Affine.Simplex.range_faceOpposite_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 : ℕ
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 :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ i ∉ {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
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
i : Fin (n + 1)
h :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ w i = 0

Tactic:
exact s.independent.eq_zero_of_affineCombination_mem_affineSpan hw h (Finset.mem_univ i)
      (by simp)

Premises used: Finset.mem_univ, Affine.Simplex.independent, AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan
-- 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
refine_2 :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)

Tactic:
rw [range_faceOpposite_points]

Premises used: Affine.Simplex.range_faceOpposite_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 : ℕ
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
refine_2 :
  ∀ (hk : Subsingleton 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)
refine_2₁ :
  ∀ (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)
⊢ 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:
rcases subsingleton_or_nontrivial k with hk | hk

Premises used: subsingleton_or_nontrivial
-- 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
⊢ Subsingleton V

Tactic:
have : Subsingleton V := Module.subsingleton k _
-- 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 : Subsingleton V
⊢ Subsingleton P

Tactic:
have : Subsingleton P := (AddTorsor.subsingleton_iff V P).1 inferInstance