internlm/Lean-Github huggingface dataset:
Theorem: LambdaCalculi.hasType_pair
Proof state before:
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.pair h t u ∶ τ) ↔ ∃ σ₁ σ₂, τ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.pair h t u ∶ τ) → ∃ σ₁ σ₂, τ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)

case mpr
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ₁ σ₂, τ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)) → (Γ ⊢[T] LambdaTerm.pair h t u ∶ τ)
Theorem: LambdaCalculi.hasType_pair
Proof state before:
case mp
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.pair h t u ∶ τ) → ∃ σ₁ σ₂, τ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.pair h✝ t u ∶ τ
⊢ ∃ σ₁ σ₂, τ = LambdaType.prod h✝ σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Theorem: LambdaCalculi.hasType_pair
Proof state before:
case mp
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.pair h✝ t u ∶ τ
⊢ ∃ σ₁ σ₂, τ = LambdaType.prod h✝ σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Tactic:
cases h
Proof state after:
case mp.pair
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ✝ τ✝ : LambdaType p✝ U✝
h✝ : p✝.prod = true
a✝¹ : Γ ⊢[T] t ∶ σ✝
a✝ : Γ ⊢[T] u ∶ τ✝
⊢ ∃ σ₁ σ₂, LambdaType.prod h✝ σ✝ τ✝ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Theorem: LambdaCalculi.hasType_pair
Proof state before:
case mp.pair
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ✝ τ✝ : LambdaType p✝ U✝
h✝ : p✝.prod = true
a✝¹ : Γ ⊢[T] t ∶ σ✝
a✝ : Γ ⊢[T] u ∶ τ✝
⊢ ∃ σ₁ σ₂, LambdaType.prod h✝ σ✝ τ✝ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)
Tactic:
exact ⟨_, _, rfl, by assumption, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_pair
Proof state before:
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ✝ τ✝ : LambdaType p✝ U✝
h✝ : p✝.prod = true
a✝¹ : Γ ⊢[T] t ∶ σ✝
a✝ : Γ ⊢[T] u ∶ τ✝
⊢ Γ ⊢[T] t ∶ σ✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_pair
Proof state before:
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ✝ τ✝ : LambdaType p✝ U✝
h✝ : p✝.prod = true
a✝¹ : Γ ⊢[T] t ∶ σ✝
a✝ : Γ ⊢[T] u ∶ τ✝
⊢ Γ ⊢[T] u ∶ τ✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_pair
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ₁ σ₂, τ = LambdaType.prod h σ₁ σ₂ ∧ (Γ ⊢[T] t ∶ σ₁) ∧ (Γ ⊢[T] u ∶ σ₂)) → (Γ ⊢[T] LambdaTerm.pair h t u ∶ τ)
Tactic:
rintro ⟨σ₁, σ₂, rfl, h₁, h₂⟩
Proof state after:
case mpr.intro.intro.intro.intro
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ₁ σ₂ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ σ₁
h₂ : Γ ⊢[T] u ∶ σ₂
⊢ Γ ⊢[T] LambdaTerm.pair h t u ∶ LambdaType.prod h σ₁ σ₂
Theorem: LambdaCalculi.hasType_pair
Proof state before:
case mpr.intro.intro.intro.intro
p : LambdaParams
U : Type ?u.19287
C : Type ?u.19290
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t u : LambdaTerm p✝ U✝ C✝
σ₁ σ₂ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ σ₁
h₂ : Γ ⊢[T] u ∶ σ₂
⊢ Γ ⊢[T] LambdaTerm.pair h t u ∶ LambdaType.prod h σ₁ σ₂
Tactic:
exact .pair h₁ h₂
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_fst
Proof state before:
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.fst h t ∶ τ) ↔ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.fst h t ∶ τ) → ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ

case mpr
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ) → (Γ ⊢[T] LambdaTerm.fst h t ∶ τ)
Theorem: LambdaCalculi.hasType_fst
Proof state before:
case mp
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.fst h t ∶ τ) → ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.fst h✝ t ∶ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h✝ τ σ
Theorem: LambdaCalculi.hasType_fst
Proof state before:
case mp
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.fst h✝ t ∶ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h✝ τ σ
Tactic:
cases h
Proof state after:
case mp.fst
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
τ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ τ τ✝
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ
Theorem: LambdaCalculi.hasType_fst
Proof state before:
case mp.fst
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
τ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ τ τ✝
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ
Tactic:
exact ⟨_, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_fst
Proof state before:
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
τ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ τ τ✝
⊢ Γ ⊢[T] t ∶ LambdaType.prod h τ ?m.21262
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_fst
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h τ σ) → (Γ ⊢[T] LambdaTerm.fst h t ∶ τ)
Tactic:
rintro ⟨σ, h⟩
Proof state after:
case mpr.intro
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.prod h✝ τ σ
⊢ Γ ⊢[T] LambdaTerm.fst h✝ t ∶ τ
Theorem: LambdaCalculi.hasType_fst
Proof state before:
case mpr.intro
p : LambdaParams
U : Type ?u.20413
C : Type ?u.20416
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.prod h✝ τ σ
⊢ Γ ⊢[T] LambdaTerm.fst h✝ t ∶ τ
Tactic:
exact .fst h
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_snd
Proof state before:
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.snd h t ∶ τ) ↔ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.snd h t ∶ τ) → ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ

