-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem ext {n : ℕ} {s1 s2 : Simplex k P n} (h : ∀ i, s1.points i = s2.points i) : s1 = s2

Proof state:
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✝, independent := independent✝ }.points i = s2.points i
⊢ { points := points✝, independent := independent✝ } = s2

Tactic:
cases s2

Result:
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✝¹, independent := independent✝¹ }.points i =
      { points := points✝, independent := independent✝ }.points i
⊢ { points := points✝¹, independent := independent✝¹ } = { points := points✝, independent := independent✝ }

Proof state:
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✝¹, independent := independent✝¹ }.points i =
      { points := points✝, independent := independent✝ }.points i
⊢ { points := points✝¹, independent := independent✝¹ } = { points := points✝, independent := independent✝ }

Tactic:
congr with i

Result:
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✝¹, independent := independent✝¹ }.points i =
      { points := points✝, independent := independent✝ }.points i
i : Fin (n + 1)
⊢ points✝¹ i = points✝ i

Proof state:
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)), s1.points i = s2.points i
⊢ s1 = s2

Tactic:
cases s1

Result:
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✝, independent := independent✝ }.points i = s2.points i
⊢ { points := points✝, independent := independent✝ } = s2

Proof state:
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✝¹, independent := independent✝¹ }.points i =
      { points := points✝, independent := independent✝ }.points i
i : Fin (n + 1)
⊢ points✝¹ i = points✝ i

Tactic:
exact h i

Result:
no goals