Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case «0»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨0, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨0, ⋯⟩).succ)

pp: case «1»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨1, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨1, ⋯⟩).succ)

pp: case «2»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨2, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨2, ⋯⟩).succ)

pp: case «3»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨3, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨3, ⋯⟩).succ)

Tactic:
;

Goal state after:
case «0»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨0, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨0, ⋯⟩).succ)

case «1»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨1, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨1, ⋯⟩).succ)

case «2»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨2, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨2, ⋯⟩).succ)

case «3»
k : Type u_1
inst✝¹⁸ : DivisionRing k
V₀ V₁ V₂ V₃ V₄ V₅ : Type u₀
inst✝¹⁷ : AddCommGroup V₀
inst✝¹⁶ : Module k V₀
inst✝¹⁵ : FiniteDimensional k V₀
inst✝¹⁴ : AddCommGroup V₁
inst✝¹³ : Module k V₁
inst✝¹² : FiniteDimensional k V₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : FiniteDimensional k V₂
inst✝⁸ : AddCommGroup V₃
inst✝⁷ : Module k V₃
inst✝⁶ : FiniteDimensional k V₃
inst✝⁵ : AddCommGroup V₄
inst✝⁴ : Module k V₄
inst✝³ : FiniteDimensional k V₄
inst✝² : AddCommGroup V₅
inst✝¹ : Module k V₅
inst✝ : FiniteDimensional k V₅
f₀ : V₀ →ₗ[k] V₁
f₁ : V₁ →ₗ[k] V₂
f₂ : V₂ →ₗ[k] V₃
f₃ : V₃ →ₗ[k] V₄
f₄ : V₄ →ₗ[k] V₅
inj : Injective ⇑f₀
exact₁ : Exact ⇑f₀ ⇑f₁
exact₂ : Exact ⇑f₁ ⇑f₂
exact₃ : Exact ⇑f₂ ⇑f₃
exact₄ : Exact ⇑f₃ ⇑f₄
surj : Surjective ⇑f₄
Vs : Fin (Nat.succ 0).succ.succ.succ.succ.succ → Type u₀ := ![V₀, V₁, V₂, V₃, V₄, V₅]
this✝¹ : (i : Fin 6) → AddCommGroup (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁷
    | 1 => inst✝¹⁴
    | 2 => inst✝¹¹
    | 3 => inst✝⁸
    | 4 => inst✝⁵
    | 5 => inst✝²
this✝ : (i : Fin 6) → Module k (Vs i) :=
  fun i ↦
    match i with
    | 0 => inst✝¹⁶
    | 1 => inst✝¹³
    | 2 => inst✝¹⁰
    | 3 => inst✝⁷
    | 4 => inst✝⁴
    | 5 => inst✝¹
this : ∀ (i : Fin 6), FiniteDimensional k (Vs i)
fs : (i : Fin 5) → Vs i.castSucc →ₗ[k] Vs i.succ :=
  fun i ↦
    match i with
    | 0 => f₀
    | 1 => f₁
    | 2 => f₂
    | 3 => f₃
    | 4 => f₄
⊢ Exact ⇑(fs ((fun i ↦ i) ⟨3, ⋯⟩).castSucc) ⇑(fs ((fun i ↦ i) ⟨3, ⋯⟩).succ)