internlm/Lean-Github huggingface dataset:
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
n : Nat
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init n
Tactic:
induction n generalizing f init
Proof state after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
n✝ : Nat
n_ih✝ : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n✝
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n✝)
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n)
Tactic:
case succ n h_ind =>
  rw [foldAllM_succ]; dsimp
  have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
    funext fun x => rfl
  conv => lhs; rhs; rw [this]; ext x; rw [h_ind]
  conv => rhs; rw [Nat.foldM_succ]
Proof state after:
no goals
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ foldAllM (f ∘ val) init = Nat.foldM f init (Nat.succ n)
Tactic:
rw [foldAllM_succ]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ (f ∘ val) 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ (f ∘ val) 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
dsimp
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
have : (f ∘ Fin.val (n:=n+1)) ∘ Fin.succ = (f ∘ Nat.succ) ∘ Fin.val :=
  funext fun x => rfl
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ f 0 init >>= foldAllM ((f ∘ val) ∘ succ) = Nat.foldM f init (Nat.succ n)
Tactic:
conv => lhs; rhs; rw [this]; ext x; rw [h_ind]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ (do
      let x ← f 0 init
      Nat.foldM (f ∘ Nat.succ) x n) =
    Nat.foldM f init (Nat.succ n)
Theorem: Fin.foldAllM_comp_val
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
h_ind : ∀ {f : Nat → α → m α} {init : α}, foldAllM (f ∘ val) init = Nat.foldM f init n
f : Nat → α → m α
init : α
this : (f ∘ val) ∘ succ = (f ∘ Nat.succ) ∘ val
⊢ (do
      let x ← f 0 init
      Nat.foldM (f ∘ Nat.succ) x n) =
    Nat.foldM f init (Nat.succ n)
Tactic:
conv => rhs; rw [Nat.foldM_succ]
Proof state after:
no goals
Theorem: Fin.foldAll_comp_val
Proof state before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ foldAll (f ∘ val) init = Nat.fold f n init
Tactic:
unfold foldAll
Proof state after:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (foldAllM (f ∘ val) init) = Nat.fold f n init
Theorem: Fin.foldAll_comp_val
Proof state before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (foldAllM (f ∘ val) init) = Nat.fold f n init
Tactic:
rw [Nat.fold_eq_foldM, foldAllM_comp_val]
Proof state after:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (Nat.foldM f init n) = Nat.foldM f init n
Theorem: Fin.foldAll_comp_val
Proof state before:
n : Nat
α : Type u
f : Nat → α → α
init : α
⊢ Id.run (Nat.foldM f init n) = Nat.foldM f init n
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAll_induction
Proof state before:
n : Nat
α : Type u
motive : Nat → α → Prop
f : Fin n → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive n (foldAll f init)
Tactic:
induction n generalizing init with
| zero => exact h0
| succ n IH =>
  dsimp [foldAll]
  rw [Fin.foldAllM_succ' (m:=Id)]
  refine hf ⟨n,n.lt_succ_self⟩ _ ?_
  refine IH _ init h0 ?_
  intro i x H
  exact hf ⟨i.1, .step i.2⟩ x H
Proof state after:
no goals
Theorem: Fin.foldAll_induction
Proof state before:
case zero
α : Type u
motive : Nat → α → Prop
f : Fin Nat.zero → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin Nat.zero) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive Nat.zero (foldAll f init)
Tactic:
exact h0
Proof state after:
no goals
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (foldAll f init)
Tactic:
dsimp [foldAll]
Proof state after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM f init))
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM f init))
Tactic:
rw [Fin.foldAllM_succ' (m:=Id)]
Proof state after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM (f ∘ castSucc) init >>= f { val := n, isLt := (_ : n < Nat.succ n) }))
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (Nat.succ n) (Id.run (foldAllM (f ∘ castSucc) init >>= f { val := n, isLt := (_ : n < Nat.succ n) }))
Tactic:
refine hf ⟨n,n.lt_succ_self⟩ _ ?_
Proof state after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (↑{ val := n, isLt := (_ : n < Nat.succ n) }) (foldAllM (f ∘ castSucc) init)
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive (↑{ val := n, isLt := (_ : n < Nat.succ n) }) (foldAllM (f ∘ castSucc) init)
Tactic:
refine IH _ init h0 ?_
Proof state after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) ((f ∘ castSucc) i x)
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ ∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) ((f ∘ castSucc) i x)
Tactic:
intro i x H
Proof state after:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
i : Fin n
x : α
H : motive (↑i) x
⊢ motive (↑i + 1) ((f ∘ castSucc) i x)
Theorem: Fin.foldAll_induction
Proof state before:
case succ
α : Type u
motive : Nat → α → Prop
n : Nat
IH :
  ∀ (f : Fin n → α → α) (init : α),
    motive 0 init → (∀ (i : Fin n) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)) → motive n (foldAll f init)
