internlm/Lean-Github huggingface dataset:
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y : α
x✝ : reflRel r x y
⊢ coRel r x x
Tactic:
exact Quasiorder.co_refl x
Proof state after:
no goals
Theorem: Relation.LinearOrder.coRel_iff_reflRel
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝¹ : StableEq α
inst✝ : ComplementedRel r
x y✝ : α
x✝ : reflRel r x y✝
y : α
hxy : r x y
⊢ coRel r x y
Tactic:
exact Asymmetric.asymm hxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.rc_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
by_cases x = y using Complemented with
| .isTrue rfl => left; right; rfl
| .isFalse hne =>
  cases Connex.connex (r:=r) hne with
  | inl hxy => left; left; exact hxy
  | inr hyx => right; left; exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.rc_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x ∨ reflRel r x x
Tactic:
left
Proof state after:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ reflRel r x x
Tactic:
right
Proof state after:
case h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ x = x
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x : α
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Relation.LinearOrder.rc_total
Proof state before:
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
cases Connex.connex (r:=r) hne with
| inl hxy => left; left; exact hxy
| inr hyx => right; left; exact hyx
Proof state after:
no goals
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inl
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
left
Proof state after:
case inl.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inl.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ reflRel r x y
Tactic:
left
Proof state after:
case inl.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ r x y
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inl.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hxy : r x y
⊢ r x y
Tactic:
exact hxy
Proof state after:
no goals
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inr
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r x y ∨ reflRel r y x
Tactic:
right
Proof state after:
case inr.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r y x
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inr.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ reflRel r y x
Tactic:
left
Proof state after:
case inr.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ r y x
Theorem: Relation.LinearOrder.rc_total
Proof state before:
case inr.h.h
α : Sort u_1
r : α → α → Prop
self : LinearOrder r
inst✝ : ComplementedEq α
x y : α
hne : ¬x = y
hyx : r y x
⊢ r y x
Tactic:
exact hyx
Proof state after:
no goals
Theorem: ENat.first_leNat_of
Proof state before:
p : Nat → Bool
x : Nat
h : p x = true
⊢ (first p).leNat x = true
Tactic:
match x with
| 0 => exact h
| x+1 => simp [first, first.leNat, h]
Proof state after:
no goals
Theorem: ENat.first_leNat_of
Proof state before:
p : Nat → Bool
x : Nat
h : p 0 = true
⊢ (first p).leNat 0 = true
Tactic:
exact h
Proof state after:
no goals
Theorem: ENat.first_leNat_of
Proof state before:
p : Nat → Bool
x✝ x : Nat
h : p (x + 1) = true
⊢ (first p).leNat (x + 1) = true
Tactic:
simp [first, first.leNat, h]
Proof state after:
no goals
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case zero
p : Nat → Bool
h : (first p).leNat 0 = true
⊢ ∃ y, y ≤ 0 ∧ p y = true
Tactic:
exists 0
Proof state after:
no goals
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case succ
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : (first p).leNat (x + 1) = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
simp [first, first.leNat] at h
Proof state after:
case succ
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true ∨ ENat.first.leNat p x = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
exists x+1
Proof state after:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1 ∧ p (x + 1) = true
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case succ.inl
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1 ∧ p (x + 1) = true
Tactic:
constructor
Proof state after:
case succ.inl.left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1

case succ.inl.right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ p (x + 1) = true
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case succ.inl.left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ x + 1 ≤ x + 1
Tactic:
exact Nat.le_refl ..
Proof state after:
no goals
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case succ.inl.right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : p (x + 1) = true
⊢ p (x + 1) = true
Tactic:
exact h
Proof state after:
no goals
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ ∃ y, y ≤ x + 1 ∧ p y = true
Tactic:
exists y
Proof state after:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1 ∧ p y = true
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1 ∧ p y = true
Tactic:
constructor
Proof state after:
case left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1

