internlm/Lean-Github huggingface dataset:
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n + 2).half + 1 = n + 2
Tactic:
unfold Nat.half
Proof state after:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n.half + 1) + 1 = n + 2
Theorem: Nat.inr_half_eq_of_isOdd
Proof state before:
case step
n : Nat
ih : n.isOdd = true → 2 * n.half + 1 = n
h : (n + 2).isOdd = true
⊢ 2 * (n.half + 1) + 1 = n + 2
Tactic:
rw [Nat.mul_succ, Nat.add_succ, Nat.add_succ, ih h]
Proof state after:
no goals
Theorem: Nat.inl_half_eq_or_inr_half_eq
Proof state before:
n : Nat
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
match isEven_or_isOdd n with
| .inl h => left; exact inl_half_eq_of_isEven h
| .inr h => right; exact inr_half_eq_of_isOdd h
Proof state after:
no goals
Theorem: Nat.inl_half_eq_or_inr_half_eq
Proof state before:
n : Nat
h : n.isEven = true
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
left
Proof state after:
case h
n : Nat
h : n.isEven = true
⊢ n.half.inl = n
Theorem: Nat.inl_half_eq_or_inr_half_eq
Proof state before:
case h
n : Nat
h : n.isEven = true
⊢ n.half.inl = n
Tactic:
exact inl_half_eq_of_isEven h
Proof state after:
no goals
Theorem: Nat.inl_half_eq_or_inr_half_eq
Proof state before:
n : Nat
h : n.isOdd = true
⊢ n.half.inl = n ∨ n.half.inr = n
Tactic:
right
Proof state after:
case h
n : Nat
h : n.isOdd = true
⊢ n.half.inr = n
Theorem: Nat.inl_half_eq_or_inr_half_eq
Proof state before:
case h
n : Nat
h : n.isOdd = true
⊢ n.half.inr = n
Tactic:
exact inr_half_eq_of_isOdd h
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ j = 0 + j
Tactic:
rw [Int.zero_add]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ 0 + j = -i + i + j
Tactic:
rw [Int.add_neg_self_left]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ -i + i + j = -i + (i + j)
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ -i + (i + j) = -i + (i + k)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ -i + (i + k) = -i + i + k
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ -i + i + k = 0 + k
Tactic:
rw [Int.add_neg_self_left]
Proof state after:
no goals
Theorem: Int.add_left_cancel'
Proof state before:
i j k : Int
h : i + j = i + k
⊢ 0 + k = k
Tactic:
rw [Int.zero_add]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ j = j + 0
Tactic:
rw [Int.add_zero]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ j + 0 = j + (i + -i)
Tactic:
rw [Int.add_neg_self_right]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ j + (i + -i) = j + i + -i
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ j + i + -i = k + i + -i
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ k + i + -i = k + (i + -i)
Tactic:
rw [Int.add_assoc]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ k + (i + -i) = k + 0
Tactic:
rw [Int.add_neg_self_right]
Proof state after:
no goals
Theorem: Int.add_right_cancel'
Proof state before:
i j k : Int
h : j + i = k + i
⊢ k + 0 = k
Tactic:
rw [Int.add_zero]
Proof state after:
no goals
Theorem: Int.le.intro'
Proof state before:
i : Int
k : Nat
⊢ (i + ↑k - i).NonNeg
Tactic:
rw [Int.sub_eq, Int.add_right_comm, Int.add_neg_self_right, Int.zero_add]
Proof state after:
i : Int
k : Nat
⊢ (↑k).NonNeg
Theorem: Int.le.intro'
Proof state before:
i : Int
k : Nat
⊢ (↑k).NonNeg
Tactic:
apply NonNeg.mk
Proof state after:
no goals
Theorem: Int.le.dest'
Proof state before:
i j : Int
⊢ i ≤ j → ∃ k, j = i + ofNat k
Tactic:
intro (h : NonNeg (j - i))
Proof state after:
i j : Int
h : (j - i).NonNeg
⊢ ∃ k, j = i + ofNat k
Theorem: Int.le.dest'
Proof state before:
i j : Int
h : (j - i).NonNeg
⊢ ∃ k, j = i + ofNat k
Tactic:
match hk : j - i with
| ofNat k => exists k; rw [←hk, Int.sub_eq, Int.add_left_comm, Int.add_neg_self_right, Int.add_zero]
| negSucc _ => rw [hk] at h; contradiction
Proof state after:
no goals
Theorem: Int.le.dest'
Proof state before:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ ∃ k, j = i + ofNat k
Tactic:
exists k
Proof state after:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ j = i + ofNat k
Theorem: Int.le.dest'
Proof state before:
i j : Int
h : (j - i).NonNeg
k : Nat
hk : j - i = ofNat k
⊢ j = i + ofNat k
Tactic:
rw [←hk, Int.sub_eq, Int.add_left_comm, Int.add_neg_self_right, Int.add_zero]
Proof state after:
no goals
Theorem: Int.le.dest'
Proof state before:
i j : Int
h : (j - i).NonNeg
a✝ : Nat
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k
Tactic:
rw [hk] at h
Proof state after:
i j : Int
a✝ : Nat
h : -[a✝+1].NonNeg
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k
Theorem: Int.le.dest'
Proof state before:
i j : Int
a✝ : Nat
h : -[a✝+1].NonNeg
hk : j - i = -[a✝+1]
⊢ ∃ k, j = i + ofNat k
Tactic:
contradiction
Proof state after:
no goals
Theorem: Int.le_iff_lt_succ
Proof state before:
i j : Int
⊢ i ≤ j ↔ i < j + 1
Tactic:
rw [Int.lt_iff_succ_le]
Proof state after:
i j : Int
⊢ i ≤ j ↔ i + 1 ≤ j + 1
Theorem: Int.le_iff_lt_succ
Proof state before:
i j : Int
⊢ i ≤ j ↔ i + 1 ≤ j + 1
Tactic:
constructor
Proof state after:
case mp
i j : Int
⊢ i ≤ j → i + 1 ≤ j + 1

