internlm/Lean-Github huggingface dataset:
Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => some (if m = n then t else if m < n then var m else var (m - 1))
      | x => none with
    | some u => u
    | none => var m) =
    var m
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.instantiate'_eq_of_freeVarRange_le
Proof state before:
case elim
p : LambdaParams
U : Type u_1
C : Type u_2
t : LambdaTerm p U C
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' (instantiateFun t) n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' (instantiateFun t) n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝
Tactic:
aesop
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m + 1 ≤ n
⊢ replace' liftFun n (var m) = var m
Tactic:
case var m =>
  rw [Nat.add_one_le_iff] at h
  rw [replace'_var, liftFun]
  simp only
  rw [if_neg]
  rw [not_le]
  exact h
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
case const
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : C
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (const a✝) = const a✝

case lambda
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ - 1 ≤ n
⊢ replace' liftFun n (lambda a✝² a✝¹ a✝) = lambda a✝² a✝¹ a✝

case app
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.lambda = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (app a✝² a✝¹ a✝) = app a✝² a✝¹ a✝

case pair
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.prod = true
a✝¹ a✝ : LambdaTerm p U C
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (freeVarRange a✝¹) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (pair a✝² a✝¹ a✝) = pair a✝² a✝¹ a✝

case fst
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (fst a✝¹ a✝) = fst a✝¹ a✝

case snd
p : LambdaParams
U : Type u_1
C : Type u_2
a✝¹ : p.prod = true
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (snd a✝¹ a✝) = snd a✝¹ a✝

case inl
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inl a✝² a✝¹ a✝) = inl a✝² a✝¹ a✝

case inr
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.coprod = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (inr a✝² a✝¹ a✝) = inr a✝² a✝¹ a✝

case case
p : LambdaParams
U : Type u_1
C : Type u_2
a✝³ : p.coprod = true
a✝² a✝¹ a✝ : LambdaTerm p U C
a_ih✝² : ∀ (n : ℕ), freeVarRange a✝² ≤ n → replace' liftFun n a✝² = a✝²
a_ih✝¹ : ∀ (n : ℕ), freeVarRange a✝¹ ≤ n → replace' liftFun n a✝¹ = a✝¹
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : max (max (freeVarRange a✝²) (freeVarRange a✝¹) - 1) (freeVarRange a✝) ≤ n
⊢ replace' liftFun n (case a✝³ a✝² a✝¹ a✝) = case a✝³ a✝² a✝¹ a✝

case star
p : LambdaParams
U : Type u_1
C : Type u_2
a✝ : p.unit = true
n : ℕ
h : 0 ≤ n
⊢ replace' liftFun n (star a✝) = star a✝

case elim
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m + 1 ≤ n
⊢ replace' liftFun n (var m) = var m
Tactic:
rw [Nat.add_one_le_iff] at h
Proof state after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ replace' liftFun n (var m) = var m
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ replace' liftFun n (var m) = var m
Tactic:
rw [replace'_var, liftFun]
Proof state after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => if n ≤ m then some (var (m + 1)) else none
      | x => none with
    | some u => u
    | none => var m) =
    var m
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match
      match var m with
      | var m => if n ≤ m then some (var (m + 1)) else none
      | x => none with
    | some u => u
    | none => var m) =
    var m
Tactic:
simp only
Proof state after:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match if n ≤ m then some (var (m + 1)) else none with
    | some u => u
    | none => var m) =
    var m
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ (match if n ≤ m then some (var (m + 1)) else none with
    | some u => u
    | none => var m) =
    var m
Tactic:
rw [if_neg]
Proof state after:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ ¬n ≤ m
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ ¬n ≤ m
Tactic:
rw [not_le]
Proof state after:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ m < n
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
case hnc
p : LambdaParams
U : Type u_1
C : Type u_2
m n : ℕ
h : m < n
⊢ m < n
Tactic:
exact h
Proof state after:
no goals
Theorem: LambdaCalculi.LambdaTerm.lift'_eq_of_freeVarRange_le
Proof state before:
case elim
p : LambdaParams
U : Type u_1
C : Type u_2
a✝² : p.empty = true
a✝¹ : LambdaType p U
a✝ : LambdaTerm p U C
a_ih✝ : ∀ (n : ℕ), freeVarRange a✝ ≤ n → replace' liftFun n a✝ = a✝
n : ℕ
h : freeVarRange a✝ ≤ n
⊢ replace' liftFun n (elim a✝² a✝¹ a✝) = elim a✝² a✝¹ a✝
Tactic:
aesop
Proof state after:
no goals
Theorem: MyNat.pow_zero
Proof state before:
m : ℕ
⊢ m ^ 0 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.pow_succ
Proof state before:
m n : ℕ
⊢ m ^ succ n = m ^ n * m
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_zero
Proof state before:
a : ℕ
⊢ a + 0 = a
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.add_succ
Proof state before:
a d : ℕ
⊢ a + succ d = succ (a + d)
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_zero
Proof state before:
a : ℕ
⊢ a * 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.mul_succ
Proof state before:
a b : ℕ
⊢ a * succ b = a * b + a
Tactic:
rfl
Proof state after:
no goals
Theorem: ν
Proof state before:
α : Type u
P : dLang α
f : Lang P
⊢ Dec (dLang.ν P)
Tactic:
induction f with
| universal => exact unit?
Proof state after:
no goals
Theorem: ν
Proof state before:
case universal
α : Type u
P : dLang α
⊢ Dec (dLang.ν fun x => PUnit)
Tactic:
exact unit?
Proof state after:
no goals
Theorem: anda
Proof state before:
a : Prop
⊢ a → a ∧ a
Tactic:
intro a
Proof state after:
a✝ : Prop
a : a✝
⊢ a✝ ∧ a✝
Theorem: anda
Proof state before:
a✝ : Prop
a : a✝
⊢ a✝ ∧ a✝
Tactic:
apply And.intro
Proof state after:
case left
a✝ : Prop
a : a✝
⊢ a✝

