internlm/Lean-Github huggingface dataset:
Theorem: List.forAllRel_flip
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
bs : List β
a : α
as : List α
h_ind : List.forAllRel (flip r) bs as = List.forAllRel r as bs
⊢ forAll (fun x => flip r x a) bs ∧ List.forAllRel r as bs ↔ forAll (r a) bs ∧ List.forAllRel r as bs
Tactic:
exact and_congr Iff.rfl Iff.rfl
Proof state after:
no goals
Theorem: List.forAllRel_reverse_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel r (reverse as) bs = List.forAllRel r as bs
Tactic:
induction bs generalizing as <;> simp
Proof state after:
case cons
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
Theorem: List.forAllRel_reverse_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
case cons _ _ h_ind =>
  rw [h_ind]; intros; exact Iff.rfl
Proof state after:
no goals
Theorem: List.forAllRel_reverse_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r (reverse as) tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
rw [h_ind]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝)
Theorem: List.forAllRel_reverse_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
⊢ forAll (fun x => r x head✝) as → (List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝)
Tactic:
intros
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
a✝ : forAll (fun x => r x head✝) as
⊢ List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝
Theorem: List.forAllRel_reverse_left
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
head✝ : β
tail✝ : List β
h_ind : ∀ {as : List α}, List.forAllRel r (reverse as) tail✝ = List.forAllRel r as tail✝
as : List α
a✝ : forAll (fun x => r x head✝) as
⊢ List.forAllRel r as tail✝ ↔ List.forAllRel r as tail✝
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: List.forAllRel_reverse_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel r as (reverse bs) = List.forAllRel r as bs
Tactic:
rw [←forAllRel_flip, ←forAllRel_flip (r:=r)]
Proof state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) (reverse bs) as = List.forAllRel (flip r) bs as
Theorem: List.forAllRel_reverse_right
Proof state before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) (reverse bs) as = List.forAllRel (flip r) bs as
Tactic:
exact forAllRel_reverse_left
Proof state after:
no goals
Theorem: and_decideEq
Proof state before:
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ (f a && decide (a = b)) = (f b && decide (a = b))
Tactic:
apply Decidable.byCases (p:=a=b) <;> (intro h; simp [h])
Proof state after:
no goals
Theorem: and_decideEq
Proof state before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ ¬a = b → (f a && decide (a = b)) = (f b && decide (a = b))
Tactic:
intro h
Proof state after:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (f a && decide (a = b)) = (f b && decide (a = b))
Theorem: and_decideEq
Proof state before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (f a && decide (a = b)) = (f b && decide (a = b))
Tactic:
simp [h]
Proof state after:
no goals
Theorem: decideEq_and
Proof state before:
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
apply Decidable.byCases (p:=a=b) <;> (intro h; simp [h])
Proof state after:
no goals
Theorem: decideEq_and
Proof state before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
⊢ ¬a = b → (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
intro h
Proof state after:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)
Theorem: decideEq_and
Proof state before:
case h2
α : Sort u
inst✝ : DecidableEq α
f : α → Bool
a b : α
h : ¬a = b
⊢ (decide (a = b) && f a) = (decide (a = b) && f b)
Tactic:
simp [h]
Proof state after:
no goals
Theorem: decide_and_decide
Proof state before:
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ (decide p && decide q) = decide (p ∧ q)
Tactic:
apply Decidable.byCases (p:=p) <;> apply Decidable.byCases (p:=q)
<;> (intro hq hp; simp [hp,hq])
Proof state after:
no goals
Theorem: decide_and_decide
Proof state before:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ ¬q → ¬p → (decide p && decide q) = decide (p ∧ q)
Tactic:
intro hq hp
Proof state after:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
hq : ¬q
hp : ¬p
⊢ (decide p && decide q) = decide (p ∧ q)
Theorem: decide_and_decide
Proof state before:
case h2.h2
α : Sort u
inst✝² : DecidableEq α
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
hq : ¬q
hp : ¬p
⊢ (decide p && decide q) = decide (p ∧ q)
Tactic:
simp [hp,hq]
Proof state after:
no goals
Theorem: Bool.and_comm
Proof state before:
a b : Bool
⊢ (a && b) = (b && a)
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.bne_and
Proof state before:
a b c : Bool
⊢ (a != b && c) = ((a && c) != (b && c))
Tactic:
cases a <;> cases b <;> cases c <;> decide
Proof state after:
no goals
Theorem: Bool.and_bne
Proof state before:
a b c : Bool
⊢ (a && b != c) = ((a && b) != (a && c))
Tactic:
cases a <;> cases b <;> cases c <;> decide
Proof state after:
no goals
Theorem: Fin.lexfold_inj
Proof state before:
m n : Nat
x₁ x₂ : Fin m
y₁ y₂ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₂
this : y₁ = y₂
⊢ x₁ = x₂ ∧ y₁ = y₂
Tactic:
cases this
Proof state after:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
⊢ x₁ = x₂ ∧ y₁ = y₁
Theorem: Fin.lexfold_inj
Proof state before:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
⊢ x₁ = x₂ ∧ y₁ = y₁
Tactic:
have : 0 < n := trans y₁.val.zero_le y₁.isLt
Proof state after:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
this : 0 < n
⊢ x₁ = x₂ ∧ y₁ = y₁
Theorem: Fin.lexfold_inj
Proof state before:
case refl
m n : Nat
x₁ x₂ : Fin m
y₁ : Fin n
h : ↑x₁ * n + ↑y₁ = ↑x₂ * n + ↑y₁
this✝ : 0 < n
this : x₁ = x₂
⊢ x₁ = x₂ ∧ y₁ = y₁
Tactic:
exact ⟨this, rfl⟩
Proof state after:
no goals
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
k : Nat
h : i + (k + 1) = n + 1
⊢ loop f i a (k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b k (_ : i + k = n)
Tactic:
induction k generalizing n f i a
Proof state after:
case zero
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ loop f i a (Nat.zero + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b Nat.zero (_ : i + Nat.zero = n)

case succ
m : Type u → Type v
inst✝ : Monad m
α : Type u
n✝ : Nat
n_ih✝ :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (n✝ + 1) = n + 1},
    loop f i a (n✝ + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b n✝ (_ : i + n✝ = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ n✝ + 1) = n + 1
⊢ loop f i a (Nat.succ n✝ + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ n✝) (_ : i + Nat.succ n✝ = n)
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ loop f i a (Nat.zero + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b Nat.zero (_ : i + Nat.zero = n)
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ loop f i a (Nat.succ k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
case succ k h_ind =>
  conv =>
    lhs
    change do loop f i.succ (← f ⟨i, h ▸ Nat.lt_add_of_pos_right k.succ.zero_lt_succ⟩ a) k.succ (by rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]; rfl)
  apply bind_congr; intro b
  rw [h_ind]
  rfl
Proof state after:
no goals
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ loop f i a (Nat.zero + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b Nat.zero (_ : i + Nat.zero = n)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ loop f i a (Nat.succ k + 1) h = do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
conv =>
  lhs
  change do loop f i.succ (← f ⟨i, h ▸ Nat.lt_add_of_pos_right k.succ.zero_lt_succ⟩ a) k.succ (by rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]; rfl)
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      loop f (Nat.succ i) __do_lift (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1)) =
    do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      loop f (Nat.succ i) __do_lift (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1)) =
    do
    let b ← f { val := i, isLt := (_ : i < n + 1) } a
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
apply bind_congr
Proof state after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ ∀ (a : α),
    loop f (Nat.succ i) a (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
      loop (f ∘ succ) i a (Nat.succ k) (_ : i + Nat.succ k = n)
Theorem: Fin.foldAllM.loop_succ
Proof state before:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ ∀ (a : α),
    loop f (Nat.succ i) a (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
      loop (f ∘ succ) i a (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
intro b
Proof state after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ loop f (Nat.succ i) b (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Theorem: Fin.foldAllM.loop_succ
Proof state before:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ loop f (Nat.succ i) b (Nat.succ k) (_ : Nat.succ i + Nat.succ k = n + 1) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
rw [h_ind]
Proof state after:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ (do
      let b ← f { val := Nat.succ i, isLt := (_ : Nat.succ i < n + 1) } b
      loop (f ∘ succ) (Nat.succ i) b k (_ : Nat.succ i + k = n)) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Theorem: Fin.foldAllM.loop_succ
Proof state before:
case h
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
b : α
⊢ (do
      let b ← f { val := Nat.succ i, isLt := (_ : Nat.succ i < n + 1) } b
      loop (f ∘ succ) (Nat.succ i) b k (_ : Nat.succ i + k = n)) =
    loop (f ∘ succ) i b (Nat.succ k) (_ : i + Nat.succ k = n)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ Nat.succ i + Nat.succ k = n + 1
Tactic:
rw [←h, Nat.add_succ, Nat.succ_add, Nat.add_succ]
Proof state after:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ Nat.succ (Nat.succ (i + k)) = Nat.succ (i + (k + 1))
Theorem: Fin.foldAllM.loop_succ
Proof state before:
m : Type u → Type v
inst✝ : Monad m
α : Type u
k : Nat
h_ind :
  ∀ {n : Nat} {f : Fin (n + 1) → α → m α} {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    loop f i a (k + 1) h = do
      let b ← f { val := i, isLt := (_ : i < n + 1) } a
      loop (f ∘ succ) i b k (_ : i + k = n)
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ Nat.succ (Nat.succ (i + k)) = Nat.succ (i + (k + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
k : Nat
h : i + (k + 1) = n + 1
⊢ foldAllM.loop f i a (k + 1) h =
    foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
induction k generalizing a i with
| zero => dsimp [Fin.foldAllM.loop]; cases h; simp only [pure_bind, bind_pure]
| succ k IH =>
  conv =>
    lhs; unfold Fin.foldAllM.loop; dsimp
    rhs; ext; rw [@IH (i+1) _ (i.succ_add (k+1) ▸ h)]
  simp only [← bind_assoc]
  rfl
Proof state after:
no goals
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ foldAllM.loop f i a (Nat.zero + 1) h =
    foldAllM.loop (f ∘ castSucc) i a Nat.zero (_ : i + Nat.zero = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
dsimp [Fin.foldAllM.loop]
Proof state after:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case zero
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
i : Nat
a : α
h : i + (Nat.zero + 1) = n + 1
⊢ (do
      let __do_lift ← f { val := i, isLt := (_ : i < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
cases h
Proof state after:
case zero.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
a : α
⊢ (do
      let __do_lift ← f { val := n, isLt := (_ : n < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case zero.refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
a : α
⊢ (do
      let __do_lift ← f { val := n, isLt := (_ : n < n + 1) } a
      pure __do_lift) =
    pure a >>= f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
simp only [pure_bind, bind_pure]
Proof state after:
no goals
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ foldAllM.loop f i a (Nat.succ k + 1) h =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
conv =>
  lhs; unfold Fin.foldAllM.loop; dsimp
  rhs; ext; rw [@IH (i+1) _ (i.succ_add (k+1) ▸ h)]
Proof state after:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (f { val := i, isLt := (_ : i < n + 1) } a >>= fun x =>
      foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }) =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (f { val := i, isLt := (_ : i < n + 1) } a >>= fun x =>
      foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }) =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
simp only [← bind_assoc]
Proof state after:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
        let x ← f { val := i, isLt := (_ : i < n + 1) } a
        foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n)) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) } =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Theorem: Fin.foldAllM_loop_succ'
Proof state before:
case succ
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
n : Nat
f : Fin (n + 1) → α → m α
k : Nat
IH :
  ∀ {i : Nat} {a : α} {h : i + (k + 1) = n + 1},
    foldAllM.loop f i a (k + 1) h =
      foldAllM.loop (f ∘ castSucc) i a k (_ : i + k = n) >>= f { val := n, isLt := (_ : n < Nat.succ n) }
i : Nat
a : α
h : i + (Nat.succ k + 1) = n + 1
⊢ (do
        let x ← f { val := i, isLt := (_ : i < n + 1) } a
        foldAllM.loop (f ∘ castSucc) (i + 1) x k (_ : i + 1 + k = n)) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) } =
    foldAllM.loop (f ∘ castSucc) i a (Nat.succ k) (_ : i + Nat.succ k = n) >>=
      f { val := n, isLt := (_ : n < Nat.succ n) }
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.foldAll_succ
Proof state before:
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ foldAll f init = foldAll (f ∘ succ) (f 0 init)
Tactic:
unfold Fin.foldAll
Proof state after:
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ Id.run (foldAllM f init) = Id.run (foldAllM (f ∘ succ) (f 0 init))
Theorem: Fin.foldAll_succ
Proof state before:
α : Type u
n : Nat
f : Fin (Nat.succ n) → α → α
init : α
⊢ Id.run (foldAllM f init) = Id.run (foldAllM (f ∘ succ) (f 0 init))
Tactic:
exact foldAllM_succ
Proof state after:
no goals