awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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
hEF : AffineSubspace.map φ E ≤ F
refine_1 : ↥E → ↥F
refine_2 : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction
⊢ AffineMap.{u_1, u_2, u_3, u_4, u_5} k ↥E ↥F
have refine_3 : ∀ (p : ↥E) (v : ↥E.direction),
  Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑(v +ᵥ p) : P₁)) sorry =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := ↥F.direction) (β := ↥F)
      (((φ.linear.restrict sorry : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
            (a : ↥E.direction) → ↥F.direction)
          v :
        ↥F.direction)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑p : P₁)) sorry : ↥F)
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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
hEF : AffineSubspace.map φ E ≤ F
⊢ LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction
have refine_2 : E.direction ≤ Submodule.comap φ.linear F.direction
Tactic: refine φ.linear.restrict (?_ : E.direction ≤ F.direction.comap φ.linear)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction
have refine_2 : (AffineSubspace.map φ E).direction ≤ F.direction
Tactic: rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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
hEF : AffineSubspace.map φ E ≤ F
p : ↥E
v : ↥E.direction
⊢ Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑(v +ᵥ p) : P₁)) ⋯ =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := ↥F.direction) (β := ↥F)
      (((φ.linear.restrict ⋯ : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
            (a : ↥E.direction) → ↥F.direction)
          v :
        ↥F.direction)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) (↑p : P₁)) ⋯ : ↥F)
have refine_3 : (φ : (a : P₁) → P₂) ((↑v : V₁) +ᵥ (↑p : P₁)) =
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V₂) (β := P₂)
    (↑(((φ.linear.restrict sorry : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction) :
            (a : ↥E.direction) → ↥F.direction)
          v) :
      V₂)
    ((φ : (a : P₁) → P₂) (↑p : P₁) : P₂)
Tactic: simp only [Subtype.ext_iff, AffineSubspace.coe_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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₂
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction
have rw : (AffineSubspace.map φ E).direction ≤ F.direction
Tactic: rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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₂
hφ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P₁) (β := P₂) (⇑φ : (a : P₁) → P₂)
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
x y : ↥E
h : Eq.{u_5 + 1} (α := ↥F) ((φ.restrict hEF : (a : ↥E) → ↥F) x : ↥F) ((φ.restrict hEF : (a : ↥E) → ↥F) y : ↥F)
⊢ x = y
have simp : ∀ (h : Eq.{u_5 + 1} (α := P₂) ((φ : (a : P₁) → P₂) (↑x : P₁) : P₂) ((φ : (a : P₁) → P₂) (↑y : P₁) : P₂)),
  (↑x : P₁) = (↑y : P₁)
Tactic: simp only [Subtype.ext_iff, AffineMap.restrict.coe_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (hypothesis)
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
x : P₂
hx : x ∈ F
⊢ ∃ (a : ↥E), (φ.restrict ⋯ : (a : ↥E) → ↥F) a = Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) x hx
have hx₁ : ∃ y ∈ E, (φ : (a : P₁) → P₂) y = x
Tactic: rw [← h, AffineSubspace.mem_map] at hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
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
x : P₂
hx_1 : x ∈ F
hx : ∃ y ∈ E, (φ : (a : P₁) → P₂) y = x
⊢ ∃ (a : ↥E), (φ.restrict ⋯ : (a : ↥E) → ↥F) a = Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) x hx_1
have obtain : ∀ (y : P₁) (hy : y ∈ E) (hx : Membership.mem (α := P₂) F ((φ : (a : P₁) → P₂) y : P₂)),
  ∃ (a : ↥E),
    Eq.{u_5 + 1} (α := ↥F) ((φ.restrict sorry : (a : ↥E) → ↥F) a : ↥F)
      (Subtype.mk (p := fun (x : P₂) ↦ x ∈ F) ((φ : (a : P₁) → P₂) y) hx : ↥F)
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ s1 = s2
have 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
Tactic: cases s1
Cleared hypotheses: s1, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ { points := points, independent := independent : Simplex k P n } = s2
have 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 }
Tactic: cases s2
Cleared hypotheses: s2, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ { points := points, independent := independent : Simplex k P n } =
    { points := points_1, independent := independent_1 }
