internlm/Lean-Github huggingface dataset:
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:
rw [hasType_app] at hσ hτ
Proof state after:
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σ : ∃ σ_1, (Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² σ_1 σ) ∧ (Γ ⊢[T] a✝ ∶ σ_1)
hτ : ∃ σ, (Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² σ τ) ∧ (Γ ⊢[T] a✝ ∶ σ)
⊢ σ = τ
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σ : ∃ σ_1, (Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² σ_1 σ) ∧ (Γ ⊢[T] a✝ ∶ σ_1)
hτ : ∃ σ, (Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² σ τ) ∧ (Γ ⊢[T] a✝ ∶ σ)
⊢ σ = τ
Tactic:
obtain ⟨_, h₁, -⟩ := hσ
Proof state after:
case intro.intro
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] a✝¹ ∶ LambdaType.lambda a✝² σ τ) ∧ (Γ ⊢[T] a✝ ∶ σ)
w✝ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ σ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro
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] a✝¹ ∶ LambdaType.lambda a✝² σ τ) ∧ (Γ ⊢[T] a✝ ∶ σ)
w✝ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ σ
⊢ σ = τ
Tactic:
obtain ⟨_, h₂, -⟩ := hτ
Proof state after:
case intro.intro.intro.intro
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✝
σ τ w✝¹ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝¹ σ
w✝ : LambdaType p✝ U✝
h₂ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ τ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro
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✝
σ τ w✝¹ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝¹ σ
w✝ : LambdaType p✝ U✝
h₂ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ τ
⊢ σ = τ
Tactic:
cases ih h₁ h₂
Proof state after:
case intro.intro.intro.intro.refl
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✝
σ w✝ : LambdaType p✝ U✝
h₁ h₂ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ σ
⊢ σ = σ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro.refl
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✝
σ w✝ : LambdaType p✝ U✝
h₁ h₂ : Γ ⊢[T] a✝¹ ∶ LambdaType.lambda a✝² w✝ σ
⊢ σ = σ
Tactic:
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:
simp only [hasType_fst, hasType_snd] at hσ hτ
Proof state after:
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σ : ∃ σ_1, Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ_1 σ
hτ : ∃ σ, Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ τ
⊢ σ = τ
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σ : ∃ σ_1, Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ_1 σ
hτ : ∃ σ, Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ τ
⊢ σ = τ
Tactic:
obtain ⟨σ', hσ⟩ := hσ
Proof state after:
case intro
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] a✝ ∶ LambdaType.prod a✝¹ σ τ
σ' : LambdaType p✝ U✝
hσ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ' σ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro
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] a✝ ∶ LambdaType.prod a✝¹ σ τ
σ' : LambdaType p✝ U✝
hσ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ' σ
⊢ σ = τ
Tactic:
obtain ⟨τ', hτ⟩ := hτ
Proof state after:
case intro.intro
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] a✝ ∶ LambdaType.prod a✝¹ σ' σ
τ' : LambdaType p✝ U✝
hτ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ τ' τ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro
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] a✝ ∶ LambdaType.prod a✝¹ σ' σ
τ' : LambdaType p✝ U✝
hτ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ τ' τ
⊢ σ = τ
Tactic:
cases ih hσ hτ
Proof state after:
case intro.intro.refl
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σ hτ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ' σ
⊢ σ = σ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.refl
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σ hτ : Γ ⊢[T] a✝ ∶ LambdaType.prod a✝¹ σ' σ
⊢ σ = σ
Tactic:
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:
rw [hasType_case] at hσ hτ
Proof state after:
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] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ σ)
hτ : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ σ = τ
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] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ σ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ σ)
hτ : ∃ τ₁ τ₂, (Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
⊢ σ = τ
Tactic:
obtain ⟨σ₁, σ₂, hσ, hσ₁, _⟩ := hσ
Proof state after:
case intro.intro.intro.intro
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] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
σ₁ σ₂ : LambdaType p✝ U✝
hσ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro
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] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] a✝² ∶ τ) ∧ (τ₂ :: Γ ⊢[T] a✝¹ ∶ τ)
σ₁ σ₂ : LambdaType p✝ U✝
hσ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ σ = τ
Tactic:
obtain ⟨τ₁, τ₂, hτ, hτ₁, _⟩ := hτ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
τ₁ τ₂ : LambdaType p✝ U✝
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
hτ₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
right✝ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
τ₁ τ₂ : LambdaType p✝ U✝
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ τ₁ τ₂
hτ₁ : τ₁ :: Γ ⊢[T] a✝² ∶ τ
right✝ : τ₂ :: Γ ⊢[T] a✝¹ ∶ τ
⊢ σ = τ
Tactic:
cases ih hσ hτ
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.refl
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
hτ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ τ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ τ
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
⊢ σ = τ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.refl
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
hτ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ τ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ τ
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
⊢ σ = τ
Tactic:
cases ih₁ hσ₁ hτ₁
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hτ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ σ = σ
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.refl.refl
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] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hσ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝¹ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
hτ : Γ ⊢[T] a✝ ∶ LambdaType.coprod a✝³ σ₁ σ₂
hτ₁ : σ₁ :: Γ ⊢[T] a✝² ∶ σ
right✝ : σ₂ :: Γ ⊢[T] a✝¹ ∶ σ
⊢ σ = σ
Tactic:
rfl
Proof state after:
no goals
Theorem: LambdaCalculi.eq_of_hasType
Proof state before:
case elim
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✝.empty = true
a✝¹ : LambdaType p✝ U✝
a✝ : LambdaTerm p✝ U✝ C✝
a_ih✝ : ∀ {Γ : Context p✝ U✝} {σ τ : LambdaType p✝ U✝}, (Γ ⊢[T] a✝ ∶ σ) → (Γ ⊢[T] a✝ ∶ τ) → σ = τ
Γ : Context p✝ U✝
σ τ : LambdaType p✝ U✝
hσ : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ σ
hτ : Γ ⊢[T] LambdaTerm.elim a✝² a✝¹ a✝ ∶ τ
⊢ σ = τ
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
case var =>
  simp only [hasType_var, List.length_append] at h ⊢
  obtain ⟨h, rfl⟩ := h
  refine ⟨Nat.lt_add_right _ _ _ h, ?_⟩
  rw [List.get_append]
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝² : p.lambda = true
a✝¹ : LambdaType p U
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.lambda a✝² a✝¹ a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.lambda a✝² a✝¹ a✝ ∶ σ
Tactic:
case lambda ih =>
  simp only [hasType_lambda] at h ⊢
  obtain ⟨σ, rfl, h⟩ := h
  exact ⟨σ, rfl, ih h⟩
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C✝
ih₁ : ∀ {Γ : Context p U} {σ : LambdaType p U}, (Γ ⊢[T] a✝² ∶ σ) → (Γ ++ Δ ⊢[T] 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✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.case a✝³ a✝² a✝¹ a✝ ∶ σ
Tactic:
case case ih₁ ih₂ ih =>
  simp only [hasType_case] at h ⊢
  obtain ⟨σ₁, σ₂, h, h₁, h₂⟩ := h
  exact ⟨σ₁, σ₂, ih h, ih₁ h₁, ih₂ h₂⟩
Proof state after:
no goals
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
σ : LambdaType p U
h : Γ ⊢[T] LambdaTerm.var a✝ ∶ σ
⊢ Γ ++ Δ ⊢[T] LambdaTerm.var a✝ ∶ σ
Tactic:
simp only [hasType_var, List.length_append] at h ⊢
Proof state after:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
σ : LambdaType p U
h : ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }
⊢ ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Theorem: LambdaCalculi.append_hasType
Proof state before:
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
σ : LambdaType p U
h : ∃ (h : a✝ < List.length Γ), σ = List.get Γ { val := a✝, isLt := h }
⊢ ∃ (h : a✝ < List.length Γ + List.length Δ),
    σ = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Tactic:
