internlm/Lean-Github huggingface dataset:
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n

case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
. apply Nat.le_of_eq (@Nat.sub_add_eq_sub_sub m k n)
Proof state after:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
. apply Nat.sub_lt
  . exact Nat.zero_lt_sub_of_lt hkm
  . exact hn
Proof state after:
no goals
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n
Tactic:
apply Nat.le_of_eq (@Nat.sub_add_eq_sub_sub m k n)
Proof state after:
no goals
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
apply Nat.sub_lt
Proof state after:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k

case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k

case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
. exact Nat.zero_lt_sub_of_lt hkm
Proof state after:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
. exact hn
Proof state after:
no goals
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k
Tactic:
exact Nat.zero_lt_sub_of_lt hkm
Proof state after:
no goals
Theorem: Nat.lt_of_sub_add
Proof state before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
exact hn
Proof state after:
no goals
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
⊢ x < y
Tactic:
unfold LT.lt
Proof state after:
x y : Nat
h : ¬x ≥ y
⊢ instLTNat.1 x y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
⊢ instLTNat.1 x y
Tactic:
unfold instLTNat
Proof state after:
x y : Nat
h : ¬x ≥ y
⊢ { lt := Nat.lt }.1 x y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
⊢ { lt := Nat.lt }.1 x y
Tactic:
unfold Nat.lt
Proof state after:
x y : Nat
h : ¬x ≥ y
⊢ { lt := fun n m => Nat.le (succ n) m }.1 x y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
⊢ { lt := fun n m => Nat.le (succ n) m }.1 x y
Tactic:
simp only
Proof state after:
x y : Nat
h : ¬x ≥ y
⊢ Nat.le (succ x) y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
⊢ Nat.le (succ x) y
Tactic:
have h' : Nat.le (Nat.succ x) y = ((x + 1) ≤ y) := rfl
Proof state after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ Nat.le (succ x) y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ Nat.le (succ x) y
Tactic:
rw [h']
Proof state after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ x + 1 ≤ y
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ x + 1 ≤ y
Tactic:
rw [←Nat.not_le_eq]
Proof state after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ ¬y ≤ x
Theorem: Nat.lt_of_not_ge
Proof state before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ ¬y ≤ x
Tactic:
apply h
Proof state after:
no goals
Theorem: Int.toNat_of_ofNat_inj
Proof state before:
⊢ ∀ (z : Int), z ≥ 0 → ofNat (toNat z) = z
Tactic:
intros z h
Proof state after:
z : Int
h : z ≥ 0
⊢ ofNat (toNat z) = z
Theorem: Int.toNat_of_ofNat_inj
Proof state before:
z : Int
h : z ≥ 0
⊢ ofNat (toNat z) = z
Tactic:
cases z with
| ofNat n => simp [toNat, ofNat]
| negSucc n => contradiction
Proof state after:
no goals
Theorem: Int.toNat_of_ofNat_inj
Proof state before:
case ofNat
n : Nat
h : ofNat n ≥ 0
⊢ ofNat (toNat (ofNat n)) = ofNat n
Tactic:
simp [toNat, ofNat]
Proof state after:
no goals
Theorem: Int.toNat_of_ofNat_inj
Proof state before:
case negSucc
n : Nat
h : negSucc n ≥ 0
⊢ ofNat (toNat (negSucc n)) = negSucc n
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.abs_of_nonneg_eq_toNat
Proof state before:
⊢ ∀ (z : Int), z ≥ 0 → abs z = toNat z
Tactic:
intros z h
Proof state after:
z : Int
h : z ≥ 0
⊢ abs z = toNat z
Theorem: Int.abs_of_nonneg_eq_toNat
Proof state before:
z : Int
h : z ≥ 0
⊢ abs z = toNat z
Tactic:
cases z with
| ofNat n => simp [toNat, ofNat, abs]
| negSucc n => contradiction
Proof state after:
no goals
Theorem: Int.abs_of_nonneg_eq_toNat
Proof state before:
case ofNat
n : Nat
h : ofNat n ≥ 0
⊢ abs (ofNat n) = toNat (ofNat n)
Tactic:
simp [toNat, ofNat, abs]
Proof state after:
no goals
Theorem: Int.abs_of_nonneg_eq_toNat
Proof state before:
case negSucc
n : Nat
h : negSucc n ≥ 0
⊢ abs (negSucc n) = toNat (negSucc n)
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.neg_succ_eq_neg_ofNat_succ
Proof state before:
n : Nat
⊢ negSucc n = -ofNat (Nat.succ n)
Tactic:
unfold Neg.neg
Proof state after:
n : Nat
⊢ negSucc n = instNegInt.1 (ofNat (Nat.succ n))
Theorem: Int.neg_succ_eq_neg_ofNat_succ
Proof state before:
n : Nat
⊢ negSucc n = instNegInt.1 (ofNat (Nat.succ n))
Tactic:
unfold instNegInt
Proof state after:
n : Nat
⊢ negSucc n = { neg := Int.neg }.1 (ofNat (Nat.succ n))
Theorem: Int.neg_succ_eq_neg_ofNat_succ
Proof state before:
n : Nat
⊢ negSucc n = { neg := Int.neg }.1 (ofNat (Nat.succ n))
Tactic:
unfold Int.neg
Proof state after:
n : Nat
⊢ negSucc n =
    {
          neg := fun n =>
            match n with
            | ofNat n => negOfNat n
            | negSucc n => ofNat (Nat.succ n) }.1
      (ofNat (Nat.succ n))
Theorem: Int.neg_succ_eq_neg_ofNat_succ
Proof state before:
n : Nat
⊢ negSucc n =
    {
          neg := fun n =>
            match n with
            | ofNat n => negOfNat n
            | negSucc n => ofNat (Nat.succ n) }.1
      (ofNat (Nat.succ n))
Tactic:
simp only [negOfNat]
Proof state after:
no goals
Theorem: Int.add_neg_eq_sub
Proof state before:
m n : Int
⊢ n < 0 → m + n = m - ofNat (abs n)
Tactic:
intros h
Proof state after:
m n : Int
h : n < 0
⊢ m + n = m - ofNat (abs n)
Theorem: Int.add_neg_eq_sub
Proof state before:
m n : Int
h : n < 0
⊢ m + n = m - ofNat (abs n)
Tactic:
cases n with
| ofNat n => contradiction
| negSucc n =>
  simp only [abs]
  unfold HSub.hSub
  unfold instHSub
  unfold Sub.sub
  unfold Int.instSubInt
  unfold Int.sub
  simp only
  rw [neg_succ_eq_neg_ofNat_succ]
Proof state after:
no goals
Theorem: Int.add_neg_eq_sub
Proof state before:
case ofNat
m : Int
n : Nat
h : ofNat n < 0
⊢ m + ofNat n = m - ofNat (abs (ofNat n))
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (abs (negSucc n))
Tactic:
simp only [abs]
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (Nat.succ n)
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m - ofNat (Nat.succ n)
Tactic:
unfold HSub.hSub
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = instHSub.1 m (ofNat (Nat.succ n))
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = instHSub.1 m (ofNat (Nat.succ n))
Tactic:
unfold instHSub
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => Sub.sub a b }.1 m (ofNat (Nat.succ n))
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => Sub.sub a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Sub.sub
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => instSubInt.1 a b }.1 m (ofNat (Nat.succ n))
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => instSubInt.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Int.instSubInt
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := Int.sub }.1 a b }.1 m (ofNat (Nat.succ n))
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := Int.sub }.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
unfold Int.sub
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := fun m n => m + -n }.1 a b }.1 m (ofNat (Nat.succ n))
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = { hSub := fun a b => { sub := fun m n => m + -n }.1 a b }.1 m (ofNat (Nat.succ n))
Tactic:
simp only
Proof state after:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m + -ofNat (Nat.succ n)
Theorem: Int.add_neg_eq_sub
Proof state before:
case negSucc
m : Int
n : Nat
h : negSucc n < 0
⊢ m + negSucc n = m + -ofNat (Nat.succ n)
Tactic:
rw [neg_succ_eq_neg_ofNat_succ]
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
⊢ ∀ (x y : Int), x + y = y + x
Tactic:
intros x y
Proof state after:
x y : Int
⊢ x + y = y + x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ x + y = y + x
Tactic:
unfold HAdd.hAdd
Proof state after:
x y : Int
⊢ instHAdd.1 x y = instHAdd.1 y x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ instHAdd.1 x y = instHAdd.1 y x
Tactic:
unfold instHAdd
Proof state after:
x y : Int
⊢ { hAdd := fun a b => Add.add a b }.1 x y = { hAdd := fun a b => Add.add a b }.1 y x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ { hAdd := fun a b => Add.add a b }.1 x y = { hAdd := fun a b => Add.add a b }.1 y x
Tactic:
unfold Add.add
Proof state after:
x y : Int
⊢ { hAdd := fun a b => instAddInt.1 a b }.1 x y = { hAdd := fun a b => instAddInt.1 a b }.1 y x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ { hAdd := fun a b => instAddInt.1 a b }.1 x y = { hAdd := fun a b => instAddInt.1 a b }.1 y x
Tactic:
unfold instAddInt
Proof state after:
x y : Int
⊢ { hAdd := fun a b => { add := Int.add }.1 a b }.1 x y = { hAdd := fun a b => { add := Int.add }.1 a b }.1 y x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ { hAdd := fun a b => { add := Int.add }.1 a b }.1 x y = { hAdd := fun a b => { add := Int.add }.1 a b }.1 y x
Tactic:
unfold Int.add
Proof state after:
x y : Int
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      x y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y x
Theorem: Int.add_comm
Proof state before:
x y : Int
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      x y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y x
Tactic:
induction x with
| ofNat n =>
  cases y with
  | ofNat m => simp [Nat.add_comm]
  | negSucc m => simp