f : Fin (Nat.succ n) → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin (Nat.succ n)) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
i : Fin n
x : α
H : motive (↑i) x
⊢ motive (↑i + 1) ((f ∘ castSucc) i x)
Tactic:
exact hf ⟨i.1, .step i.2⟩ x H
Proof state after:
no goals
Theorem: Fin.length_elementList
Proof state before:
n : Nat
⊢ List.length (Fin.elementList n) = n
Tactic:
induction n
Proof state after:
case zero

⊢ List.length (Fin.elementList Nat.zero) = Nat.zero

case succ
n✝ : Nat
n_ih✝ : List.length (Fin.elementList n✝) = n✝
⊢ List.length (Fin.elementList (Nat.succ n✝)) = Nat.succ n✝
Theorem: Fin.length_elementList
Proof state before:
⊢ List.length (Fin.elementList Nat.zero) = Nat.zero
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Fin.length_elementList
Proof state before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
Tactic:
case succ n h_ind => unfold Fin.elementList; unfold List.length; rw [List.length_map, h_ind]
Proof state after:
no goals
Theorem: Fin.length_elementList
Proof state before:
⊢ List.length (Fin.elementList Nat.zero) = Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.length_elementList
Proof state before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length (Fin.elementList (Nat.succ n)) = Nat.succ n
Tactic:
unfold Fin.elementList
Proof state after:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
      ({ val := 0, isLt := (_ : 0 < Nat.succ n) } ::
        List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) =
    Nat.succ n
Theorem: Fin.length_elementList
Proof state before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
      ({ val := 0, isLt := (_ : 0 < Nat.succ n) } ::
        List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) =
    Nat.succ n
Tactic:
unfold List.length
Proof state after:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
        (List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) +
      1 =
    Nat.succ n
Theorem: Fin.length_elementList
Proof state before:
n : Nat
h_ind : List.length (Fin.elementList n) = n
⊢ List.length
        (List.map
          (fun x =>
            match x with
            | { val := i, isLt := h } => { val := i + 1, isLt := (_ : Nat.succ i < Nat.succ n) })
          (Fin.elementList n)) +
      1 =
    Nat.succ n