case mpr
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ) → (Γ ⊢[T] LambdaTerm.snd h t ∶ τ)
Theorem: LambdaCalculi.hasType_snd
Proof state before:
case mp
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.snd h t ∶ τ) → ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.snd h✝ t ∶ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h✝ σ τ
Theorem: LambdaCalculi.hasType_snd
Proof state before:
case mp
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.snd h✝ t ∶ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h✝ σ τ
Tactic:
cases h
Proof state after:
case mp.snd
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
σ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ σ✝ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ
Theorem: LambdaCalculi.hasType_snd
Proof state before:
case mp.snd
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
σ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ σ✝ τ
⊢ ∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ
Tactic:
exact ⟨_, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_snd
Proof state before:
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.prod = true
σ✝ : LambdaType p✝ U✝
a✝ : Γ ⊢[T] t ∶ LambdaType.prod h✝ σ✝ τ
⊢ Γ ⊢[T] t ∶ LambdaType.prod h ?m.22205 τ
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_snd
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, Γ ⊢[T] t ∶ LambdaType.prod h σ τ) → (Γ ⊢[T] LambdaTerm.snd h t ∶ τ)
Tactic:
rintro ⟨σ, h⟩
Proof state after:
case mpr.intro
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.prod h✝ σ τ
⊢ Γ ⊢[T] LambdaTerm.snd h✝ t ∶ τ
Theorem: LambdaCalculi.hasType_snd
Proof state before:
case mpr.intro
p : LambdaParams
U : Type ?u.21356
C : Type ?u.21359
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.prod = true
t : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ LambdaType.prod h✝ σ τ
⊢ Γ ⊢[T] LambdaTerm.snd h✝ t ∶ τ
Tactic:
exact .snd h
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inl
Proof state before:
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inl h τ t ∶ σ) ↔ ∃ ρ, σ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inl h τ t ∶ σ) → ∃ ρ, σ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)

case mpr
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (∃ ρ, σ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)) → (Γ ⊢[T] LambdaTerm.inl h τ t ∶ σ)
Theorem: LambdaCalculi.hasType_inl
Proof state before:
case mp
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inl h τ t ∶ σ) → ∃ ρ, σ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inl h✝ τ t ∶ σ
⊢ ∃ ρ, σ = LambdaType.coprod h✝ ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Theorem: LambdaCalculi.hasType_inl
Proof state before:
case mp
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inl h✝ τ t ∶ σ
⊢ ∃ ρ, σ = LambdaType.coprod h✝ ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
cases h
Proof state after:
case mp.inl
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ σ✝
⊢ ∃ ρ, LambdaType.coprod h✝ σ✝ τ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Theorem: LambdaCalculi.hasType_inl
Proof state before:
case mp.inl
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ σ✝
⊢ ∃ ρ, LambdaType.coprod h✝ σ✝ τ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
exact ⟨_, rfl, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inl
Proof state before:
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ σ✝
⊢ Γ ⊢[T] t ∶ σ✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inl
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (∃ ρ, σ = LambdaType.coprod h ρ τ ∧ (Γ ⊢[T] t ∶ ρ)) → (Γ ⊢[T] LambdaTerm.inl h τ t ∶ σ)
Tactic:
rintro ⟨σ, rfl, h⟩
Proof state after:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.inl h✝ τ t ∶ LambdaType.coprod h✝ σ τ
Theorem: LambdaCalculi.hasType_inl
Proof state before:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.22299
C : Type ?u.22302
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.inl h✝ τ t ∶ LambdaType.coprod h✝ σ τ
Tactic:
exact .inl h
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inr
Proof state before:
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inr h τ t ∶ σ) ↔ ∃ ρ, σ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inr h τ t ∶ σ) → ∃ ρ, σ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)

case mpr
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (∃ ρ, σ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)) → (Γ ⊢[T] LambdaTerm.inr h τ t ∶ σ)
Theorem: LambdaCalculi.hasType_inr
Proof state before:
case mp
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.inr h τ t ∶ σ) → ∃ ρ, σ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inr h✝ τ t ∶ σ
⊢ ∃ ρ, σ = LambdaType.coprod h✝ τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Theorem: LambdaCalculi.hasType_inr
Proof state before:
case mp
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.inr h✝ τ t ∶ σ
⊢ ∃ ρ, σ = LambdaType.coprod h✝ τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
cases h
Proof state after:
case mp.inr
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ τ✝
⊢ ∃ ρ, LambdaType.coprod h✝ τ τ✝ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Theorem: LambdaCalculi.hasType_inr
Proof state before:
case mp.inr
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ τ✝
⊢ ∃ ρ, LambdaType.coprod h✝ τ τ✝ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)
Tactic:
refine ⟨_, rfl, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inr
Proof state before:
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ✝ : LambdaType p✝ U✝
h✝ : p✝.coprod = true
a✝ : Γ ⊢[T] t ∶ τ✝
⊢ Γ ⊢[T] t ∶ τ✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_inr
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
⊢ (∃ ρ, σ = LambdaType.coprod h τ ρ ∧ (Γ ⊢[T] t ∶ ρ)) → (Γ ⊢[T] LambdaTerm.inr h τ t ∶ σ)
Tactic:
rintro ⟨σ, rfl, h⟩
Proof state after:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.inr h✝ τ t ∶ LambdaType.coprod h✝ τ σ
Theorem: LambdaCalculi.hasType_inr
Proof state before:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.23350
C : Type ?u.23353
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.coprod = true
τ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.inr h✝ τ t ∶ LambdaType.coprod h✝ τ σ
Tactic:
exact .inr h
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✝
⊢ (Γ ⊢[T] LambdaTerm.case h l r t ∶ σ) ↔
    ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)
Tactic:
constructor
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✝
⊢ (Γ ⊢[T] LambdaTerm.case h l r t ∶ σ) →
    ∃ τ₁ τ₂, (Γ ⊢[T] t ∶ LambdaType.coprod h τ₁ τ₂) ∧ (τ₁ :: Γ ⊢[T] l ∶ σ) ∧ (τ₂ :: Γ ⊢[T] r ∶ σ)

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 ∶ σ)