awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e.symm).reindex e = s
have rw : s.reindex (e.symm.trans e) = s
Tactic: rw [← reindex_trans, Equiv.symm_trans_self, 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 (n + 1) ≃ Fin (m + 1)
rw : s.reindex (e.symm.trans e) = s
⊢ (s.reindex e.symm).reindex e = s
have rw₁ : s.reindex (Equiv.refl (Fin (m + 1))) = s
Tactic: rw [← reindex_trans, Equiv.symm_trans_self, 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 (n + 1) ≃ Fin (m + 1)
rw : s.reindex (e.symm.trans e) = s
rw₁ : s.reindex (Equiv.refl (Fin (m + 1))) = s
⊢ (s.reindex e.symm).reindex e = s
have rw₂ : s = s
Tactic: rw [← reindex_trans, Equiv.symm_trans_self, 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)
⊢ Set.range (s.reindex e).points = Set.range s.points
have rw : Set.range
    { points := s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)), independent := sorry : Simplex k P n }.points =
  Set.range s.points
Tactic: rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]
-- 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 :
  Set.range
      { points := s.points ∘ (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)), independent := ⋯ : Simplex k P n }.points =
    Set.range s.points
⊢ Set.range (s.reindex e).points = Set.range s.points
have rw₁ : s.points '' Set.range (ι := Fin (n + 1)) (⇑e.symm : (a : Fin (n + 1)) → Fin (m + 1)) = Set.range s.points
Tactic: rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]
-- 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 :
  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
⊢ Set.range (s.reindex e).points = Set.range s.points
have rw₂ : s.points '' Set.univ = Set.range s.points
Tactic: rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]
-- 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 :
  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
⊢ Set.range (s.reindex e).points = Set.range s.points
have rw₃ : Set.range s.points = Set.range s.points
Tactic: rw [reindex, Set.range_comp, Equiv.range_eq_univ, Set.image_univ]
-- 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)
fs : Finset (Fin (n + 1))
n' : ℕ
h : #fs = n' + 1
⊢ Set.range ((s.reindex e).face h).points =
    Set.range (ι := Fin (n' + 1)) (points (s.face (fs := Finset.map e.symm.toEmbedding fs) ⋯))
have 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)))
Tactic: simp only [range_face_points, reindex_points, Set.image_comp]
-- 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 : ℕ
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 ((s.reindex e).faceOpposite i).points =
    Set.range (s.faceOpposite ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i)).points
have rw : Set.range (ι := Fin (n - 1 + 1)) (points (s.face (fs := Finset.map e.symm.toEmbedding {i}ᶜ) sorry)) =
  Set.range (s.faceOpposite ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i)).points
Tactic: rw [faceOpposite, range_face_reindex]
-- 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
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 := ⋯
⊢ (s.restrict S hS).face h = (s.face h).restrict S ⋯
have h₁ : ∀ (i : Fin (m + 1)),
  (↑(((s.restrict S hS).face h).points i) : P) = (↑(points ((s.face h).restrict S sorry : Simplex k (↥S) m) i) : P)