case mpr
i j : Int
⊢ i + 1 ≤ j + 1 → i ≤ j
Theorem: Int.le_iff_lt_succ
Proof state before:
case mp
i j : Int
⊢ i ≤ j → i + 1 ≤ j + 1
Tactic:
apply Int.add_le_add_right (c:=1)
Proof state after:
no goals
Theorem: Int.le_iff_lt_succ
Proof state before:
case mpr
i j : Int
⊢ i + 1 ≤ j + 1 → i ≤ j
Tactic:
apply Int.le_of_add_le_add_right
Proof state after:
no goals
Theorem: Int.le_or_gt
Proof state before:
i j : Int
⊢ i ≤ j ∨ j < i
Tactic:
induction i using Int.casesMkOn with
| mk mi ni =>
  induction j using Int.casesMkOn with
  | mk mj nj =>
    rw [mk_le_mk, mk_lt_mk]
    rw [Nat.add_comm mi, Nat.add_comm mj]
    exact (Nat.lt_or_ge ..).symm
Proof state after:
no goals
Theorem: Int.le_or_gt
Proof state before:
case mk
j : Int
mi ni : Nat
⊢ mi ⊖ ni ≤ j ∨ j < mi ⊖ ni
Tactic:
induction j using Int.casesMkOn with
| mk mj nj =>
  rw [mk_le_mk, mk_lt_mk]
  rw [Nat.add_comm mi, Nat.add_comm mj]
  exact (Nat.lt_or_ge ..).symm
Proof state after:
no goals
Theorem: Int.le_or_gt
Proof state before:
case mk.mk
mi ni mj nj : Nat
⊢ mi ⊖ ni ≤ mj ⊖ nj ∨ mj ⊖ nj < mi ⊖ ni
Tactic:
rw [mk_le_mk, mk_lt_mk]
Proof state after:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ mj + ni ∨ ni + mj < mi + nj
Theorem: Int.le_or_gt
Proof state before:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ mj + ni ∨ ni + mj < mi + nj
Tactic:
rw [Nat.add_comm mi, Nat.add_comm mj]
Proof state after:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ ni + mj ∨ ni + mj < nj + mi
Theorem: Int.le_or_gt
Proof state before:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ ni + mj ∨ ni + mj < nj + mi
Tactic:
exact (Nat.lt_or_ge ..).symm
Proof state after:
no goals
Theorem: Int.lt_or_ge
Proof state before:
i j : Int
⊢ i < j ∨ j ≤ i
Tactic:
cases Int.le_or_gt j i with
| inl h => right; exact h
| inr h => left; exact h
Proof state after:
no goals
Theorem: Int.lt_or_ge
Proof state before:
case inl
i j : Int
h : j ≤ i
⊢ i < j ∨ j ≤ i
Tactic:
right
Proof state after:
case inl.h
i j : Int
h : j ≤ i
⊢ j ≤ i
Theorem: Int.lt_or_ge
Proof state before:
case inl.h
i j : Int
h : j ≤ i
⊢ j ≤ i
Tactic:
exact h
Proof state after:
no goals
Theorem: Int.lt_or_ge
Proof state before:
case inr
i j : Int
h : i < j
⊢ i < j ∨ j ≤ i
Tactic:
left
Proof state after:
case inr.h
i j : Int
h : i < j
⊢ i < j
Theorem: Int.lt_or_ge
Proof state before:
case inr.h
i j : Int
h : i < j
⊢ i < j
Tactic:
exact h
Proof state after:
no goals
Theorem: Int.lt_or_eq_of_le
Proof state before:
i j : Int
⊢ i ≤ j → i < j ∨ i = j
Tactic:
intro hle
Proof state after:
i j : Int
hle : i ≤ j
⊢ i < j ∨ i = j
Theorem: Int.lt_or_eq_of_le
Proof state before:
i j : Int
hle : i ≤ j
⊢ i < j ∨ i = j
Tactic:
match le.dest' hle with
| ⟨0, (h : j = i + 0)⟩ =>
  right
  rw [h, Int.add_zero]
