internlm/Lean-Github huggingface dataset:
Theorem: Section19sheet2.lemma1
Proof state before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a
Tactic:
intro h
Proof state after:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a
Theorem: Section19sheet2.lemma1
Proof state before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a
Tactic:
exact IsIntegral.of_mem_of_fg _ h _ (Algebra.self_mem_adjoin_singleton R a)
Proof state after:
no goals
Theorem: QSqrt2.ext
Proof state before:
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
a b : QSqrt2
h1 : a.R = b.R
h2 : a.i = b.i
⊢ a = b
Tactic:
cases a
Proof state after:
case mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
b : QSqrt2
R✝ i✝ : ℚ
h1 : { R := R✝, i := i✝ }.R = b.R
h2 : { R := R✝, i := i✝ }.i = b.i
⊢ { R := R✝, i := i✝ } = b
Theorem: QSqrt2.ext
Proof state before:
case mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
b : QSqrt2
R✝ i✝ : ℚ
h1 : { R := R✝, i := i✝ }.R = b.R
h2 : { R := R✝, i := i✝ }.i = b.i
⊢ { R := R✝, i := i✝ } = b
Tactic:
cases b
Proof state after:
case mk.mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
R✝¹ i✝¹ R✝ i✝ : ℚ
h1 : { R := R✝¹, i := i✝¹ }.R = { R := R✝, i := i✝ }.R
h2 : { R := R✝¹, i := i✝¹ }.i = { R := R✝, i := i✝ }.i
⊢ { R := R✝¹, i := i✝¹ } = { R := R✝, i := i✝ }
Theorem: QSqrt2.ext
Proof state before:
case mk.mk
K : Type
inst✝¹ : Field K
inst✝ : NumberField K
R✝¹ i✝¹ R✝ i✝ : ℚ
h1 : { R := R✝¹, i := i✝¹ }.R = { R := R✝, i := i✝ }.R
h2 : { R := R✝¹, i := i✝¹ }.i = { R := R✝, i := i✝ }.i
⊢ { R := R✝¹, i := i✝¹ } = { R := R✝, i := i✝ }
Tactic:
simp_all
Proof state after:
no goals
Theorem: Section2sheet3solutions.tendsTo_def
Proof state before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Tactic:
rfl
Proof state after:
no goals
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
⊢ TendsTo (fun n => 37) 37
Tactic:
rw [tendsTo_def]
Proof state after:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
intro ε hε
Proof state after:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
use 100
Proof state after:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 100 ≤ n → |37 - 37| < ε
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 100 ≤ n → |37 - 37| < ε
Tactic:
intro n hn
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ |37 - 37| < ε
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ |37 - 37| < ε
Tactic:
norm_num
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ 0 < ε
Theorem: Section2sheet3solutions.tendsTo_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
hn : 100 ≤ n
⊢ 0 < ε
Tactic:
exact hε
Proof state after:
no goals
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
c : ℝ
⊢ TendsTo (fun n => c) c
Tactic:
intro ε hε
Proof state after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c) n - c| < ε
Tactic:
dsimp only
Proof state after:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
c ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |c - c| < ε
Tactic:
use 37
Proof state after:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
⊢ ∀ (n : ℕ), 37 ≤ n → |c - c| < ε
Tactic:
intro n hn
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |c - c| < ε
Tactic:
ring_nf
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ |0| < ε
Tactic:
norm_num
Proof state after:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε
Theorem: Section2sheet3solutions.tendsTo_const
Proof state before:
case h
c ε : ℝ
hε : ε > 0
n : ℕ
hn : 37 ≤ n
⊢ 0 < ε
Tactic:
exact hε
Proof state after:
no goals
Theorem: Section2sheet3solutions.tendsTo_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n + c) (t + c)
Tactic:
rw [tendsTo_def] at h ⊢
Proof state after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Theorem: Section2sheet3solutions.tendsTo_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + c - (t + c)| < ε
Tactic:
ring_nf
Proof state after:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Theorem: Section2sheet3solutions.tendsTo_add_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Tactic:
exact h
Proof state after:
no goals
Theorem: Section20sheet2.RepMap.comp_id
Proof state before:
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
⊢ comp φ (id ρ) = φ
Tactic:
sorry
Proof state after:
no goals
Theorem: Section20sheet2.RepMap.id_comp
Proof state before:
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
⊢ comp (id σ) φ = φ
Tactic:
sorry
Proof state after:
no goals
Theorem: Section20sheet2.RepMap.comp_assoc
Proof state before:
k : Type
inst✝⁹ : Field k
G : Type
inst✝⁸ : Group G
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
W : Type
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝³ : AddCommGroup X
inst✝² : Module k X
τ : Representation k G X
Y : Type
inst✝¹ : AddCommGroup Y
inst✝ : Module k Y
υ : Representation k G Y
ξ : RepMap τ υ
ψ : RepMap σ τ
φ : RepMap ρ σ
⊢ comp (comp ξ ψ) φ = comp ξ (comp ψ φ)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section15Sheet5.sixteen_pow_sixtyfour_mod_nineteen
Proof state before:
⊢ 16 ^ 64 = 16
Tactic:
rfl
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_const
Proof state before:
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.const c ∶ σ) ↔ σ = T c
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.const c ∶ σ) → σ = T c

