Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
env : VEnv
Δ Δ₂ : VLCtx
dk n k : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂
H : TrExpr env Us Δ₁ e e'
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) e dk
⊢ ∃ e', TrExpr env Us Δ e e'
Tactic:
induction H generalizing Δ Δ₂ dk k with
| @bvar e A Δ₁ i h1 =>
  suffices ∃ p, Δ.find? (.inl i) = some p from let ⟨_, h⟩ := this; ⟨_, .bvar h⟩
  simp [InScope] at hs
  induction W generalizing i e A Δ₁ with | @cons_bvar _ Δ₂ _ _ _ d W ih => ?_ | _ => cases hs
  obtain ⟨d, Δ₂, rfl, hΔ₁⟩ : ∃ d Δ₁', Δ₁ = (none, d) :: Δ₁' ∧
      VLCtx.IsDefEq env Us.length Δ₁' Δ₂ := by cases d <;> cases hΔ <;> exact ⟨_, _, rfl, ‹_›⟩
  simp [VLCtx.find?] at h1 ⊢
  rcases i with _ | i <;> simp [VLCtx.next, bind] at h1 ⊢
  obtain ⟨_, h1, _⟩ := h1
  have ⟨_, h1⟩ := ih h1 hΔ₁ (Nat.lt_of_succ_lt_succ hs)
  exact ⟨_, _, h1, rfl⟩
| @fvar e A _ fv h1 => let ⟨_, h⟩ := VLCtx.find?_eq_some.2 hs; exact ⟨_, .fvar h⟩
| sort h1 => exact ⟨_, .sort h1⟩
| const h1 h2 h3 => exact ⟨_, .const h1 h2 h3⟩
| app h1 h2 hf ha ih1 ih2 =>
  have hΔ₁ := hΔ.wf; have hΔ₂ := (hΔ.symm henv).wf
  let ⟨f₁, ih1⟩ := ih1 W hΔ hs.1
  let ⟨a₁, ih2⟩ := ih2 W hΔ hs.2
  have h1 := h1.defeqU_l henv hΔ₁.toCtx <| hf.uniq henv hΔ (ih1.weakN henv W hΔ₂)
  have h2 := h2.defeqU_l henv hΔ₁.toCtx <| ha.uniq henv hΔ (ih2.weakN henv W hΔ₂)
  have := VExpr.WF.weakN_iff henv hΔ₂.toCtx W.toCtx (e := f₁.app a₁)
  have := this.1 ⟨_, (h1.app h2).defeqDFC henv hΔ.defeqCtx⟩
  have ⟨_, _, h1, h2⟩ := this.app_inv henv (W.wf henv hΔ₂).toCtx
  exact ⟨_, .app h1 h2 ih1 ih2⟩
| lam h1 ht hb ih1 ih2 =>
  let ⟨_, h1⟩ := h1
  have hΔ₁ := hΔ.wf; have hΔ₂ := (hΔ.symm henv).wf
  let ⟨ty₁, ih1⟩ := ih1 W hΔ hs.1
  have htt := ht.uniq henv hΔ (ih1.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h1
  have ⟨_, ih2⟩ := ih2 (W.cons_bvar (.vlam _))
    (hΔ.cons (ofv := none) nofun <| .vlam htt) hs.2.fvars_cons
  have h1 := HasType.weakN_iff (A := .sort _) henv hΔ₂.toCtx W.toCtx
    |>.1 (htt.hasType.2.defeqDFC henv hΔ.defeqCtx)
  exact ⟨_, .lam ⟨_, h1⟩ ih1 ih2⟩
| forallE h1 h2 ht hb ih1 ih2 =>
  let ⟨_, h1⟩ := h1; let ⟨_, h2⟩ := h2
  have hΔ₁ := hΔ.wf; have hΔ₂ := (hΔ.symm henv).wf
  let ⟨ty₁, ih1⟩ := ih1 W hΔ hs.1
  have htt := ht.uniq henv hΔ (ih1.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h1
  have hΔ' := hΔ.cons (ofv := none) nofun <| .vlam htt
  have ⟨_, ih2⟩ := ih2 (W.cons_bvar (.vlam _)) hΔ' hs.2.fvars_cons
  have h1' := htt.hasType.2.defeqDFC henv hΔ.defeqCtx
  have h1 := HasType.weakN_iff (A := .sort _) henv hΔ₂.toCtx W.toCtx |>.1 h1'
  have hΔ₂' : VLCtx.WF _ _ ((none, .vlam _) :: _) := ⟨hΔ₂, nofun, _, h1'⟩
  have h2 := (HasType.weakN_iff (A := .sort _) henv hΔ₂'.toCtx (W.cons_bvar (.vlam _)).toCtx).1 <|
    hb.uniq henv hΔ' (ih2.weakN henv (W.cons_bvar _) hΔ₂')
    |>.of_l (Γ := _::_) henv ⟨hΔ₁.toCtx, _, htt.hasType.1⟩ h2
    |>.hasType.2.defeqDFC henv (.succ hΔ.defeqCtx htt)
  exact ⟨_, .forallE ⟨_, h1⟩ ⟨_, h2⟩ ih1 ih2⟩
| letE h1 ht hv hb ih1 ih2 ih3 =>
  have hΔ₁ := hΔ.wf; have hΔ₂ := (hΔ.symm henv).wf
  let ⟨ty₁, ih1⟩ := ih1 W hΔ hs.1
  let ⟨val₁, ih2⟩ := ih2 W hΔ hs.2.1
  have hvv := hv.uniq henv hΔ (ih2.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h1
  let ⟨_, h2⟩ := h1.isType henv hΔ₁.toCtx
  have htt := ht.uniq henv hΔ (ih1.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h2
  have ⟨_, ih3⟩ := ih3 (W.cons_bvar (.vlet ..)) (hΔ.cons nofun <| .vlet hvv htt) hs.2.2.fvars_cons
  have h1 := HasType.weakN_iff henv hΔ₂.toCtx W.toCtx
    |>.1 ((htt.defeqDF hvv).hasType.2.defeqDFC henv hΔ.defeqCtx)
  exact ⟨_, .letE h1 ih1 ih2 ih3⟩
| lit _ ih => let ⟨_, ih⟩ := ih W hΔ .toConstructor; exact ⟨_, .lit ih⟩
| mdata _ ih => let ⟨_, ih⟩ := ih W hΔ hs; exact ⟨_, .mdata ih⟩
| proj h1 h2 ih =>
  have hΔ₁ := hΔ.wf; have hΔ₂ := (hΔ.symm henv).wf
  let ⟨_, ih⟩ := ih W hΔ hs
  have htt := h1.uniq henv hΔ (ih.weakN henv W hΔ₂)
  have ⟨_, h2⟩ := h2.defeqDFC henv hΔ.defeqCtx htt
  have ⟨_, h2⟩ := h2.weakN_inv henv hΔ₂.toCtx W.toCtx
  exact ⟨_, .proj ih h2⟩
Proof state after:
no goals