Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
k : Nat
Γ₁ Γ : List VExpr
e1 e2 A : VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ₁ Γ
H : IsDefEqStrong env U Γ₁ e1 e2 A
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst e1 e₀ k) (inst e2 e₀ k) (inst A e₀ k)
Tactic:
induction H generalizing Γ k with
| @bvar _ i ty _ h _ h2 ih =>
  dsimp [inst]; clear h2 ih
  induction W generalizing i ty with
  | zero =>
    cases h with simp [inst_lift]
    | zero => exact h₀
    | succ h =>
      let ⟨u, hty⟩ := hΓ₀.lookup henv h
      exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
  | succ _ ih =>
    cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
    | zero =>
      let ⟨u, hty⟩ := hΓ.lookup henv .zero
      exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
    | succ h => exact (ih h hΓ.1).weakN henv .one
| symm _ ih => exact .symm (ih W hΓ)
| trans _ _ ih1 ih2 => exact .trans (ih1 W hΓ) (ih2 W hΓ)
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| constDF h1 h2 h3 h4 h5 h6 h7 h8 _ _ _ _ ih3 ih4 =>
  simp [(henv.closedC h1).instL.instN_eq (Nat.zero_le _)] at ih3 ih4 ⊢
  exact .constDF h1 h2 h3 h4 h5 h6 h7 h8 (ih3 W hΓ) (ih4 W hΓ)
| appDF h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact inst0_inst_hi .. ▸ .appDF h1 h2
    (ih1 W hΓ) (ih2 W.succ ⟨hΓ, _, ih1 W hΓ⟩)
    (ih3 W hΓ) (ih4 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih5 W hΓ)
| lamDF h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact
    have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
    have hΓ'' := ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩
    .lamDF h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ'') (ih4 W.succ hΓ') (ih5 W.succ hΓ'')
| forallEDF h1 h2 _ _ _ ih1 ih2 ih3 =>
  exact .forallEDF h1 h2 (ih1 W hΓ)
    (ih2 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩) (ih3 W.succ ⟨hΓ, _, (ih1 W hΓ).hasType.2⟩)
| defeqDF h1 _ _ ih1 ih2 => exact .defeqDF h1 (ih1 W hΓ) (ih2 W hΓ)
| beta h1 h2 _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 ih6 =>
  rw [inst0_inst_hi, inst0_inst_hi]; exact
    have hΓ' := ⟨hΓ, _, ih1 W hΓ⟩
    .beta h1 h2
      (ih1 W hΓ) (ih2 W.succ hΓ') (ih3 W.succ hΓ') (ih4 W hΓ)
      (inst0_inst_hi .. ▸ ih5 W hΓ) (inst0_inst_hi .. ▸ inst0_inst_hi .. ▸ ih6 W hΓ)
| eta h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  have :=
    have hΓ' := ⟨hΓ, _, (ih1 W hΓ).hasType.1⟩
    IsDefEqStrong.eta h1 h2 (ih1 W hΓ) (ih2 W.succ hΓ')
      (by
        have := ih3 W.succ.succ ⟨hΓ', _, by
          rw [← lift_instN_lo]; exact (ih1 W hΓ).hasType.1.weakN henv .one⟩
        rwa [lift_instN_lo, liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
      (ih4 W hΓ)
      (by
        have := ih5 W.succ hΓ'
        simp only [inst, ← lift_instN_lo] at this
        rwa [liftN_instN_lo (hj := Nat.le_add_left ..), Nat.add_comm 1])
  rw [lift, liftN_instN_lo (hj := Nat.zero_le _), Nat.add_comm] at this
  simpa [inst]
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel (ih1 W hΓ) (ih2 W hΓ) (ih3 W hΓ)
| extra h1 h2 h3 h4 h5 h6 h7 _ _ _ _ _ ih4 ih5 =>
  have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
  simp [
    hA1.instL.instN_eq (Nat.zero_le _),
    hA2.instL.instN_eq (Nat.zero_le _),
    hA3.instL.instN_eq (Nat.zero_le _)] at ih4 ih5 ⊢
  exact .extra h1 h2 h3 h4 h5 h6 h7 (ih4 W hΓ) (ih5 W hΓ)
Proof state after:
no goals