case right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ p y = true
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case left
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ y ≤ x + 1
Tactic:
exact Nat.le_trans hle (Nat.le_succ ..)
Proof state after:
no goals
Theorem: ENat.exists_le_first_of_first_leNat
Proof state before:
case right
p : Nat → Bool
x : Nat
ih : (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
h : ENat.first.leNat p x = true
y : Nat
hle : y ≤ x
hy : p y = true
⊢ p y = true
Tactic:
exact hy
Proof state after:
no goals
Theorem: ENat.first_leNat_iff_exists_le
Proof state before:
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true ↔ ∃ y, y ≤ x ∧ p y = true
Tactic:
constructor
Proof state after:
case mp
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true

case mpr
p : Nat → Bool
x : Nat
⊢ (∃ y, y ≤ x ∧ p y = true) → (first p).leNat x = true
Theorem: ENat.first_leNat_iff_exists_le
Proof state before:
case mp
p : Nat → Bool
x : Nat
⊢ (first p).leNat x = true → ∃ y, y ≤ x ∧ p y = true
Tactic:
exact exists_le_first_of_first_leNat
Proof state after:
no goals
Theorem: ENat.first_leNat_iff_exists_le
Proof state before:
case mpr
p : Nat → Bool
x : Nat
⊢ (∃ y, y ≤ x ∧ p y = true) → (first p).leNat x = true
Tactic:
intro ⟨y, hle, hy⟩
Proof state after:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat x = true
Theorem: ENat.first_leNat_iff_exists_le
Proof state before:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat x = true
Tactic:
apply mono hle
Proof state after:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat y = true
Theorem: ENat.first_leNat_iff_exists_le
Proof state before:
case mpr
p : Nat → Bool
x y : Nat
hle : y ≤ x
hy : p y = true
⊢ (first p).leNat y = true
Tactic:
exact first_leNat_of hy
Proof state after:
no goals
Theorem: Nat.pos_of_nonzero
Proof state before:
n : Nat
⊢ n ≠ 0 → n > 0
Tactic:
cases n with
| zero => intro; contradiction
| succ n => intro; exact is_pos _
Proof state after:
no goals
Theorem: Nat.pos_of_nonzero
Proof state before:
case zero

⊢ 0 ≠ 0 → 0 > 0
Tactic:
intro
Proof state after:
case zero
a✝ : 0 ≠ 0
⊢ 0 > 0
Theorem: Nat.pos_of_nonzero
Proof state before:
case zero
a✝ : 0 ≠ 0
⊢ 0 > 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.pos_of_nonzero
Proof state before:
case succ
n : Nat
⊢ n + 1 ≠ 0 → n + 1 > 0
Tactic:
intro
Proof state after:
case succ
n : Nat
a✝ : n + 1 ≠ 0
⊢ n + 1 > 0
Theorem: Nat.pos_of_nonzero
Proof state before:
case succ
n : Nat
a✝ : n + 1 ≠ 0
⊢ n + 1 > 0
Tactic:
exact is_pos _
Proof state after:
no goals
Theorem: List.ext'Iff
Proof state before:
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) ↔ as₁ = as₂
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) → as₁ = as₂

