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

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

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
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✝ σ τ

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
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 σ τ

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⟩
State after:
no goals

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
State after:
no goals

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⟩
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 ∶ τ

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
State after:
no goals