internlm/Lean-Github huggingface dataset:
Theorem: Pos.lt_of_mul_lt_mul_right
Proof state before:
x y z : Pos
⊢ x * z < y * z → x < y
Tactic:
by_toNat
Proof state after:
x y z : Pos
⊢ y.toNat * z.toNat > x.toNat * z.toNat → y.toNat > x.toNat
Theorem: Pos.lt_of_mul_lt_mul_right
Proof state before:
x y z : Pos
⊢ y.toNat * z.toNat > x.toNat * z.toNat → y.toNat > x.toNat
Tactic:
exact Nat.lt_of_mul_lt_mul_right
Proof state after:
no goals
Theorem: Pos.mul_lt_mul_of_lt_of_lt
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ < y₁ → x₂ < y₂ → x₁ * x₂ < y₁ * y₂
Tactic:
by_toNat
Proof state after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat * y₂.toNat > x₁.toNat * x₂.toNat
Theorem: Pos.mul_lt_mul_of_lt_of_lt
Proof state before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat > x₁.toNat → y₂.toNat > x₂.toNat → y₁.toNat * y₂.toNat > x₁.toNat * x₂.toNat
Tactic:
exact Nat.mul_lt_mul_of_lt_of_lt
Proof state after:
no goals
Theorem: Pos.pow_le_pow_left
Proof state before:
x y : Nat
⊢ x ≤ y → ∀ (z : Pos), z ^ x ≤ z ^ y
Tactic:
by_toNat
Proof state after:
x y : Nat
⊢ x ≤ y → ∀ (z : Pos), z.toNat ^ y ≥ z.toNat ^ x
Theorem: Pos.pow_le_pow_left
Proof state before:
x y : Nat
⊢ x ≤ y → ∀ (z : Pos), z.toNat ^ y ≥ z.toNat ^ x
Tactic:
intro h z
Proof state after:
x y : Nat
h : x ≤ y
z : Pos
⊢ z.toNat ^ y ≥ z.toNat ^ x
Theorem: Pos.pow_le_pow_left
Proof state before:
x y : Nat
h : x ≤ y
z : Pos
⊢ z.toNat ^ y ≥ z.toNat ^ x
Tactic:
exact Nat.pow_le_pow_of_pos_left h (Nat.zero_lt z.toNat)
Proof state after:
no goals
Theorem: Pos.pow_le_pow_right
Proof state before:
x y : Pos
⊢ x ≤ y → ∀ (z : Nat), x ^ z ≤ y ^ z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Nat), y.toNat ^ z ≥ x.toNat ^ z
Theorem: Pos.pow_le_pow_right
Proof state before:
x y : Pos
⊢ y.toNat ≥ x.toNat → ∀ (z : Nat), y.toNat ^ z ≥ x.toNat ^ z
Tactic:
exact Nat.pow_le_pow_left
Proof state after:
no goals
Theorem: Pos.pow_lt_pow_of_pos_left
Proof state before:
x y : Pos
⊢ x < y → ∀ {z : Nat}, z > 0 → x ^ z < y ^ z
Tactic:
by_toNat
Proof state after:
x y : Pos
⊢ y.toNat > x.toNat → ∀ {z : Nat}, z > 0 → y.toNat ^ z > x.toNat ^ z
Theorem: Pos.pow_lt_pow_of_pos_left
Proof state before:
x y : Pos
⊢ y.toNat > x.toNat → ∀ {z : Nat}, z > 0 → y.toNat ^ z > x.toNat ^ z
Tactic:
exact Nat.pow_lt_pow_of_pos_right
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
x y : Pos
⊢ x < y → ∃ z, x + z = y
Tactic:
intro h
Proof state after:
x y : Pos
h : x < y
⊢ ∃ z, x + z = y
Theorem: Pos.lt.dest
Proof state before:
x y : Pos
h : x < y
⊢ ∃ z, x + z = y
Tactic:
induction x, y with
| one_one =>
  absurd h
  exact Pos.not_lt_one 1
