internlm/Lean-Github huggingface dataset:
Theorem: LambdaCalculi.hasType_case
Proof state before:
case mp
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.case h l r t ∶ σ) →
    ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case h✝ l r t ∶ σ
⊢ ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Theorem: LambdaCalculi.hasType_case
Proof state before:
case mp
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case h✝ l r t ∶ σ
⊢ ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Tactic:
cases h
Proof state after:
case mp.case
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
τ₁✝ τ₂✝ : LambdaType p✝ U✝
a✝² : Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁✝ τ₂✝
a✝¹ : τ₁✝ :: Γ ⊢[T] l ∶ σ
a✝ : τ₂✝ :: Γ ⊢[T] r ∶ σ
⊢ ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Theorem: LambdaCalculi.hasType_case
Proof state before:
case mp.case
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
τ₁✝ τ₂✝ : LambdaType p✝ U✝
a✝² : Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁✝ τ₂✝
a✝¹ : τ₁✝ :: Γ ⊢[T] l ∶ σ
a✝ : τ₂✝ :: Γ ⊢[T] r ∶ σ
⊢ ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Tactic:
refine ⟨_, _, by assumption, by assumption, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_case
Proof state before:
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
τ₁✝ τ₂✝ : LambdaType p✝ U✝
a✝² : Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁✝ τ₂✝
a✝¹ : τ₁✝ :: Γ ⊢[T] l ∶ σ
a✝ : τ₂✝ :: Γ ⊢[T] r ∶ σ
⊢ Γ ⊢[T] t ∶ LambdaType.coprod h ?m.25397 ?m.25410
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_case
Proof state before:
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
τ₁✝ τ₂✝ : LambdaType p✝ U✝
a✝² : Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁✝ τ₂✝
a✝¹ : τ₁✝ :: Γ ⊢[T] l ∶ σ
a✝ : τ₂✝ :: Γ ⊢[T] r ∶ σ
⊢ τ₁✝ :: Γ ⊢[T] l ∶ σ
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_case
Proof state before:
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
τ₁✝ τ₂✝ : LambdaType p✝ U✝
a✝² : Γ ⊢[T] t ∶ LambdaType.coprod h✝ τ₁✝ τ₂✝
a✝¹ : τ₁✝ :: Γ ⊢[T] l ∶ σ
a✝ : τ₂✝ :: Γ ⊢[T] r ∶ σ
⊢ τ₂✝ :: Γ ⊢[T] r ∶ σ
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_case
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)) →
    (Γ ⊢[T] LambdaTerm.case h l r t ∶ σ)
Tactic:
rintro ⟨τ₁, τ₂, h₁, h₂, h₃⟩
Proof state after:
case mpr.intro.intro.intro.intro
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ τ₁ τ₂ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂
h₂ : τ₁ :: Γ ⊢[T] l ∶ σ
h₃ : τ₂ :: Γ ⊢[T] r ∶ σ
⊢ Γ ⊢[T] LambdaTerm.case h l r t ∶ σ
Theorem: LambdaCalculi.hasType_case
Proof state before:
case mpr.intro.intro.intro.intro
p : LambdaParams
U : Type ?u.24401
C : Type ?u.24404
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
l r t : LambdaTerm p✝ U✝ C✝
σ τ₁ τ₂ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂
h₂ : τ₁ :: Γ ⊢[T] l ∶ σ
h₃ : τ₂ :: Γ ⊢[T] r ∶ σ
⊢ Γ ⊢[T] LambdaTerm.case h l r t ∶ σ
Tactic:
exact .case h₁ h₂ h₃
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_star
Proof state before:
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) ↔ σ = LambdaType.unit h
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) → σ = LambdaType.unit h