| ⟨n+1, (h : j = i + (ofNat n + 1))⟩ =>
  left
  rw [Int.lt_iff_succ_le]
  rw [h, ←Int.add_assoc, Int.add_right_comm]
  apply Int.le.intro'
Proof state after:
no goals
Theorem: Int.lt_or_eq_of_le
Proof state before:
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i < j ∨ i = j
Tactic:
right
Proof state after:
case h
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i = j
Theorem: Int.lt_or_eq_of_le
Proof state before:
case h
i j : Int
hle : i ≤ j
h : j = i + 0
⊢ i = j
Tactic:
rw [h, Int.add_zero]
Proof state after:
no goals
Theorem: Int.lt_or_eq_of_le
Proof state before:
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j ∨ i = j
Tactic:
left
Proof state after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j
Theorem: Int.lt_or_eq_of_le
Proof state before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i < j
Tactic:
rw [Int.lt_iff_succ_le]
Proof state after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ j
Theorem: Int.lt_or_eq_of_le
Proof state before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ j
Tactic:
rw [h, ←Int.add_assoc, Int.add_right_comm]
Proof state after:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ i + 1 + ofNat n
Theorem: Int.lt_or_eq_of_le
Proof state before:
case h
i j : Int
hle : i ≤ j
n : Nat
h : j = i + (ofNat n + 1)
⊢ i + 1 ≤ i + 1 + ofNat n
Tactic:
apply Int.le.intro'
Proof state after:
no goals
Theorem: Int.lt_of_le_of_ne
Proof state before:
i j : Int
⊢ i ≤ j → i ≠ j → i < j
Tactic:
intro hle hne
Proof state after:
i j : Int
hle : i ≤ j
hne : i ≠ j
⊢ i < j
Theorem: Int.lt_of_le_of_ne
Proof state before:
i j : Int
hle : i ≤ j
hne : i ≠ j
⊢ i < j
Tactic:
cases lt_or_eq_of_le hle with
| inl hlt => exact hlt
| inr heq => absurd heq; exact hne
Proof state after:
no goals
Theorem: Int.lt_of_le_of_ne
Proof state before:
case inl
i j : Int
hle : i ≤ j
hne : i ≠ j
hlt : i < j
⊢ i < j
Tactic:
exact hlt
Proof state after:
no goals
Theorem: Int.lt_of_le_of_ne
Proof state before:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ i < j
Tactic:
absurd heq
Proof state after:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ ¬i = j
Theorem: Int.lt_of_le_of_ne
Proof state before:
case inr
i j : Int
hle : i ≤ j
hne : i ≠ j
heq : i = j
⊢ ¬i = j
Tactic:
exact hne
Proof state after:
no goals
Theorem: Int.lt_connex
Proof state before:
i j : Int
⊢ i ≠ j → i < j ∨ j < i
Tactic:
intro hne
Proof state after:
i j : Int
hne : i ≠ j
⊢ i < j ∨ j < i
Theorem: Int.lt_connex
Proof state before:
i j : Int
hne : i ≠ j
⊢ i < j ∨ j < i
Tactic:
cases Int.le_or_gt i j with
| inl hle => left; apply Int.lt_of_le_of_ne hle hne
| inr hgt => right; exact hgt
Proof state after:
no goals
Theorem: Int.lt_connex
Proof state before:
case inl
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j ∨ j < i
Tactic:
left
Proof state after:
case inl.h
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j
Theorem: Int.lt_connex
Proof state before:
case inl.h
i j : Int
hne : i ≠ j
hle : i ≤ j
⊢ i < j
Tactic:
apply Int.lt_of_le_of_ne hle hne
Proof state after:
no goals
Theorem: Int.lt_connex
Proof state before:
case inr
i j : Int
hne : i ≠ j
hgt : j < i
⊢ i < j ∨ j < i
Tactic:
right
Proof state after:
case inr.h
i j : Int
hne : i ≠ j
hgt : j < i
⊢ j < i
Theorem: Int.lt_connex
Proof state before:
case inr.h
i j : Int
hne : i ≠ j
hgt : j < i
⊢ j < i
Tactic:
exact hgt
Proof state after:
no goals
Theorem: Int.lt_compare
Proof state before:
i j : Int
⊢ i < j → ∀ (k : Int), i < k ∨ k < j
Tactic:
intro hij k
Proof state after:
i j : Int
hij : i < j
k : Int
⊢ i < k ∨ k < j
Theorem: Int.lt_compare
Proof state before:
i j : Int
hij : i < j
k : Int
⊢ i < k ∨ k < j
Tactic:
cases Int.le_or_gt k i with
| inl hle => right; exact Int.lt_of_le_of_lt hle hij
| inr hgt => left; exact hgt
Proof state after:
no goals
Theorem: Int.lt_compare
Proof state before:
case inl
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ i < k ∨ k < j
Tactic:
right
Proof state after:
case inl.h
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ k < j
Theorem: Int.lt_compare
Proof state before:
case inl.h
i j : Int
hij : i < j
k : Int
hle : k ≤ i
⊢ k < j
Tactic:
exact Int.lt_of_le_of_lt hle hij
Proof state after:
no goals
Theorem: Int.lt_compare
Proof state before:
case inr
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k ∨ k < j
Tactic:
left
Proof state after:
case inr.h
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k
Theorem: Int.lt_compare
Proof state before:
case inr.h
i j : Int
hij : i < j
k : Int
hgt : i < k
⊢ i < k
Tactic:
exact hgt
Proof state after:
no goals
Theorem: LList.cons_append
Proof state before:
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs = a :: as.append bs
Tactic:
apply eq_of_heq
Proof state after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs ≅ a :: as.append bs
Theorem: LList.cons_append
Proof state before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (a :: as).append bs ≅ a :: as.append bs
Tactic:
unfold LList.append LList.cons
Proof state after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (let_fun this := ⋯ ▸ (HList.cons a as).append bs;
    this) ≅
    HList.cons a
      (let_fun this := ⋯ ▸ HList.append as bs;
      this)