| one_succ y =>
  exists y
  exact Pos.one_add_eq_add_one y
| succ_one x =>
  absurd h
  exact Pos.not_lt_one (x+1)
| succ_succ x y ih =>
  match ih (Pos.lt_of_succ_lt_succ h) with
  | ⟨z, hz⟩ =>
    exists z
    rw [Pos.succ_add, hz]
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
case one_one
h : 1 < 1
⊢ ∃ z, 1 + z = 1
Tactic:
absurd h
Proof state after:
case one_one
h : 1 < 1
⊢ ¬1 < 1
Theorem: Pos.lt.dest
Proof state before:
case one_one
h : 1 < 1
⊢ ¬1 < 1
Tactic:
exact Pos.not_lt_one 1
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ ∃ z, 1 + z = y + 1
Tactic:
exists y
Proof state after:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ 1 + y = y + 1
Theorem: Pos.lt.dest
Proof state before:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ 1 + y = y + 1
Tactic:
exact Pos.one_add_eq_add_one y
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ∃ z, x + 1 + z = 1
Tactic:
absurd h
Proof state after:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ¬x + 1 < 1
Theorem: Pos.lt.dest
Proof state before:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ¬x + 1 < 1
Tactic:
exact Pos.not_lt_one (x+1)
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
case succ_succ
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
⊢ ∃ z, x + 1 + z = y + 1
Tactic:
match ih (Pos.lt_of_succ_lt_succ h) with
| ⟨z, hz⟩ =>
  exists z
  rw [Pos.succ_add, hz]