case right
a✝ : Prop
a : a✝
⊢ a✝
Theorem: anda
Proof state before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
case left => assumption
Proof state after:
no goals
Theorem: anda
Proof state before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
case right => assumption
Proof state after:
no goals
Theorem: anda
Proof state before:
a✝ : Prop
a : a✝
⊢ a✝
Tactic:
assumption
Proof state after:
no goals
Theorem: rewrite_test
Proof state before:
α✝ : Type u_1
a b c : α✝
⊢ a ≡ b → b ≡ c → a ≡ c
Tactic:
intro ab bc
Proof state after:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Theorem: rewrite_test
Proof state before:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Tactic:
constructor
Proof state after:
case a
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a = c
Theorem: rewrite_test
Proof state before:
case a
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a = c
Tactic:
cases ab with
| mk ab =>
  rw [ab]
  cases bc with
  | mk bc =>
    rw [bc]
Proof state after:
no goals
Theorem: rewrite_test
Proof state before:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ a = c
Tactic:
rw [ab]
Proof state after:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b = c
Theorem: rewrite_test
Proof state before:
case a.mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b = c
Tactic:
cases bc with
| mk bc =>
  rw [bc]
Proof state after:
no goals
Theorem: rewrite_test
Proof state before:
case a.mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ b = c
Tactic:
rw [bc]
Proof state after:
no goals
Theorem: rewrite_test'
Proof state before:
α✝ : Type u_1
a b c : α✝
⊢ a ≡ b → b ≡ c → a ≡ c
Tactic:
intro ab bc
Proof state after:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Theorem: rewrite_test'
Proof state before:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Tactic:
cases ab with
| mk ab =>
  rw [ab]
  cases bc with
  | mk bc =>
    rw [bc]
    constructor
    rfl
Proof state after:
no goals
Theorem: rewrite_test'
Proof state before:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ a ≡ c
Tactic:
rw [ab]
Proof state after:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b ≡ c
Theorem: rewrite_test'
Proof state before:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b ≡ c
Tactic:
cases bc with
| mk bc =>
  rw [bc]
  constructor
  rfl
Proof state after:
no goals
Theorem: rewrite_test'
Proof state before:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ b ≡ c
Tactic:
rw [bc]
Proof state after:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c ≡ c
Theorem: rewrite_test'
Proof state before:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c ≡ c
Tactic:
constructor
Proof state after:
case mk.mk.a
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c = c
Theorem: rewrite_test'
Proof state before:
case mk.mk.a
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c = c
Tactic:
rfl
Proof state after:
no goals
Theorem: rewrite_test'''
Proof state before:
α✝ : Type u_1
a b c : α✝
⊢ a ≡ b → b ≡ c → a ≡ c
Tactic:
intro ab bc
Proof state after:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Theorem: rewrite_test'''
Proof state before:
α✝ : Type u_1
a b c : α✝
ab : a ≡ b
bc : b ≡ c
⊢ a ≡ c
Tactic:
cases ab with
| mk ab =>
  rw [ab]
  cases bc with
  | mk bc =>
    rw [bc]
    constructor
    rfl
Proof state after:
no goals
Theorem: rewrite_test'''
Proof state before:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ a ≡ c
Tactic:
rw [ab]
Proof state after:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b ≡ c
Theorem: rewrite_test'''
Proof state before:
case mk
α✝ : Type u_1
a b c : α✝
bc : b ≡ c
ab : a = b
⊢ b ≡ c
Tactic:
cases bc with
| mk bc =>
  rw [bc]
  constructor
  rfl