case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ σ = LambdaType.unit h → (Γ ⊢[T] LambdaTerm.star h ∶ σ)
Theorem: LambdaCalculi.hasType_star
Proof state before:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.star h ∶ σ) → σ = LambdaType.unit h
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.unit = true
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star h✝ ∶ σ
⊢ σ = LambdaType.unit h✝
Theorem: LambdaCalculi.hasType_star
Proof state before:
case mp
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.unit = true
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.star h✝ ∶ σ
⊢ σ = LambdaType.unit h✝
Tactic:
cases h
Proof state after:
case mp.star
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h h✝ : p✝.unit = true
⊢ LambdaType.unit h✝ = LambdaType.unit h
Theorem: LambdaCalculi.hasType_star
Proof state before:
case mp.star
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h h✝ : p✝.unit = true
⊢ LambdaType.unit h✝ = LambdaType.unit h
Tactic:
rfl
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_star
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
σ : LambdaType p✝ U✝
⊢ σ = LambdaType.unit h → (Γ ⊢[T] LambdaTerm.star h ∶ σ)
Tactic:
rintro rfl
Proof state after:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
⊢ Γ ⊢[T] LambdaTerm.star h ∶ LambdaType.unit h
Theorem: LambdaCalculi.hasType_star
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.25589
C : Type ?u.25592
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.unit = true
⊢ Γ ⊢[T] LambdaTerm.star h ∶ LambdaType.unit h
Tactic:
exact .star
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_elim
Proof state before:
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.elim h τ t ∶ σ) ↔ σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h)
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.elim h τ t ∶ σ) → σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h)

case mpr
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h) → (Γ ⊢[T] LambdaTerm.elim h τ t ∶ σ)
Theorem: LambdaCalculi.hasType_elim
Proof state before:
case mp
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.elim h τ t ∶ σ) → σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim h✝ τ t ∶ σ
⊢ σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h✝)
Theorem: LambdaCalculi.hasType_elim
Proof state before:
case mp
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim h✝ τ t ∶ σ
⊢ σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h✝)
Tactic:
cases h
Proof state after:
case mp.elim
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
h✝ : p✝.empty = true
a✝ : Γ ⊢[T] t ∶ LambdaType.empty h✝
⊢ τ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h)
Theorem: LambdaCalculi.hasType_elim
Proof state before:
case mp.elim
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
h✝ : p✝.empty = true
a✝ : Γ ⊢[T] t ∶ LambdaType.empty h✝
⊢ τ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h)
Tactic:
exact ⟨rfl, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_elim
Proof state before:
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
h✝ : p✝.empty = true
a✝ : Γ ⊢[T] t ∶ LambdaType.empty h✝
⊢ Γ ⊢[T] t ∶ LambdaType.empty h
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_elim
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.empty = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ σ = τ ∧ (Γ ⊢[T] t ∶ LambdaType.empty h) → (Γ ⊢[T] LambdaTerm.elim h τ t ∶ σ)
Tactic:
rintro ⟨rfl, h⟩
Proof state after:
case mpr.intro
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.empty = true
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.empty h✝
⊢ Γ ⊢[T] LambdaTerm.elim h✝ σ t ∶ σ
Theorem: LambdaCalculi.hasType_elim
Proof state before:
case mpr.intro
p : LambdaParams
U : Type ?u.26427
C : Type ?u.26430
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.empty = true
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.empty h✝
⊢ Γ ⊢[T] LambdaTerm.elim h✝ σ t ∶ σ
Tactic:
exact .elim h
Proof state after:
no goals
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
case lambda ih =>
  simp at h ⊢
  obtain ⟨σ, rfl, h⟩ := h
  exact ih h
Proof state after:
no goals
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
case case ih₁ ih₂ ih =>
  simp at h ⊢
  obtain ⟨τ₁, τ₂, h, h₁, h₂⟩ := h
  exact ⟨⟨ih₁ h₁, ih₂ h₂⟩, ih h⟩
