Theorem: Lean4Lean.VEnv.IsDefEqStrong.mono (Lean4Lean/Theory/Typing/Strong.lean)

State before:
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
H : IsDefEqStrong env U Γ e1 e2 A
⊢ IsDefEqStrong env' U Γ e1 e2 A
Tactic:
induction H with
| bvar h1 h2 _ ih => exact .bvar h1 h2 ih
| symm _ ih => exact .symm ih
| trans _ _ ih1 ih2 => exact .trans ih1 ih2
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| constDF h1 h2 h3 h4 h5 h6 _ _ _ _ ih1 ih2 ih3 ih4 =>
  exact .constDF (henv.1 _ _ h1) h2 h3 h4 h5 h6 ih1 ih2 ih3 ih4
| appDF h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 => exact .appDF h1 h2 ih1 ih2 ih3 ih4 ih5
| lamDF h1 h2  _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 => exact .lamDF h1 h2 ih1 ih2 ih3 ih4 ih5
| forallEDF h1 h2 _ _ _ ih1 ih2 ih3 => exact .forallEDF h1 h2 ih1 ih2 ih3
| defeqDF h1 _ _ ih1 ih2 => exact .defeqDF h1 ih1 ih2
| beta h1 h2 _ _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 ih6 => exact .beta h1 h2 ih1 ih2 ih3 ih4 ih5 ih6
| eta h1 h2 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 => exact .eta h1 h2 ih1 ih2 ih3 ih4 ih5
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel ih1 ih2 ih3
| extra h1 h2 h3 h4 _ _ _ _ _ ih1 ih2 ih3 ih4 ih5 =>
  exact .extra (henv.2 _ h1) h2 h3 h4 ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case bvar
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h1 : Lookup Γ✝ i✝ A✝
h2 : VLevel.WF U u✝
a✝ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
ih : IsDefEqStrong env' U Γ✝ A✝ A✝ (sort u✝)
⊢ IsDefEqStrong env' U Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝) A✝
Tactic:
exact .bvar h1 h2 ih
State after:
no goals

State before:
case symm
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : IsDefEqStrong env' U Γ✝ e✝ e'✝ A✝
⊢ IsDefEqStrong env' U Γ✝ e'✝ e✝ A✝
Tactic:
exact .symm ih
State after:
no goals

State before:
case trans
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
ih1 : IsDefEqStrong env' U Γ✝ e₁✝ e₂✝ A✝
ih2 : IsDefEqStrong env' U Γ✝ e₂✝ e₃✝ A✝
⊢ IsDefEqStrong env' U Γ✝ e₁✝ e₃✝ A✝
Tactic:
exact .trans ih1 ih2
State after:
no goals

State before:
case sortDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
⊢ IsDefEqStrong env' U Γ✝ (sort l✝) (sort l'✝) (sort (VLevel.succ l✝))
Tactic:
exact .sortDF h1 h2 h3
State after:
no goals

State before:
case constDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
h6 : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
ih1 : IsDefEqStrong env' U [] (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
ih2 : IsDefEqStrong env' U [] (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
ih3 : IsDefEqStrong env' U Γ✝ (instL ls✝ ci✝.type) (instL ls✝ ci✝.type) (sort u✝)
ih4 : IsDefEqStrong env' U Γ✝ (instL ls'✝ ci✝.type) (instL ls'✝ ci✝.type) (sort u✝)
⊢ IsDefEqStrong env' U Γ✝ (const c✝ ls✝) (const c✝ ls'✝) (instL ls✝ ci✝.type)
Tactic:
exact .constDF (henv.1 _ _ h1) h2 h3 h4 h5 h6 ih1 ih2 ih3 ih4
State after:
no goals

