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

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

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

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

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

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

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

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

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₃⟩
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 ∶ σ

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