Theorem: LList.cons_append
Proof state before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (let_fun this := ⋯ ▸ (HList.cons a as).append bs;
    this) ≅
    HList.cons a
      (let_fun this := ⋯ ▸ HList.append as bs;
      this)
Tactic:
elim_casts
Proof state after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (HList.cons a as).append bs ≅ HList.cons a (⋯ ▸ HList.append as bs)
Theorem: LList.cons_append
Proof state before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ (HList.cons a as).append bs ≅ HList.cons a (⋯ ▸ HList.append as bs)
Tactic:
rw [HList.cons_append]
Proof state after:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.cons a (HList.append as bs) ≅ HList.cons a (⋯ ▸ HList.append as bs)
Theorem: LList.cons_append
Proof state before:
case h
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.cons a (HList.append as bs) ≅ HList.cons a (⋯ ▸ HList.append as bs)
Tactic:
apply HList.cons_hcongr
Proof state after:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ α = α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ List.replicate n α ++ List.replicate m α = List.replicate (m + n) α

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ a ≅ a

case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ ⋯ ▸ HList.append as bs
Theorem: LList.cons_append
Proof state before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ α = α
Tactic:
reflexivity
Proof state after:
no goals
Theorem: LList.cons_append
Proof state before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ List.replicate n α ++ List.replicate m α = List.replicate (m + n) α
Tactic:
rw [List.replicate_add]
Proof state after:
no goals
Theorem: LList.cons_append
Proof state before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ a ≅ a
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: LList.cons_append
Proof state before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ ⋯ ▸ HList.append as bs
Tactic:
elim_casts
Proof state after:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ HList.append as bs
Theorem: LList.cons_append
Proof state before:
case h.a
α : Sort u_1
n m : Nat
a : α
as : LList α n
bs : LList α m
⊢ HList.append as bs ≅ HList.append as bs
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: LList.append_nil
Proof state before:
case nil
α : Sort u_1
n : Nat
⊢ LList.nil.append LList.nil ≅ LList.nil
Tactic:
rw [LList.nil_append]
Proof state after:
no goals
Theorem: LList.append_nil
Proof state before:
case cons
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ (a✝ :: as✝).append LList.nil ≅ a✝ :: as✝
Tactic:
rw [LList.cons_append]
Proof state after:
case cons
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ :: as✝.append LList.nil ≅ a✝ :: as✝
Theorem: LList.append_nil
Proof state before:
case cons
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ :: as✝.append LList.nil ≅ a✝ :: as✝
Tactic:
apply LList.cons_hcongr
Proof state after:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ α = α

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ 0 + n✝ = n✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ ≅ a✝