case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Theorem: List.ext'Iff
Proof state before:
case mp
α : Type u_1
as₁ as₂ : List α
⊢ All (as₁.ext'Aux as₂) → as₁ = as₂

case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Tactic:
exact List.ext' as₁ as₂
Proof state after:
case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Theorem: List.ext'Iff
Proof state before:
case mpr
α : Type u_1
as₁ as₂ : List α
⊢ as₁ = as₂ → All (as₁.ext'Aux as₂)
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
as₁ as₂ : List α
h : as₁ = as₂
⊢ All (as₁.ext'Aux as₂)
Theorem: List.ext'Iff
Proof state before:
case mpr
α : Type u_1
as₁ as₂ : List α
h : as₁ = as₂
⊢ All (as₁.ext'Aux as₂)
Tactic:
cases h
Proof state after:
case mpr.refl
α : Type u_1
as₁ : List α
⊢ All (as₁.ext'Aux as₁)
Theorem: List.ext'Iff
Proof state before:
case mpr.refl
α : Type u_1
as₁ : List α
⊢ All (as₁.ext'Aux as₁)
Tactic:
induction as₁ with
| nil => exact All.nil
| cons _ _ H => exact All.cons rfl H
Proof state after:
no goals
Theorem: List.ext'Iff
Proof state before:
case mpr.refl.nil
α : Type u_1
⊢ All ([].ext'Aux [])
Tactic:
exact All.nil
Proof state after:
no goals
Theorem: List.ext'Iff
Proof state before:
case mpr.refl.cons
α : Type u_1
head✝ : α
tail✝ : List α
H : All (tail✝.ext'Aux tail✝)
⊢ All ((head✝ :: tail✝).ext'Aux (head✝ :: tail✝))
Tactic:
exact All.cons rfl H
Proof state after:
no goals
Theorem: List.take_all
Proof state before:
α : Type u_1
as : List α
⊢ take as.length as = as
Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  rw [length_cons]
  rw [take_cons_succ]
  rw [ih]
Proof state after:
no goals
Theorem: List.take_all
Proof state before:
case nil
α : Type u_1
⊢ take [].length [] = []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.take_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take (a :: as).length (a :: as) = a :: as
Tactic:
rw [length_cons]
Proof state after:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take as.length.succ (a :: as) = a :: as
Theorem: List.take_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take as.length.succ (a :: as) = a :: as
Tactic:
rw [take_cons_succ]
Proof state after:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ a :: take as.length as = a :: as
Theorem: List.take_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ a :: take as.length as = a :: as
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.drop_all
Proof state before:
α : Type u_1
as : List α
⊢ drop as.length as = []
Tactic:
induction as with
| nil =>
  rw [drop_nil]
| cons a as ih =>
  rw [length_cons]
  rw [drop_succ_cons]
  rw [ih]
Proof state after:
no goals
Theorem: List.drop_all
Proof state before:
case nil
α : Type u_1
⊢ drop [].length [] = []
Tactic:
rw [drop_nil]
Proof state after:
no goals
Theorem: List.drop_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop (a :: as).length (a :: as) = []
Tactic:
rw [length_cons]
Proof state after:
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop as.length.succ (a :: as) = []
Theorem: List.drop_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop as.length.succ (a :: as) = []
Tactic:
rw [drop_succ_cons]
Proof state after:
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop as.length as = []
Theorem: List.drop_all
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : drop as.length as = []
⊢ drop as.length as = []
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.drop_get
Proof state before:
α : Type u_1
as : List α
n : Nat
hn : n < as.length
⊢ drop n as = as[n] :: drop (n + 1) as
Tactic:
induction as generalizing n with
| nil => absurd hn; exact Nat.not_lt_zero n
| cons a as ih =>
  match n with
  | 0 =>
    rw [drop_succ_cons]
    rw [drop]
    rw [getElem_eq_get]
    rw [get]
    rw [drop]
  | n+1 =>
    rw [drop_succ_cons]
    rw [drop_succ_cons]
    rw [getElem_eq_get]
    rw [get_cons_succ]
    rw [←getElem_eq_get]
    exact ih ..
Proof state after:
no goals
Theorem: List.drop_get
Proof state before:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ drop n [] = [][n] :: drop (n + 1) []
Tactic:
absurd hn
Proof state after:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ ¬n < [].length
Theorem: List.drop_get
Proof state before:
case nil
α : Type u_1
n : Nat
hn : n < [].length
⊢ ¬n < [].length
Tactic:
exact Nat.not_lt_zero n
Proof state after:
no goals
Theorem: List.drop_get
Proof state before:
case cons
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : n < (a :: as).length
⊢ drop n (a :: as) = (a :: as)[n] :: drop (n + 1) (a :: as)
Tactic:
match n with
| 0 =>
  rw [drop_succ_cons]
  rw [drop]
  rw [getElem_eq_get]
  rw [get]
  rw [drop]
| n+1 =>
  rw [drop_succ_cons]
  rw [drop_succ_cons]
  rw [getElem_eq_get]
  rw [get_cons_succ]
  rw [←getElem_eq_get]
  exact ih ..
Proof state after:
no goals
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop (0 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop 0 as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ drop 0 (a :: as) = (a :: as)[0] :: drop 0 as
Tactic:
rw [drop]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as)[0] :: drop 0 as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as)[0] :: drop 0 as
Tactic:
rw [getElem_eq_get]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as).get ⟨0, hn⟩ :: drop 0 as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = (a :: as).get ⟨0, hn⟩ :: drop 0 as
Tactic:
rw [get]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = a :: drop 0 as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n : Nat
hn : 0 < (a :: as).length
⊢ a :: as = a :: drop 0 as
Tactic:
rw [drop]
Proof state after:
no goals
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop (n + 1) (a :: as) = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1 + 1) (a :: as)
Tactic:
rw [drop_succ_cons]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1) as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as)[n + 1] :: drop (n + 1) as
Tactic:
rw [getElem_eq_get]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as).get ⟨n + 1, hn⟩ :: drop (n + 1) as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = (a :: as).get ⟨n + 1, hn⟩ :: drop (n + 1) as
Tactic:
rw [get_cons_succ]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as.get ⟨n, ⋯⟩ :: drop (n + 1) as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as.get ⟨n, ⋯⟩ :: drop (n + 1) as
Tactic:
rw [←getElem_eq_get]
Proof state after:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as[n] :: drop (n + 1) as
Theorem: List.drop_get
Proof state before:
α : Type u_1
a : α
as : List α
ih : ∀ (n : Nat) (hn : n < as.length), drop n as = as[n] :: drop (n + 1) as
n✝ n : Nat
hn : n + 1 < (a :: as).length
⊢ drop n as = as[n] :: drop (n + 1) as
Tactic:
exact ih ..
Proof state after:
no goals
Theorem: HList.append_nil
Proof state before:
case nil
αs : List (Sort u_1)
⊢ nil.append nil ≅ nil
Tactic:
rw [HList.nil_append]
Proof state after:
no goals
Theorem: HList.append_nil
Proof state before:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ (a✝¹ :: a✝).append nil ≅ a✝¹ :: a✝
Tactic:
rw [HList.cons_append]
Proof state after:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ :: a✝.append nil ≅ a✝¹ :: a✝
Theorem: HList.append_nil
Proof state before:
case cons
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ :: a✝.append nil ≅ a✝¹ :: a✝
Tactic:
apply HList.cons_hcongr
Proof state after:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ α✝ = α✝

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ αs✝ ++ [] = αs✝

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ ≅ a✝¹

case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝.append nil ≅ a✝
Theorem: HList.append_nil
Proof state before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ α✝ = α✝
Tactic:
reflexivity
Proof state after:
no goals
Theorem: HList.append_nil
Proof state before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ αs✝ ++ [] = αs✝
Tactic:
rw [List.append_nil]
Proof state after:
no goals
Theorem: HList.append_nil
Proof state before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝¹ ≅ a✝¹
Tactic:
reflexivity using (.≅.)
Proof state after:
no goals
Theorem: HList.append_nil
Proof state before:
case cons.a
αs : List (Sort u_1)
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : a✝.append nil ≅ a✝
⊢ a✝.append nil ≅ a✝
Tactic:
exact ih
Proof state after:
no goals
Theorem: HList.append_assoc
Proof state before:
case nil
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
⊢ (nil.append bs).append cs ≅ nil.append (bs.append cs)
Tactic:
rw [HList.nil_append, HList.nil_append]
Proof state after:
no goals
Theorem: HList.append_assoc
Proof state before:
case cons
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ ((a✝¹ :: a✝).append bs).append cs ≅ (a✝¹ :: a✝).append (bs.append cs)
Tactic:
rw [HList.cons_append, HList.cons_append]
Proof state after:
case cons
αs βs γs : List (Sort u_1)
bs : HList βs
cs : HList γs
α✝ : Sort u_1
αs✝ : List (Sort u_1)
a✝¹ : α✝
a✝ : HList αs✝
ih : (a✝.append bs).append cs ≅ a✝.append (bs.append cs)
⊢ a✝¹ :: (a✝.append bs).append cs ≅ (a✝¹ :: a✝).append (bs.append cs)