Proof state after:
no goals
Theorem: Pos.lt.dest
Proof state before:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ ∃ z, x + 1 + z = y + 1
Tactic:
exists z
Proof state after:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ x + 1 + z = y + 1
Theorem: Pos.lt.dest
Proof state before:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ x + 1 + z = y + 1
Tactic:
rw [Pos.succ_add, hz]
Proof state after:
no goals
Theorem: Pos.lt.intro
Proof state before:
x y z : Pos
⊢ x + z = y → x < y
Tactic:
intro h
Proof state after:
x y z : Pos
h : x + z = y
⊢ x < y
Theorem: Pos.lt.intro
Proof state before:
x y z : Pos
h : x + z = y
⊢ x < y
Tactic:
rw [←h]
Proof state after:
x y z : Pos
h : x + z = y
⊢ x < x + z
Theorem: Pos.lt.intro
Proof state before:
x y z : Pos
h : x + z = y
⊢ x < x + z
Tactic:
exact Pos.lt_add_right x z
Proof state after:
no goals
Theorem: List.extract_stop
Proof state before:
α : Type u_1
as : List α
stop : Nat
⊢ as.extract stop stop = []
Tactic:
unfold extract
Proof state after:
α : Type u_1
as : List α
stop : Nat
⊢ take (stop - stop) (drop stop as) = []
Theorem: List.extract_stop
Proof state before:
α : Type u_1
as : List α
stop : Nat
⊢ take (stop - stop) (drop stop as) = []
Tactic:
rw [Nat.sub_self]
Proof state after:
α : Type u_1
as : List α
stop : Nat
⊢ take 0 (drop stop as) = []
Theorem: List.extract_stop
Proof state before:
α : Type u_1
as : List α
stop : Nat
⊢ take 0 (drop stop as) = []
Tactic:
rw [take_zero]
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ as.extract start stop = as.get ⟨start, ⋯⟩ :: as.extract (start + 1) stop
Tactic:
unfold extract
Proof state after:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Theorem: List.extract_step
Proof state before:
α : Type u_1
as : List α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Tactic:
induction start, stop using Nat.recDiag generalizing as with
| zero_zero => contradiction
| succ_zero start => contradiction
| zero_succ stop => match as with | a :: as => simp
| succ_succ start stop ih =>
  match as with
  | a :: as =>
    simp
    rw [ih]
    exact Nat.lt_of_succ_lt_succ hstart
    exact Nat.le_of_succ_le_succ hstop
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
case zero_zero
α : Type u_1
as : List α
hstart : 0 < 0
hstop : 0 ≤ as.length
⊢ take (0 - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (0 - (0 + 1)) (drop (0 + 1) as)
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
case succ_zero
α : Type u_1
start : Nat
a✝ :
  ∀ (as : List α) (hstart : start < 0) (hstop : 0 ≤ as.length),
    take (0 - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (0 - (start + 1)) (drop (start + 1) as)
as : List α
hstart : start + 1 < 0
hstop : 0 ≤ as.length
⊢ take (0 - (start + 1)) (drop (start + 1) as) =
    as.get ⟨start + 1, ⋯⟩ :: take (0 - (start + 1 + 1)) (drop (start + 1 + 1) as)
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
case zero_succ
α : Type u_1
stop : Nat
a✝ :
  ∀ (as : List α) (hstart : 0 < stop) (hstop : stop ≤ as.length),
    take (stop - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop - (0 + 1)) (drop (0 + 1) as)
as : List α
hstart : 0 < stop + 1
hstop : stop + 1 ≤ as.length
⊢ take (stop + 1 - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop + 1 - (0 + 1)) (drop (0 + 1) as)
Tactic:
match as with | a :: as => simp
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
α : Type u_1
stop : Nat
a✝ :
  ∀ (as : List α) (hstart : 0 < stop) (hstop : stop ≤ as.length),
    take (stop - 0) (drop 0 as) = as.get ⟨0, ⋯⟩ :: take (stop - (0 + 1)) (drop (0 + 1) as)
as✝ : List α
hstart : 0 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop + 1 - 0) (drop 0 (a :: as)) = (a :: as).get ⟨0, ⋯⟩ :: take (stop + 1 - (0 + 1)) (drop (0 + 1) (a :: as))
Tactic:
simp
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
case succ_succ
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as : List α
hstart : start + 1 < stop + 1
hstop : stop + 1 ≤ as.length
⊢ take (stop + 1 - (start + 1)) (drop (start + 1) as) =
    as.get ⟨start + 1, ⋯⟩ :: take (stop + 1 - (start + 1 + 1)) (drop (start + 1 + 1) as)
Tactic:
match as with
| a :: as =>
  simp
  rw [ih]
  exact Nat.lt_of_succ_lt_succ hstart
  exact Nat.le_of_succ_le_succ hstop
Proof state after:
no goals
Theorem: List.extract_step
Proof state before:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop + 1 - (start + 1)) (drop (start + 1) (a :: as)) =
    (a :: as).get ⟨start + 1, ⋯⟩ :: take (stop + 1 - (start + 1 + 1)) (drop (start + 1 + 1) (a :: as))
Tactic:
simp
Proof state after:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Theorem: List.extract_step
Proof state before:
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
Tactic:
rw [ih]
Proof state after:
case hstart
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ start < stop

case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Theorem: List.extract_step
Proof state before:
case hstart
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ start < stop

case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Tactic:
exact Nat.lt_of_succ_lt_succ hstart
Proof state after:
case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Theorem: List.extract_step
Proof state before:
case hstop
α : Type u_1
start stop : Nat
ih :
  ∀ (as : List α) (hstart : start < stop) (hstop : stop ≤ as.length),
    take (stop - start) (drop start as) = as.get ⟨start, ⋯⟩ :: take (stop - (start + 1)) (drop (start + 1) as)