Tactic:
rw [List.length_map, h_ind]
Proof state after:
no goals
Theorem: KVChain.eq_of_toList_eq
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend : List.Ascending (Sigma.relOnFst r) xs
ys : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) ys
h : { toList := xs, ascend := xascend }.toList = { toList := ys, ascend := ascend✝ }.toList
⊢ { toList := xs, ascend := xascend } = { toList := ys, ascend := ascend✝ }
Tactic:
cases h
Proof state after:
case refl
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ { toList := xs, ascend := xascend } = { toList := xs, ascend := ascend✝ }
Theorem: KVChain.eq_of_toList_eq
Proof state before:
case refl
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ { toList := xs, ascend := xascend } = { toList := xs, ascend := ascend✝ }
Tactic:
rw [proofIrrel xascend _]
Proof state after:
no goals
Theorem: KVChain.cons_hingeable
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
a : α
b : β a
xs : KVChain (flip r) β
haxs : boundLeft a xs
ys : KVChain r β
⊢ hingeable (KVChain.cons a b xs haxs) ys = boundLeft a ys
Tactic:
unfold hingeable
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
a : α
b : β a
xs : KVChain (flip r) β
haxs : boundLeft a xs
ys : KVChain r β
⊢ List.relHead (Sigma.relOnFst r) (KVChain.cons a b xs haxs).toList ys.toList = boundLeft a ys
Theorem: KVChain.cons_hingeable
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
a : α
b : β a
xs : KVChain (flip r) β
haxs : boundLeft a xs
ys : KVChain r β
⊢ List.relHead (Sigma.relOnFst r) (KVChain.cons a b xs haxs).toList ys.toList = boundLeft a ys
Tactic:
rw [List.relHead_cons_left]
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
a : α
b : β a
xs : KVChain (flip r) β
haxs : boundLeft a xs
ys : KVChain r β
⊢ List.predHead (Sigma.relOnFst r { fst := a, snd := b }) ys.toList = boundLeft a ys
Theorem: KVChain.cons_hingeable
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
a : α
b : β a
xs : KVChain (flip r) β
haxs : boundLeft a xs
ys : KVChain r β
⊢ List.predHead (Sigma.relOnFst r { fst := a, snd := b }) ys.toList = boundLeft a ys
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.hingeable_cons
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ hingeable xs (KVChain.cons a b ys hay) = boundLeft a xs
Tactic:
unfold hingeable
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.relHead (Sigma.relOnFst r) xs.toList (KVChain.cons a b ys hay).toList = boundLeft a xs
Theorem: KVChain.hingeable_cons
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.relHead (Sigma.relOnFst r) xs.toList (KVChain.cons a b ys hay).toList = boundLeft a xs
Tactic:
rw [List.relHead_cons_right]
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.predHead (fun a_1 => Sigma.relOnFst r a_1 { fst := a, snd := b }) xs.toList = boundLeft a xs
Theorem: KVChain.hingeable_cons
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hay : boundLeft a ys
⊢ List.predHead (fun a_1 => Sigma.relOnFst r a_1 { fst := a, snd := b }) xs.toList = boundLeft a xs
Tactic:
rfl
Proof state after:
no goals
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ hingeable (KVChain.cons a₁ x✝³ x✝² x✝¹) (KVChain.cons a b ys hays) → hingeable (KVChain.cons a₁ x✝³ x✝² x✝¹) ys
Tactic:
rw [cons_hingeable, cons_hingeable]
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ boundLeft a₁ (KVChain.cons a b ys hays) → boundLeft a₁ ys
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ boundLeft a₁ (KVChain.cons a b ys hays) → boundLeft a₁ ys
Tactic:
dsimp [boundLeft, List.predHead]
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
dsimp [boundLeft, List.predHead] at hays
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
cases hys : ys.toList
Proof state after:
case nil
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst

case cons
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
case nil => intros; exact True.intro
Proof state after:
no goals
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hys : ys.toList = head✝ :: tail✝
⊢ r a₁ a →
    match head✝ :: tail✝ with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
case cons => intro h; rw [hys] at hays; exact trans (t:=r) h hays
Proof state after:
no goals
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
⊢ r a₁ a →
    match [] with
    | [] => True
    | a :: tail => r a₁ a.fst
Tactic:
intros
Proof state after:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
a✝ : r a₁ a
⊢ match [] with
  | [] => True
  | a :: tail => r a₁ a.fst
Theorem: KVChain.hingeable_skip_right
Proof state before:
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
hys : ys.toList = []
a✝ : r a₁ a
⊢ match [] with
  | [] => True
  | a :: tail => r a₁ a.fst
Tactic:
exact True.intro
Proof state after:
no goals