have mk : ∀ (i : Fin (n + 1)), points i = points_1 i
Tactic: congr with i
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ s.face ⋯ = mkOfPoint k (s.points i)
have h : ∀ (i_1 : Fin (HAdd.hAdd (α := ℕ) 0 1)), (s.face sorry).points i_1 = points (mkOfPoint k (s.points i)) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ Set.range (s.face h).points = s.points '' (↑fs : Set (Fin (n + 1)))
have 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)))
Tactic: rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)))
⊢ Set.range (s.face h).points = s.points '' (↑fs : Set (Fin (n + 1)))
have 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)))
Tactic: rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)))
⊢ Set.range (s.face h).points = s.points '' (↑fs : Set (Fin (n + 1)))
have rw₂ : s.points '' (↑fs : Set (Fin (n + 1))) = s.points '' (↑fs : Set (Fin (n + 1)))
Tactic: rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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 (Set.range (s.face h).points)) (s.points i) ↔ i ∈ fs
have rw : Membership.mem (γ := AffineSubspace k P) (affineSpan k (s.points '' (↑fs : Set (Fin (n + 1))))) (s.points i) ↔ i ∈ fs
Tactic: rw [range_face_points]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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 (γ := AffineSubspace k P) (affineSpan k (Set.range (s.faceOpposite i).points)) (s.points j) ↔ j ≠ i
have rw : Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ j ↔ j ≠ i
Tactic: rw [faceOpposite, s.points_mem_affineSpan_face]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ s.points i ∉ affineSpan k (Set.range (s.faceOpposite i).points)
have rw : ¬i ≠ i
Tactic: rw [points_mem_affineSpan_faceOpposite]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))
have simp_rw : (s.face sorry).points j = s.points (i.succAbove (Fin.cast sorry j))
Tactic: simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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))
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))
have simp_rw₁ : (s.points ∘ (⇑(orderEmbOfFin {i}ᶜ sorry) : (a : Fin (n - 1 + 1)) → Fin (n + 1))) j = s.points (i.succAbove (Fin.cast sorry j))
Tactic: simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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))
⊢ (s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))
have simp_rw₂ : s.points ((orderEmbOfFin {i}ᶜ sorry : (a : Fin (n - 1 + 1)) → Fin (n + 1)) j) = s.points (i.succAbove (Fin.cast sorry j))
Tactic: simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ (s.faceOpposite i).points n = s.points i.rev
have h : i.rev = i.succAbove n
Tactic: have h : i.rev = Fin.succAbove i n := by decide +revert
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
have 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
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ 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
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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)
⊢ w i = 0
have 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)
Tactic: rw [range_faceOpposite_points] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [range_faceOpposite_points]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have 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)
Tactic: rcases subsingleton_or_nontrivial k with hk | hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have 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)
Tactic: rcases subsingleton_or_nontrivial k with hk | hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have this : Subsingleton V
Tactic: have : Subsingleton V := Module.subsingleton k _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have this₁ : Subsingleton P
Tactic: have : Subsingleton P := (AddTorsor.subsingleton_iff V P).1 inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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 (α := P) (γ := AffineSubspace k P) (affineSpan k (s.points '' {i}ᶜ))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have 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)
Tactic: rw [(affineSpan_eq_top_iff_nonempty_of_subsingleton k).2 (by simp)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ (s.reindex e).reindex e.symm = s
have rw : s.reindex (e.trans e.symm) = s
Tactic: rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ (s.reindex e).reindex e.symm = s
have rw₁ : s.reindex (Equiv.refl (Fin (m + 1))) = s
Tactic: rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
⊢ (s.reindex e).reindex e.symm = s
have rw₂ : s = s
Tactic: rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]