case mpr
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
⊢ σ = T c → (Γ ⊢[T] LambdaTerm.const c ∶ σ)
Theorem: LambdaCalculi.hasType_const
Proof state before:
case mp
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.const c ∶ σ) → σ = T c
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.const c ∶ σ
⊢ σ = T c
Theorem: LambdaCalculi.hasType_const
Proof state before:
case mp
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.const c ∶ σ
⊢ σ = T c
Tactic:
cases h
Proof state after:
case mp.const
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
⊢ T c = T c
Theorem: LambdaCalculi.hasType_const
Proof state before:
case mp.const
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
⊢ T c = T c
Tactic:
rfl
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_const
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
σ : LambdaType p✝ U✝
⊢ σ = T c → (Γ ⊢[T] LambdaTerm.const c ∶ σ)
Tactic:
rintro rfl
Proof state after:
case mpr
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
⊢ Γ ⊢[T] LambdaTerm.const c ∶ T c
Theorem: LambdaCalculi.hasType_const
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.15403
C : Type ?u.15406
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
c : C✝
⊢ Γ ⊢[T] LambdaTerm.const c ∶ T c
Tactic:
exact .const
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_var
Proof state before:
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) ↔ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) → ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }

case mpr
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }) → (Γ ⊢[T] LambdaTerm.var n ∶ σ)
Theorem: LambdaCalculi.hasType_var
Proof state before:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.var n ∶ σ) → ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var n ∶ σ
⊢ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Theorem: LambdaCalculi.hasType_var
Proof state before:
case mp
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.var n ∶ σ
⊢ ∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }
Tactic:
cases h
Proof state after:
case mp.var
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h✝ : n < List.length Γ
⊢ ∃ (h : n < List.length Γ), List.get Γ { val := n, isLt := h✝ } = List.get Γ { val := n, isLt := h }
Theorem: LambdaCalculi.hasType_var
Proof state before:
case mp.var
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h✝ : n < List.length Γ
⊢ ∃ (h : n < List.length Γ), List.get Γ { val := n, isLt := h✝ } = List.get Γ { val := n, isLt := h }
Tactic:
exact ⟨_, rfl⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_var
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
σ : LambdaType p✝ U✝
⊢ (∃ (h : n < List.length Γ), σ = List.get Γ { val := n, isLt := h }) → (Γ ⊢[T] LambdaTerm.var n ∶ σ)
Tactic:
rintro ⟨h, rfl⟩
Proof state after:
case mpr.intro
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h : n < List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var n ∶ List.get Γ { val := n, isLt := h }
Theorem: LambdaCalculi.hasType_var
Proof state before:
case mpr.intro
p : LambdaParams
U : Type ?u.16248
C : Type ?u.16251
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
n : ℕ
h : n < List.length Γ
⊢ Γ ⊢[T] LambdaTerm.var n ∶ List.get Γ { val := n, isLt := h }
Tactic:
exact .var h
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_lambda
Proof 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
Proof 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 ∶ τ)
Theorem: LambdaCalculi.hasType_lambda
Proof 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
Proof 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 ∶ σ)
Theorem: LambdaCalculi.hasType_lambda
Proof 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
Proof 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 ∶ σ)
Theorem: LambdaCalculi.hasType_lambda
Proof 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⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_lambda
Proof 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
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_lambda
Proof 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⟩
Proof 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✝ ρ σ
Theorem: LambdaCalculi.hasType_lambda
Proof 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
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_app
Proof state before:
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.app h t u ∶ τ) ↔ ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Tactic:
constructor
Proof state after:
case mp
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.app h t u ∶ τ) → ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)