as✝ : List α
hstart : start + 1 < stop + 1
a : α
as : List α
hstop : stop + 1 ≤ (a :: as).length
⊢ stop ≤ as.length
Tactic:
exact Nat.le_of_succ_le_succ hstop
Proof state after:
no goals
Theorem: List.extract_all
Proof state before:
α : Type u_1
as : List α
⊢ as.extract 0 as.length = as
Tactic:
unfold extract
Proof state after:
α : Type u_1
as : List α
⊢ take (as.length - 0) (drop 0 as) = as
Theorem: List.extract_all
Proof state before:
α : Type u_1
as : List α
⊢ take (as.length - 0) (drop 0 as) = as
Tactic:
rw [Nat.sub_zero]
Proof state after:
α : Type u_1
as : List α
⊢ take as.length (drop 0 as) = as
Theorem: List.extract_all
Proof state before:
α : Type u_1
as : List α
⊢ take as.length (drop 0 as) = as
Tactic:
rw [List.drop]
Proof state after:
α : Type u_1
as : List α
⊢ take as.length as = as
Theorem: List.extract_all
Proof state before:
α : Type u_1
as : List α
⊢ take as.length as = as
Tactic:
rw [take_length]
Proof state after:
no goals
Theorem: List.pure_bind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
a : α
⊢ [a].bind f = f a
Tactic:
rw [cons_bind, nil_bind, append_nil]
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → List β
g : β → List γ
as : List α
⊢ (as.bind f).bind g = as.bind fun a => (f a).bind g
Tactic:
induction as with
| nil => rfl
| cons a as H => rw [cons_bind, cons_bind, append_bind, H]
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → List β
g : β → List γ
⊢ ([].bind f).bind g = [].bind fun a => (f a).bind g
Tactic:
rfl
Proof state after:
no goals
Theorem: List.bind_assoc
Proof state before:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → List β
g : β → List γ
a : α
as : List α
H : (as.bind f).bind g = as.bind fun a => (f a).bind g
⊢ ((a :: as).bind f).bind g = (a :: as).bind fun a => (f a).bind g
Tactic:
rw [cons_bind, cons_bind, append_bind, H]
Proof state after:
no goals
Theorem: List.Index.option_eq_iff_eq_unoption
Proof state before:
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
⊢ option i = k ↔ i = k.unoption
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
⊢ option i = k → i = k.unoption

case mpr
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
⊢ i = k.unoption → option i = k
Theorem: List.Index.option_eq_iff_eq_unoption
Proof state before:
case mp
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
⊢ option i = k → i = k.unoption
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
h : option i = k
⊢ i = k.unoption
Theorem: List.Index.option_eq_iff_eq_unoption
Proof state before:
case mp
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
h : option i = k
⊢ i = k.unoption
Tactic:
rw [←h, unoption_option]
Proof state after:
no goals
Theorem: List.Index.option_eq_iff_eq_unoption
Proof state before:
case mpr
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
⊢ i = k.unoption → option i = k
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
h : i = k.unoption
⊢ option i = k
Theorem: List.Index.option_eq_iff_eq_unoption
Proof state before:
case mpr
α✝ : Type u_1
xs : List α✝
i : Option xs.Index
k : xs.option.Index
h : i = k.unoption
⊢ option i = k
Tactic:
rw [h, option_unoption]
Proof state after:
no goals
Theorem: List.Index.unoption_eq_iff_eq_option
Proof state before:
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i ↔ k = option i
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i → k = option i

case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k = option i → k.unoption = i
Theorem: List.Index.unoption_eq_iff_eq_option
Proof state before:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i → k = option i
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k.unoption = i
⊢ k = option i
Theorem: List.Index.unoption_eq_iff_eq_option
Proof state before:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k.unoption = i
⊢ k = option i
Tactic:
rw [←h, option_unoption]
Proof state after:
no goals
Theorem: List.Index.unoption_eq_iff_eq_option
Proof state before:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k = option i → k.unoption = i
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k = option i
⊢ k.unoption = i
Theorem: List.Index.unoption_eq_iff_eq_option
Proof state before:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k = option i
⊢ k.unoption = i
Tactic:
rw [h, unoption_option]
Proof state after:
no goals
Theorem: List.Index.val_option
Proof state before:
α : Type u_1
xs : List α
i : Option xs.Index
⊢ (match i with
    | none => none
    | some i => some i.val) =
    (option i).val