obtain ⟨h, rfl⟩ := h
Proof state after:
case intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
h : a✝ < List.length Γ
⊢ ∃ (h_1 : a✝ < List.length Γ + List.length Δ),
    List.get Γ { val := a✝, isLt := h } = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Theorem: LambdaCalculi.append_hasType
Proof state before:
case intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
h : a✝ < List.length Γ
⊢ ∃ (h_1 : a✝ < List.length Γ + List.length Δ),
    List.get Γ { val := a✝, isLt := h } = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Tactic:
refine ⟨Nat.lt_add_right _ _ _ h, ?_⟩
Proof state after:
case intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
h : a✝ < List.length Γ
⊢ List.get Γ { val := a✝, isLt := h } = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Theorem: LambdaCalculi.append_hasType
Proof state before:
case intro
p : LambdaParams
U : Type u_2
C : Type ?u.350830
C✝ : Type u_1
T : C✝ → LambdaType p U
Δ : Context p U
a✝ : ℕ
Γ : Context p U
h : a✝ < List.length Γ
⊢ List.get Γ { val := a✝, isLt := h } = List.get (Γ ++ Δ) { val := a✝, isLt := (_ : a✝ < List.length (Γ ++ Δ)) }
Tactic:
rw [List.get_append]
Proof state after:
no goals