Tactic: ext 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
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).face h).points i) : P) = (↑(points ((s.face h).restrict S ⋯ : Simplex k (↥S) m) i) : P)
have h₁ : (↑(((s.restrict S hS).face h).points i) : P) = (s.face h).points i
Tactic: rw [restrict_points_coe]
-- 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
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).face h).points i) : P) = (s.face h).points i
have 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)
Tactic: simp_rw [Affine.Simplex.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_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
have 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
Tactic: refine ⟨fun ⟨w', hw', hw'01, hww'⟩ ↦ ?_, fun h ↦ ⟨w, hw, h, rfl⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
⊢ Simplex.setInterior I (s.reindex e) = Simplex.setInterior I s
have h : ∀ (p : P), p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
have h : p ∈ Simplex.setInterior I (s.reindex e) →
  ∀ (w : Fin (m + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1) (hwI : ∀ (i : Fin (m + 1)), w i ∈ I)
    (h : (affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w = p), p ∈ Simplex.setInterior I s
Tactic: refine ⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
h :
  p ∈ Simplex.setInterior I (s.reindex e) →
    ∀ (w : Fin (m + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1) (hwI : ∀ (i : Fin (m + 1)), w i ∈ I)
      (h : (affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w = p),
      p ∈ Simplex.setInterior I s
⊢ p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s
have h₁ : p ∈ Simplex.setInterior I s →
  ∀ (w : Fin (n + 1) → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1) (hwI : ∀ (i : Fin (n + 1)), w i ∈ I)
    (h : (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w = p), p ∈ Simplex.setInterior I (s.reindex e)
Tactic: refine ⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
h_1 : p ∈ Simplex.setInterior I (s.reindex e)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h : (affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w = p
⊢ p ∈ Simplex.setInterior I s
have h₁ : Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P) →
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
Tactic: subst h
Cleared hypotheses: p, h_1, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
have h : Membership.mem (α := P) (Simplex.setInterior I s)
  ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P) w :
    P)
Tactic: simp_rw [reindex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P) w :
      P)
have h : Membership.mem (α := P) (Simplex.setInterior I s)
  ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) : P)
Tactic: rw [← Function.comp_id w, ← e.self_comp_symm, ← Function.comp_assoc,
      ← Equiv.coe_toEmbedding, ← Finset.univ.affineCombination_map e.symm.toEmbedding,
      map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
have rwa : (Finset.map e.toEmbedding univ).sum w = 1
Tactic: rwa [sum_comp_equiv, map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) : P)
have hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
Tactic: have hw' : ∑ i, (w ∘ e) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (m + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), w i) 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i) 1
⊢ Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) : P)
have h : ∀ (i : Fin (n + 1)), (w ∘ (⇑e : (a : Fin (n + 1)) → Fin (m + 1))) i ∈ I
Tactic: rw [affineCombination_mem_setInterior_iff hw']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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
h_1 : p ∈ Simplex.setInterior I s
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h : (affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w = p
⊢ p ∈ Simplex.setInterior I (s.reindex e)
have h₁ : Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P) →
  Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
Tactic: subst h
Cleared hypotheses: p, h_1, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
have h : Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
  ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P)
      (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
    P)
Tactic: rw [← Function.comp_id w, ← Function.comp_id s.points, ← e.symm_comp_self,
      ← Function.comp_assoc, ← Function.comp_assoc, ← e.coe_toEmbedding,
      ← Finset.univ.affineCombination_map e.toEmbedding, map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
have h : Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
  ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P)
      (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
    P)
Tactic: change Finset.univ.affineCombination k (s.reindex e).points _ ∈ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
have rwa : (Finset.map e.symm.toEmbedding univ).sum w = 1
Tactic: rwa [sum_comp_equiv, map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (hypothesis)
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)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
have hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
Tactic: have hw' : ∑ i, (w ∘ e.symm) i = 1 := by rwa [sum_comp_equiv, map_univ_equiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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)
w : Fin (n + 1) → k
hw : Eq.{u_1 + 1} (α := k) (∑ i : Fin (n + 1), w i) 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h :
  Membership.mem (α := P) (Simplex.setInterior I s)
    ((affineCombination k univ s.points : (a : Fin (n + 1) → k) → P) w : P)
hw' : Eq.{u_1 + 1} (α := k) (∑ i : Fin (m + 1), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i) 1
⊢ Membership.mem (α := P) (Simplex.setInterior I (s.reindex e))
    ((affineCombination k univ (s.reindex e).points : (a : Fin (m + 1) → k) → P)
        (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
have h : ∀ (i : Fin (m + 1)), (w ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i ∈ I
Tactic: rw [affineCombination_mem_setInterior_iff hw']
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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₂)
⊢ Simplex.setInterior I (s.map f hf) = (⇑f : (a : P) → P₂) '' Simplex.setInterior I s
have h : ∀ (p : P₂),
  p ∈ Simplex.setInterior I (s.map f hf) ↔
    Membership.mem (γ := Set P₂) ((⇑f : (a : P) → P₂) '' Simplex.setInterior I s) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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₂
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have pos : ∀ (hp : Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p),
  p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
Tactic: by_cases hp : p ∈ affineSpan k (Set.range (s.map f hf).points)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic (goal)
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₂
pos :
  ∀ (hp : Membership.mem (γ := AffineSubspace k P₂) (affineSpan k (Set.range (s.map f hf).points)) p),
    p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
⊢ p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
have neg : ∀ (hp : p ∉ affineSpan k (Set.range (s.map f hf).points)),
  p ∈ Simplex.setInterior I (s.map f hf) ↔ ∃ x ∈ Simplex.setInterior I s, (f : (a : P) → P₂) x = p
Tactic: by_cases hp : p ∈ affineSpan k (Set.range (s.map f hf).points)