Tactic:
match i with
| none => rfl
| some i => rw [option, val_map]
Proof state after:
no goals
Theorem: List.Index.val_option
Proof state before:
α : Type u_1
xs : List α
i : Option xs.Index
⊢ (match none with
    | none => none
    | some i => some i.val) =
    (option none).val
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.val_option
Proof state before:
α : Type u_1
xs : List α
i✝ : Option xs.Index
i : xs.Index
⊢ (match some i with
    | none => none
    | some i => some i.val) =
    (option (some i)).val
Tactic:
rw [option, val_map]
Proof state after:
no goals
Theorem: List.Index.val_unoption
Proof state before:
α : Type u_1
xs : List α
k : xs.option.Index
⊢ k.val =
    match k.unoption with
    | none => none
    | some k => some k.val
Tactic:
rw [←option_unoption k, val_option, unoption_option]
Proof state after:
no goals
Theorem: List.Index.unbind_bind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
i : xs.Index
j : (f i.val).Index
⊢ unbind f (bind f ⟨i, j⟩) = ⟨i, j⟩
Tactic:
induction i with simp only [bind, unbind, unappend_append]
| tail _ ih => rw [ih]
Proof state after:
no goals
Theorem: List.Index.unbind_bind
Proof state before:
case tail
α : Type u_1
β : Type u_2
f : α → List β
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : ∀ (j : (f a✝.val).Index), unbind f (bind f ⟨a✝, j⟩) = ⟨a✝, j⟩
j : (f a✝.tail.val).Index
⊢ ⟨(unbind f (bind f ⟨a✝, j⟩)).fst.tail, (unbind f (bind f ⟨a✝, j⟩)).snd⟩ = ⟨a✝.tail, j⟩
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.Index.bind_unbind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
k : (xs.bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  rw [unbind]
  split
  next h => rw [bind, append_inl, ←h, append_unappend]
  next h => rw [bind, append_inr, ih, ←h, append_unappend]
Proof state after:
no goals
Theorem: List.Index.bind_unbind
Proof state before:
case nil
α : Type u_1
β : Type u_2
f : α → List β
k : ([].bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.bind_unbind
Proof state before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f (unbind f k) = k
Tactic:
rw [unbind]
Proof state after:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f
      (match k.unappend with
      | Sum.inl j => ⟨head, j⟩
      | Sum.inr k => ⟨(unbind f k).fst.tail, (unbind f k).snd⟩) =
    k
Theorem: List.Index.bind_unbind
Proof state before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
⊢ bind f
      (match k.unappend with
      | Sum.inl j => ⟨head, j⟩
      | Sum.inr k => ⟨(unbind f k).fst.tail, (unbind f k).snd⟩) =
    k
Tactic:
split
Proof state after:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
heq✝ : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k

case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Theorem: List.Index.bind_unbind
Proof state before:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
heq✝ : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k

case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
next h => rw [bind, append_inl, ←h, append_unappend]
Proof state after:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Theorem: List.Index.bind_unbind
Proof state before:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
heq✝ : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
next h => rw [bind, append_inr, ih, ←h, append_unappend]
Proof state after:
no goals
Theorem: List.Index.bind_unbind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
j✝ : (f x).Index
h : k.unappend = Sum.inl j✝
⊢ bind f ⟨head, j✝⟩ = k
Tactic:
rw [bind, append_inl, ←h, append_unappend]
Proof state after:
no goals
Theorem: List.Index.bind_unbind
Proof state before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (k : (xs.bind f).Index), bind f (unbind f k) = k
k : ((x :: xs).bind f).Index
x✝ : (f x).Index ⊕ (map f xs).join.Index
k✝ : (map f xs).join.Index
h : k.unappend = Sum.inr k✝
⊢ bind f ⟨(unbind f k✝).fst.tail, (unbind f k✝).snd⟩ = k
Tactic:
rw [bind, append_inr, ih, ←h, append_unappend]
Proof state after:
no goals