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

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

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

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

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

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

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

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