case mpr
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)) → (Γ ⊢[T] LambdaTerm.app h t u ∶ τ)
Theorem: LambdaCalculi.hasType_app
Proof state before:
case mp
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (Γ ⊢[T] LambdaTerm.app h t u ∶ τ) → ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Tactic:
intro h
Proof state after:
case mp
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.app h✝ t u ∶ τ
⊢ ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h✝ σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Theorem: LambdaCalculi.hasType_app
Proof state before:
case mp
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h✝ : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h : Γ ⊢[T] LambdaTerm.app h✝ t u ∶ τ
⊢ ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h✝ σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Tactic:
cases h
Proof state after:
case mp.app
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
τ✝ : LambdaType p✝ U✝
a✝¹ : Γ ⊢[T] u ∶ τ✝
a✝ : Γ ⊢[T] t ∶ LambdaType.lambda h✝ τ✝ τ
⊢ ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Theorem: LambdaCalculi.hasType_app
Proof state before:
case mp.app
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
τ✝ : LambdaType p✝ U✝
a✝¹ : Γ ⊢[T] u ∶ τ✝
a✝ : Γ ⊢[T] t ∶ LambdaType.lambda h✝ τ✝ τ
⊢ ∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)
Tactic:
exact ⟨_, by assumption, by assumption⟩
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_app
Proof state before:
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
τ✝ : LambdaType p✝ U✝
a✝¹ : Γ ⊢[T] u ∶ τ✝
a✝ : Γ ⊢[T] t ∶ LambdaType.lambda h✝ τ✝ τ
⊢ Γ ⊢[T] t ∶ LambdaType.lambda h ?m.19157 τ
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_app
Proof state before:
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
h✝ : p✝.lambda = true
τ✝ : LambdaType p✝ U✝
a✝¹ : Γ ⊢[T] u ∶ τ✝
a✝ : Γ ⊢[T] t ∶ LambdaType.lambda h✝ τ✝ τ
⊢ Γ ⊢[T] u ∶ τ✝
Tactic:
assumption
Proof state after:
no goals
Theorem: LambdaCalculi.hasType_app
Proof state before:
case mpr
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ : LambdaType p✝ U✝
⊢ (∃ σ, (Γ ⊢[T] t ∶ LambdaType.lambda h σ τ) ∧ (Γ ⊢[T] u ∶ σ)) → (Γ ⊢[T] LambdaTerm.app h t u ∶ τ)
Tactic:
rintro ⟨σ, h₁, h₂⟩
Proof state after:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ LambdaType.lambda h σ τ
h₂ : Γ ⊢[T] u ∶ σ
⊢ Γ ⊢[T] LambdaTerm.app h t u ∶ τ
Theorem: LambdaCalculi.hasType_app
Proof state before:
case mpr.intro.intro
p : LambdaParams
U : Type ?u.18239
C : Type ?u.18242
C✝ : Type u_1
p✝ : LambdaParams
U✝ : Type u_2
T : C✝ → LambdaType p✝ U✝
Γ : Context p✝ U✝
h : p✝.lambda = true
t u : LambdaTerm p✝ U✝ C✝
τ σ : LambdaType p✝ U✝
h₁ : Γ ⊢[T] t ∶ LambdaType.lambda h σ τ
h₂ : Γ ⊢[T] u ∶ σ
⊢ Γ ⊢[T] LambdaTerm.app h t u ∶ τ
Tactic:
exact .app h₁ h₂
Proof state after:
no goals