Theorem: Lean4Lean.IsFVarUpSet.congr (Lean4Lean/Verify/Typing/Lemmas.lean)

State before:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ IsFVarUpSet P ((some fv, d) :: Δ) ↔ IsFVarUpSet Q ((some fv, d) :: Δ)
Tactic:
refine and_congr (imp_congr (H _ (.head _)) ?_) (congr fun fv h => H _ (.tail _ h))
State after:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d ↔
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d

State before:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d ↔
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Tactic:
apply iff_of_eq
State after:
case a
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d =
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d

State before:
case a
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d =
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Tactic:
congr
State after:
case a.e_P
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) = fun i =>
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv

State before:
case a.e_P
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) = fun i =>
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
funext i
State after:
case a.e_P.h
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
i : Nat
⊢ (∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) =
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv

State before:
case a.e_P.h
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
i : Nat
⊢ (∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) =
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
refine forall_congr fun fv => propext ?_
State after:
case a.e_P.h
P Q : FVarId → Prop
fv✝ : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv : FVarId), fv ∈ VLCtx.fvars ((some fv✝, d) :: Δ) → (P fv ↔ Q fv)
i : Nat
fv : FVarId
⊢ VLCtx.vlamName Δ i = some (some fv) → P fv ↔ VLCtx.vlamName Δ i = some (some fv) → Q fv

State before:
case a.e_P.h
P Q : FVarId → Prop
fv✝ : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv : FVarId), fv ∈ VLCtx.fvars ((some fv✝, d) :: Δ) → (P fv ↔ Q fv)
i : Nat
fv : FVarId
⊢ VLCtx.vlamName Δ i = some (some fv) → P fv ↔ VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
exact imp_congr_right fun ha => H _ (.tail _ (VLCtx.vlamName_mem_fvars ha))
State after:
no goals