Proof state after:
no goals
Theorem: rewrite_test'''
Proof state before:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ b ≡ c
Tactic:
rw [bc]
Proof state after:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c ≡ c
Theorem: rewrite_test'''
Proof state before:
case mk.mk
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c ≡ c
Tactic:
constructor
Proof state after:
case mk.mk.a
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c = c
Theorem: rewrite_test'''
Proof state before:
case mk.mk.a
α✝ : Type u_1
a b c : α✝
ab : a = b
bc : b = c
⊢ c = c
Tactic:
rfl
Proof state after:
no goals
Theorem: cmp_symm
Proof state before:
⊢ ∀ (x y : SmartDesc), Ordering.swap (SmartDesc.compare x y) = SmartDesc.compare y x
Tactic:
sorry
Proof state after:
no goals
Theorem: Ordering.lex_assoc
Proof state before:
⊢ ∀ (a b c : Ordering), lex (lex a b) c = lex a (lex b c)
Tactic:
intros a b c
Proof state after:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Theorem: Ordering.lex_assoc
Proof state before:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
cases a <;> simp [lex]
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
cases a
Proof state after:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)

case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Theorem: Ordering.lex_assoc'
Proof state before:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)

case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
{
  case lt => rfl
}
Proof state after:
case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)

case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)
Tactic:
case eq => rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
case gt => rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
case lt => rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'
Proof state before:
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc''
Proof state before:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
cases a with
| eq => rfl
| lt => rfl
| gt => rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc''
Proof state before:
case eq
b c : Ordering
⊢ lex (lex eq b) c = lex eq (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc''
Proof state before:
case lt
b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc''
Proof state before:
case gt
b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'''
Proof state before:
a b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_assoc'''
Proof state before:
a b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_left_identity
Proof state before:
a : Ordering
⊢ lex eq a = a
Tactic:
cases a <;> rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity
Proof state before:
a : Ordering
⊢ lex a eq = a
Tactic:
cases a <;> rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity'
Proof state before:
⊢ ∀ (x : Ordering), lex x eq = x
Tactic:
intro x
Proof state after:
x : Ordering
⊢ lex x eq = x
Theorem: Ordering.lex_right_identity'
Proof state before:
x : Ordering
⊢ lex x eq = x
Tactic:
cases x
Proof state after:
case lt

⊢ lex lt eq = lt

case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Theorem: Ordering.lex_right_identity'
Proof state before:
case lt

⊢ lex lt eq = lt
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity'
Proof state before:
case eq

⊢ lex eq eq = eq
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity'
Proof state before:
case gt

⊢ lex gt eq = gt
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity''
Proof state before:
⊢ ∀ (x : Ordering), lex x eq = x
Tactic:
intro x
Proof state after:
x : Ordering
⊢ lex x eq = x
Theorem: Ordering.lex_right_identity''
Proof state before:
x : Ordering
⊢ lex x eq = x
Tactic:
cases x
Proof state after:
case lt

⊢ lex lt eq = lt

case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Theorem: Ordering.lex_right_identity''
Proof state before:
case lt

⊢ lex lt eq = lt

case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
Proof state after:
case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Theorem: Ordering.lex_right_identity''
Proof state before:
case eq

⊢ lex eq eq = eq

case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
Proof state after:
case gt

⊢ lex gt eq = gt
Theorem: Ordering.lex_right_identity''
Proof state before:
case gt

⊢ lex gt eq = gt
Tactic:
{ rfl }
Proof state after:
no goals
Theorem: Ordering.lex_right_identity''
Proof state before:
case lt

⊢ lex lt eq = lt
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity''
Proof state before:
case eq

⊢ lex eq eq = eq
Tactic:
rfl
Proof state after:
no goals
Theorem: Ordering.lex_right_identity''
Proof state before:
case gt

⊢ lex gt eq = gt
Tactic:
rfl
Proof state after:
no goals
Theorem: add_left_identity
Proof state before:
a : ℕ
⊢ 0 + a = a
Tactic:
simp
Proof state after:
no goals
Theorem: add_right_identity
Proof state before:
a : ℕ
⊢ a + 0 = a
Tactic:
simp
Proof state after:
no goals
Theorem: bool_or_assoc
Proof state before:
⊢ ∀ (a b c : Bool), (a || b || c) = (a || (b || c))
Tactic:
intro a b c
Proof state after:
a b c : Bool
⊢ (a || b || c) = (a || (b || c))
Theorem: bool_or_assoc
Proof state before:
a b c : Bool
⊢ (a || b || c) = (a || (b || c))
Tactic:
cases a with
| false =>
  simp
| true =>
  simp
Proof state after:
no goals
Theorem: bool_or_assoc
Proof state before:
case false
b c : Bool
⊢ (false || b || c) = (false || (b || c))
Tactic:
simp
Proof state after:
no goals
Theorem: bool_or_assoc
Proof state before:
case true
b c : Bool
⊢ (true || b || c) = (true || (b || c))
Tactic:
simp
Proof state after:
no goals
Theorem: ThunkOrdering.lex_assoc
Proof state before:
⊢ ∀ (a b c : Thunk Ordering), lex (lex a b) c = lex a (lex b c)
Tactic:
intros a b c
Proof state after:
a b c : Thunk Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Theorem: ThunkOrdering.lex_assoc
Proof state before:
a b c : Thunk Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
unfold lex
Proof state after:
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Thunk.get a with
        | Ordering.eq => b
        | x => { fn := fun x => Thunk.get a }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Thunk.get a with
            | Ordering.eq => b
            | x => { fn := fun x => Thunk.get a }) }) =
    match Thunk.get a with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Thunk.get a }
Theorem: ThunkOrdering.lex_assoc
Proof state before:
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Thunk.get a with
        | Ordering.eq => b
        | x => { fn := fun x => Thunk.get a }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Thunk.get a with
            | Ordering.eq => b
            | x => { fn := fun x => Thunk.get a }) }) =
    match Thunk.get a with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Thunk.get a }
Tactic:
cases a.get with
| lt => simp only
        simp [Thunk.get]
| gt => dsimp
        rfl
| eq => dsimp only
Proof state after:
no goals
Theorem: ThunkOrdering.lex_assoc
Proof state before:
case lt
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.lt with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.lt }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.lt with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.lt }) }) =
    match Ordering.lt with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.lt }
Tactic:
simp only
Proof state after:
case lt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.lt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.lt } }) =
    { fn := fun x => Ordering.lt }
Theorem: ThunkOrdering.lex_assoc
Proof state before:
case lt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.lt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.lt } }) =
    { fn := fun x => Ordering.lt }
Tactic:
simp [Thunk.get]
Proof state after:
no goals
Theorem: ThunkOrdering.lex_assoc
Proof state before:
case gt
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.gt with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.gt }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.gt with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.gt }) }) =
    match Ordering.gt with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.gt }
Tactic:
dsimp
Proof state after:
case gt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.gt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.gt } }) =
    { fn := fun x => Ordering.gt }
Theorem: ThunkOrdering.lex_assoc
Proof state before:
case gt
a b c : Thunk Ordering
⊢ (match Thunk.get { fn := fun x => Ordering.gt } with
    | Ordering.eq => c
    | x => { fn := fun x => Thunk.get { fn := fun x => Ordering.gt } }) =
    { fn := fun x => Ordering.gt }
Tactic:
rfl
Proof state after:
no goals
Theorem: ThunkOrdering.lex_assoc
Proof state before:
case eq
a b c : Thunk Ordering
⊢ (match
      Thunk.get
        (match Ordering.eq with
        | Ordering.eq => b
        | x => { fn := fun x => Ordering.eq }) with
    | Ordering.eq => c
    | x =>
      {
        fn := fun x =>
          Thunk.get
            (match Ordering.eq with
            | Ordering.eq => b
            | x => { fn := fun x => Ordering.eq }) }) =
    match Ordering.eq with
    | Ordering.eq =>
      match Thunk.get b with
      | Ordering.eq => c
      | x => { fn := fun x => Thunk.get b }
    | x => { fn := fun x => Ordering.eq }
Tactic:
dsimp only
Proof state after:
no goals
Theorem: ThunkOrdering.lex_left_identity
Proof state before:
a : Thunk Ordering
⊢ lex { fn := fun x => Ordering.eq } a = a
Tactic:
cases a <;> rfl
Proof state after:
no goals
Theorem: ThunkOrdering.lex_right_identity
Proof state before:
a : Thunk Ordering
⊢ lex a { fn := fun x => Ordering.eq } = a
Tactic:
unfold lex
Proof state after:
a : Thunk Ordering
⊢ (match Thunk.get a with
    | Ordering.eq => { fn := fun x => Ordering.eq }
    | x => { fn := fun x => Thunk.get a }) =
    a
Theorem: ThunkOrdering.lex_right_identity
Proof state before:
a : Thunk Ordering
⊢ (match Thunk.get a with
    | Ordering.eq => { fn := fun x => Ordering.eq }
    | x => { fn := fun x => Thunk.get a }) =
    a
Tactic:
cases h: a.get <;>
  simp only <;>
  rw [<-h] <;>
  rfl
Proof state after:
no goals
Theorem: Eq.all_tequal
Proof state before:
α✝ : Sort u_1
x y : α✝
p q : x = y
⊢ p = q
Tactic:
cases p
Proof state after:
case refl
α✝ : Sort u_1
x : α✝
q : x = x
⊢ (_ : x = x) = q