| negSucc n =>
  cases y with
  | ofNat m => simp
  | negSucc m => simp [Nat.add_comm]
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case ofNat
y : Int
n : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y (ofNat n)
Tactic:
cases y with
| ofNat m => simp [Nat.add_comm]
| negSucc m => simp
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case ofNat.ofNat
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) (ofNat m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat m) (ofNat n)
Tactic:
simp [Nat.add_comm]
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case ofNat.negSucc
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat n) (negSucc m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc m) (ofNat n)
Tactic:
simp
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case negSucc
y : Int
n : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) y =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      y (negSucc n)
Tactic:
cases y with
| ofNat m => simp
| negSucc m => simp [Nat.add_comm]
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case negSucc.ofNat
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) (ofNat m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (ofNat m) (negSucc n)
Tactic:
simp
Proof state after:
no goals
Theorem: Int.add_comm
Proof state before:
case negSucc.negSucc
n m : Nat
⊢ {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc n) (negSucc m) =
    {
          hAdd := fun a b =>
            {
                  add := fun m n =>
                    match m, n with
                    | ofNat m, ofNat n => ofNat (m + n)
                    | ofNat m, negSucc n => subNatNat m (Nat.succ n)
                    | negSucc m, ofNat n => subNatNat n (Nat.succ m)
                    | negSucc m, negSucc n => negSucc (Nat.succ (m + n)) }.1
              a b }.1
      (negSucc m) (negSucc n)
Tactic:
simp [Nat.add_comm]
Proof state after:
no goals
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
p q : Prop
ip : Decidable p
iq : Decidable q
h : p = q
⊢ decide p = decide q
Tactic:
cases h
Proof state after:
case refl
p : Prop
ip iq : Decidable p
⊢ decide p = decide p
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl
p : Prop
ip iq : Decidable p
⊢ decide p = decide p
Tactic:
apply congr
Proof state after:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p

case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p

case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
. simp
Proof state after:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
. apply eq_of_heq
  apply Subsingleton.helim
  rfl
Proof state after:
no goals
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₁
p : Prop
ip iq : Decidable p
⊢ @decide p = @decide p
Tactic:
simp
Proof state after:
no goals
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₂
p : Prop
ip iq : Decidable p
⊢ ip = iq
Tactic:
apply eq_of_heq
Proof state after:
case refl.h₂.h
p : Prop
ip iq : Decidable p
⊢ HEq ip iq
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₂.h
p : Prop
ip iq : Decidable p
⊢ HEq ip iq
Tactic:
apply Subsingleton.helim
Proof state after:
case refl.h₂.h.h₂
p : Prop
ip iq : Decidable p
⊢ Decidable p = Decidable p
Theorem: Decidable.prop_eq_of_decide_eq
Proof state before:
case refl.h₂.h.h₂
p : Prop
ip iq : Decidable p
⊢ Decidable p = Decidable p
Tactic:
rfl
Proof state after:
no goals
Theorem: List.matchKey_snd_length
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), length (matchKey xs k).snd ≤ length xs
Tactic:
intros xs k
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs
Theorem: List.matchKey_snd_length
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
induction xs with
| nil => exact Nat.le.refl
| cons x xs ih =>
  simp only [matchKey]
  apply @Decidable.byCases (x.1=k) _
  . intros heq
    simp only [heq]
    rw [ite_true]
    simp only [Prod.snd]
    apply Nat.le_step
    exact ih
  . intros hneq
    simp only [hneq]
    rw [ite_false]
    simp only [Prod.fst]
    apply Nat.succ_le_succ
    exact ih
Proof state after:
no goals
Theorem: List.matchKey_snd_length
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
⊢ length (matchKey [] k).snd ≤ length []
Tactic:
exact Nat.le.refl
Proof state after:
no goals
Theorem: List.matchKey_snd_length
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length (matchKey (x :: xs) k).snd ≤ length (x :: xs)
Tactic:
simp only [matchKey]
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length
      (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ length
      (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
Tactic:
apply @Decidable.byCases (x.1=k) _
Proof state after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
          else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
      length (x :: xs)

case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
          else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
      length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
          else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
      length (x :: xs)

case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
          else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
      length (x :: xs)
Tactic:
. intros heq
  simp only [heq]
  rw [ite_true]
  simp only [Prod.snd]
  apply Nat.le_step
  exact ih
Proof state after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
          else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd ≤
      length (x :: xs)