Proof state after:
no goals
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.lambda a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
simp at h ⊢
Proof state after:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ σ, τ = LambdaType.lambda a✝² a✝¹ σ ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ)
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ σ, τ = LambdaType.lambda a✝² a✝¹ σ ∧ (a✝¹ :: Γ ⊢[T] a✝ ∶ σ)
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Tactic:
obtain ⟨σ, rfl, h⟩ := h
Proof state after:
case intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
case intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
σ : LambdaType p✝ U✝
h : a✝¹ :: Γ ⊢[T] a✝ ∶ σ
⊢ LambdaTerm.freeVarRange a✝ ≤ List.length Γ + 1
Tactic:
exact ih h
Proof state after:
no goals
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.case a✝³ a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
simp at h ⊢
Proof state after:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Tactic:
obtain ⟨τ₁, τ₂, h, h₁, h₂⟩ := h
Proof state after:
case intro.intro.intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ τ₁ τ₂ : LambdaType p✝ U✝
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
h₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
h₂ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
case intro.intro.intro.intro
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ τ) → LambdaTerm.freeVarRange a✝² ≤ List.length Γ
ih₂ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ τ) → LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ
ih : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ τ₁ τ₂ : LambdaType p✝ U✝
h : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
h₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
h₂ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ (LambdaTerm.freeVarRange a✝² ≤ List.length Γ + 1 ∧ LambdaTerm.freeVarRange a✝¹ ≤ List.length Γ + 1) ∧
    LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Tactic:
exact ⟨⟨ih₁ h₁, ih₂ h₂⟩, ih h⟩
Proof state after:
no goals
Theorem: LambdaCalculi.freeVarRange_le_length
Proof state before:
case elim
p : LambdaParams
U : Type ?u.27425
C : Type ?u.27428
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ : ∀ {Γ : Context p✝ U✝} {τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ τ) → LambdaTerm.freeVarRange a✝ ≤ List.length Γ
Γ : Context p✝ U✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ τ
⊢ LambdaTerm.freeVarRange (LambdaTerm.elim a✝² a✝¹ a✝) ≤ List.length Γ
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝² : p✝.lambda = true
a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ⊢[T] a✝¹ ∶ τ) → σ = τ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ⊢[T] a✝ ∶ τ) → σ = τ
Γ : Context p✝ U✝
σ τ : LambdaType p✝ U✝
hσ : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.app a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ
Tactic:
case app ih _ =>
  rw [hasType_app] at hσ hτ
  obtain ⟨_, h₁, -⟩ := hσ
  obtain ⟨_, h₂, -⟩ := hτ
  cases ih h₁ h₂
  rfl
Proof state after:
no goals
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝¹ : p✝.prod = true
a✝ : LambdaTerm p✝ U✝ C✝
ih : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ⊢[T] a✝ ∶ τ) → σ = τ
Γ : Context p✝ U✝
σ τ : LambdaType p✝ U✝
hσ : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.snd a✝¹ a✝ ∶ τ
⊢ σ = τ
Tactic:
case fst ih | snd ih =>
  simp only [hasType_fst, hasType_snd] at hσ hτ
  obtain ⟨σ', hσ⟩ := hσ
  obtain ⟨τ', hτ⟩ := hτ
  cases ih hσ hτ
  rfl
Proof state after:
no goals
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
p : LambdaParams
U : Type ?u.145218
C : Type ?u.145221
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
a✝³ : p✝.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p✝ U✝ C✝
ih₁ : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ⊢[T] a✝² ∶ τ) → σ = τ
a_ih✝ : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝¹ ∶ σ) → (Γ ⊢[T] a✝¹ ∶ τ) → σ = τ
ih : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ⊢[T] a✝ ∶ τ) → σ = τ
Γ : Context p✝ U✝
σ τ : LambdaType p✝ U✝
hσ : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ
Tactic:
case case ih₁ _ ih =>
  rw [hasType_case] at hσ hτ
  obtain ⟨σ₁, σ₂, hσ, hσ₁, _⟩ := hσ
  obtain ⟨τ₁, τ₂, hτ, hτ₁, _⟩ := hτ
  cases ih hσ hτ
  cases ih₁ hσ₁ hτ₁
  rfl
Proof state after:
no goals