no goals
n m : ℕ
C : Fin (n + 1) → Sort u_1
⊢ { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
simp only [mk_zero]
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
i : Fin (n + 1)
h : { val := 0, isLt := (_ : 0 < Nat.succ n) } = i
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
h0 : C 0
⊢ C 0
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
i : Fin (n + 1)
h : { val := 0, isLt := (_ : 0 < Nat.succ n) } = i
h0 : C i
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
⊢ C 0
simp [← h] at h0
no goals
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
i : Fin (n + 1)
h : { val := 0, isLt := (_ : 0 < Nat.succ n) } = i
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
h0 : C 0
⊢ C 0
exact h0
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
h0 : C { val := 0, isLt := (_ : 0 < Nat.succ n) }
hs✝ : (i : Fin n) → C (↑castSucc i) → C (succ i)
⊢ (let_fun this := fun i =>
        induction
          (Eq.mp (_ : C { val := 0, isLt := (_ : 0 < Nat.succ n) } = C { val := 0, isLt := (_ : 0 < Nat.succ n) }) h0)
          hs✝ i;
      this)
      { val := 0, isLt := (_ : 0 < Nat.succ n) } =
    h0
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
⊢ (fun i h =>
      ∀ (h0 : C i) (hs : (i : Fin n) → C (↑castSucc i) → C (succ i)),
        (let_fun this := fun i_1 =>
              induction (Eq.mp (_ : C i = C { val := 0, isLt := (_ : 0 < Nat.succ n) }) h0) hs i_1;
            this)
            i =
          h0)
    { val := 0, isLt := (_ : 0 < Nat.succ n) }
    (_ : { val := 0, isLt := (_ : 0 < Nat.succ n) } = { val := 0, isLt := (_ : 0 < Nat.succ n) })
intros h0 _
no goals
n m : ℕ
C : Fin (n + 1) → Sort u_1
this : { val := 0, isLt := (_ : 0 < Nat.succ n) } = 0
h0 : C { val := 0, isLt := (_ : 0 < Nat.succ n) }
hs✝ : (i : Fin n) → C (↑castSucc i) → C (succ i)
⊢ (let_fun this := fun i =>
        induction
          (Eq.mp (_ : C { val := 0, isLt := (_ : 0 < Nat.succ n) } = C { val := 0, isLt := (_ : 0 < Nat.succ n) }) h0)
          hs✝ i;
      this)
      { val := 0, isLt := (_ : 0 < Nat.succ n) } =
    h0
simp [induction]