Theorem: LambdaCalculi.hasType_lambda (LambdaCalculi/HasType.lean)

State before:
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.lambda h ρ t ∶ τ) ↔ ∃ σ, τ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)
Tactic:
constructor
State after:
case mp
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.lambda h ρ t ∶ τ) → ∃ σ, τ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)

case mpr
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, τ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)) → (Γ ⊢[T] LambdaTerm.lambda h ρ t ∶ τ)

State before:
case mp
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.lambda h ρ t ∶ τ) → ∃ σ, τ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)
Tactic:
intro h
State after:
case mp
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda h✝ ρ t ∶ τ
⊢ ∃ σ, τ = LambdaType.lambda h✝ ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)

State before:
case mp
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.lambda h✝ ρ t ∶ τ
⊢ ∃ σ, τ = LambdaType.lambda h✝ ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)
Tactic:
cases h
State after:
case mp.lambda
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
a✝ : ρ :: Γ ⊢[T] t ∶ σ✝
⊢ ∃ σ, LambdaType.lambda h✝ ρ σ✝ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)

State before:
case mp.lambda
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
a✝ : ρ :: Γ ⊢[T] t ∶ σ✝
⊢ ∃ σ, LambdaType.lambda h✝ ρ σ✝ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)
Tactic:
exact ⟨_, rfl, by assumption⟩
State after:
no goals

State before:
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ✝ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
a✝ : ρ :: Γ ⊢[T] t ∶ σ✝
⊢ ρ :: Γ ⊢[T] t ∶ σ✝
Tactic:
assumption
State after:
no goals

State before:
case mpr
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, τ = LambdaType.lambda h ρ σ ∧ (ρ :: Γ ⊢[T] t ∶ σ)) → (Γ ⊢[T] LambdaTerm.lambda h ρ t ∶ τ)
Tactic:
rintro ⟨σ, rfl, h⟩
State after:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : ρ :: Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.lambda h✝ ρ t ∶ LambdaType.lambda h✝ ρ σ

State before:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.17183
C : Type ?u.17186
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
ρ : LambdaType p✝ U✝
t : LambdaTerm p✝ U✝ C✝
σ : LambdaType p✝ U✝
h : ρ :: Γ ⊢[T] t ∶ σ
⊢ Γ ⊢[T] LambdaTerm.lambda h✝ ρ t ∶ LambdaType.lambda h✝ ρ σ
Tactic:
exact .lambda h
State after:
no goals