case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ as✝.append LList.nil ≅ as✝
Theorem: LList.append_nil
Proof state before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ α = α
Tactic:
reflexivity
Proof state after:
no goals
Theorem: LList.append_nil
Proof state before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ 0 + n✝ = n✝
Tactic:
rw [Nat.zero_add]
Proof state after:
no goals
Theorem: LList.append_nil
Proof state before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ a✝ ≅ a✝
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: LList.append_nil
Proof state before:
case cons.a
α : Sort u_1
n n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : as✝.append LList.nil ≅ as✝
⊢ as✝.append LList.nil ≅ as✝
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: LList.append_assoc
Proof state before:
case nil
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
⊢ (LList.nil.append bs).append cs ≅ LList.nil.append (bs.append cs)
Tactic:
rw [LList.nil_append, LList.nil_append]
Proof state after:
no goals
Theorem: LList.append_assoc
Proof state before:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ ((a✝ :: as✝).append bs).append cs ≅ (a✝ :: as✝).append (bs.append cs)
Tactic:
rw [LList.cons_append, LList.cons_append, LList.cons_append]
Proof state after:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ :: (as✝.append bs).append cs ≅ a✝ :: as✝.append (bs.append cs)
Theorem: LList.append_assoc
Proof state before:
case cons
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ :: (as✝.append bs).append cs ≅ a✝ :: as✝.append (bs.append cs)
Tactic:
apply LList.cons_hcongr
Proof state after:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ α = α

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ n + (m + n✝) = n + m + n✝

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ ≅ a✝

case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
Theorem: LList.append_assoc
Proof state before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ α = α
Tactic:
reflexivity
Proof state after:
no goals
Theorem: LList.append_assoc
Proof state before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ n + (m + n✝) = n + m + n✝
Tactic:
rw [Nat.add_assoc]
Proof state after:
no goals
Theorem: LList.append_assoc
Proof state before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ a✝ ≅ a✝
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: LList.append_assoc
Proof state before:
case cons.a
α : Sort u_1
l m n : Nat
bs : LList α m
cs : LList α n
n✝ : Nat
a✝ : α
as✝ : LList α n✝
ih : (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
⊢ (as✝.append bs).append cs ≅ as✝.append (bs.append cs)
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: LList.eval_cons_zero
Proof state before:
α : Sort u_1
n : Nat
a : α
as : LList α n
⊢ (a :: as).eval (Fin.zero ⋯) = a
Tactic:
simp only [Fin.zero, LList.eval]
Proof state after:
no goals
Theorem: LList.eval_cons_succ
Proof state before:
α : Sort u_1
n : Nat
a : α
as : LList α n
i : Fin n
⊢ (a :: as).eval i.succ = as.eval i
Tactic:
simp only [Fin.succ, LList.eval]
Proof state after:
no goals
Theorem: Fin.val_ndrec
Proof state before:
n m : Nat
i : Fin n
h : n = m
⊢ ↑(h ▸ i) = ↑i
Tactic:
cases h
Proof state after:
case refl
n : Nat
i : Fin n
⊢ ↑(⋯ ▸ i) = ↑i
Theorem: Fin.val_ndrec
Proof state before:
case refl
n : Nat
i : Fin n
⊢ ↑(⋯ ▸ i) = ↑i
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero ↔ IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
constructor
Proof state after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨0, isLt✝⟩

case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = IndView.zero
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
intro
Proof state after:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : ⟨0, isLt✝⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mp
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : ⟨0, isLt✝⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩
Tactic:
reflexivity
Proof state after:
no goals
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
⊢ IndView.zero.toFin = ⟨0, isLt✝⟩ → ⟨0, isLt✝⟩.toIndView = IndView.zero
Tactic:
intro
Proof state after:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : IndView.zero.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero
Theorem: Fin.toIndView_eq_iff_toFin_eq
Proof state before:
case mpr
n✝¹ n✝ : Nat
i : Fin n✝
j : Fin.IndView n✝
n : Nat
isLt✝ : 0 < n + 1
a✝ : IndView.zero.toFin = ⟨0, isLt✝⟩
⊢ ⟨0, isLt✝⟩.toIndView = IndView.zero
Tactic:
reflexivity
Proof state after:
no goals