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

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

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

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

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

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

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

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₂⟩
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 σ₁ σ₂

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