State before:
case appDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁵ a'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁵ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁵) (inst B✝ a'✝) (sort v✝)
ih1 : IsDefEqStrong env' U Γ✝ A✝ A✝ (sort u✝)
ih2 : IsDefEqStrong env' U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
ih3 : IsDefEqStrong env' U Γ✝ f✝ f'✝ (forallE A✝ B✝)
ih4 : IsDefEqStrong env' U Γ✝ a✝⁵ a'✝ A✝
ih5 : IsDefEqStrong env' U Γ✝ (inst B✝ a✝⁵) (inst B✝ a'✝) (sort v✝)
⊢ IsDefEqStrong env' U Γ✝ (app f✝ a✝⁵) (app f'✝ a'✝) (inst B✝ a✝⁵)
Tactic:
exact .appDF h1 h2 ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case lamDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ih1 : IsDefEqStrong env' U Γ✝ A✝ A'✝ (sort u✝)
ih2 : IsDefEqStrong env' U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
ih3 : IsDefEqStrong env' U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
ih4 : IsDefEqStrong env' U (A✝ :: Γ✝) body✝ body'✝ B✝
ih5 : IsDefEqStrong env' U (A'✝ :: Γ✝) body✝ body'✝ B✝
⊢ IsDefEqStrong env' U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (forallE A✝ B✝)
Tactic:
exact .lamDF h1 h2 ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case forallEDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
ih1 : IsDefEqStrong env' U Γ✝ A✝ A'✝ (sort u✝)
ih2 : IsDefEqStrong env' U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
ih3 : IsDefEqStrong env' U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
⊢ IsDefEqStrong env' U Γ✝ (forallE A✝ body✝) (forallE A'✝ body'✝) (sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallEDF h1 h2 ih1 ih2 ih3
State after:
no goals

State before:
case defeqDF
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
h1 : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
ih1 : IsDefEqStrong env' U Γ✝ A✝ B✝ (sort u✝)
ih2 : IsDefEqStrong env' U Γ✝ e1✝ e2✝ A✝
⊢ IsDefEqStrong env' U Γ✝ e1✝ e2✝ B✝
Tactic:
exact .defeqDF h1 ih1 ih2
State after:
no goals

State before:
case beta
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 : IsDefEqStrong env' U Γ✝ A✝ A✝ (sort u✝)
ih2 : IsDefEqStrong env' U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
ih3 : IsDefEqStrong env' U (A✝ :: Γ✝) e✝ e✝ B✝
ih4 : IsDefEqStrong env' U Γ✝ e'✝ e'✝ A✝
ih5 : IsDefEqStrong env' U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
ih6 : IsDefEqStrong env' U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
⊢ IsDefEqStrong env' U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
exact .beta h1 h2 ih1 ih2 ih3 ih4 ih5 ih6
State after:
no goals

State before:
case eta
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 : IsDefEqStrong env' U Γ✝ A✝ A✝ (sort u✝)
ih2 : IsDefEqStrong env' U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
ih3 : IsDefEqStrong env' U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
ih4 : IsDefEqStrong env' U Γ✝ e✝ e✝ (forallE A✝ B✝)
ih5 : IsDefEqStrong env' U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
⊢ IsDefEqStrong env' U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (forallE A✝ B✝)
Tactic:
exact .eta h1 h2 ih1 ih2 ih3 ih4 ih5
State after:
no goals

State before:
case proofIrrel
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 : IsDefEqStrong env' U Γ✝ p✝ p✝ (sort VLevel.zero)
ih2 : IsDefEqStrong env' U Γ✝ h✝ h✝ p✝
ih3 : IsDefEqStrong env' U Γ✝ h'✝ h'✝ p✝
⊢ IsDefEqStrong env' U Γ✝ h✝ h'✝ p✝
Tactic:
exact .proofIrrel ih1 ih2 ih3
State after:
no goals

State before:
case extra
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝² : IsDefEqStrong env U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
ih1 : IsDefEqStrong env' U [] (instL ls✝ df✝.type) (instL ls✝ df✝.type) (sort u✝)
ih2 : IsDefEqStrong env' U [] (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
ih3 : IsDefEqStrong env' U [] (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
ih4 : IsDefEqStrong env' U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.lhs) (instL ls✝ df✝.type)
ih5 : IsDefEqStrong env' U Γ✝ (instL ls✝ df✝.rhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
⊢ IsDefEqStrong env' U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Tactic:
exact .extra (henv.2 _ h1) h2 h3 h4 ih1 ih2 ih3 ih4 ih5
State after:
no goals