case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : 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 := points✝, Independent := Independent✝ } i = points s2 i
⊢ { points := points✝, Independent := Independent✝ } = s2
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s1 s2 : Simplex k P n
h : ∀ (i : Fin (n + 1)), points s1 i = points s2 i
⊢ s1 = s2
cases s1
case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
points✝¹ : Fin (n + 1) → P
Independent✝¹ : AffineIndependent k points✝¹
points✝ : Fin (n + 1) → P
Independent✝ : AffineIndependent k points✝
h :
  ∀ (i : Fin (n + 1)),
    points { points := points✝¹, Independent := Independent✝¹ } i =
      points { points := points✝, Independent := Independent✝ } i
⊢ { points := points✝¹, Independent := Independent✝¹ } = { points := points✝, Independent := Independent✝ }
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : 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 := points✝, Independent := Independent✝ } i = points s2 i
⊢ { points := points✝, Independent := Independent✝ } = s2
cases s2
case mk.mk.e_points.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
points✝¹ : Fin (n + 1) → P
Independent✝¹ : AffineIndependent k points✝¹
points✝ : Fin (n + 1) → P
Independent✝ : AffineIndependent k points✝
h :
  ∀ (i : Fin (n + 1)),
    points { points := points✝¹, Independent := Independent✝¹ } i =
      points { points := points✝, Independent := Independent✝ } i
i : Fin (n + 1)
⊢ points✝¹ i = points✝ i
case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
points✝¹ : Fin (n + 1) → P
Independent✝¹ : AffineIndependent k points✝¹
points✝ : Fin (n + 1) → P
Independent✝ : AffineIndependent k points✝
h :
  ∀ (i : Fin (n + 1)),
    points { points := points✝¹, Independent := Independent✝¹ } i =
      points { points := points✝, Independent := Independent✝ } i
⊢ { points := points✝¹, Independent := Independent✝¹ } = { points := points✝, Independent := Independent✝ }
congr with i
no goals
case mk.mk.e_points.h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
points✝¹ : Fin (n + 1) → P
Independent✝¹ : AffineIndependent k points✝¹
points✝ : Fin (n + 1) → P
Independent✝ : AffineIndependent k points✝
h :
  ∀ (i : Fin (n + 1)),
    points { points := points✝¹, Independent := Independent✝¹ } i =
      points { points := points✝, Independent := Independent✝ } i
i : Fin (n + 1)
⊢ points✝¹ i = points✝ i
exact h i