internlm/Lean-Github huggingface dataset:
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ queue[0]? = some event ∧ time event.val ≥ next.val
Tactic:
apply And.intro h'
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ time event.val ≥ next.val
Theorem: Queue.nextTime_some
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
event : { e // bound ≤ time e }
h' : queue[0]? = some event
h : { val := time event.val, property := (_ : bound ≤ time event.val) } = next
⊢ time event.val ≥ next.val
Tactic:
simp [←h]
Proof state after:
no goals
Theorem: Queue.nextTime_isSome_iff_not_isEmpty
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ ¬isEmpty queue = true
Tactic:
rw [Queue.isEmpty, ←Array.getElem?_zero_isSome_iff_not_isEmpty]
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true
Theorem: Queue.nextTime_isSome_iff_not_isEmpty
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true
Tactic:
simp [nextTime]
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true
Theorem: Queue.nextTime_isSome_iff_not_isEmpty
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true
Tactic:
constructor <;> split <;> simp_all [Option.isSome]
Proof state after:
case mp.h_2
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
nextEvent✝ : { e // bound ≤ time e }
heq✝ : queue[0]? = some nextEvent✝
⊢ (match queue.events[0]? with
    | some val => true
    | none => false) =
    true
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
⊢ event ∈ queue₂ → event ∈ merge queue₁ queue₂
Tactic:
intro h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂
Tactic:
simp [merge]
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈
    if isEmpty queue₁ = true then queue₂
    else
      if isEmpty queue₂ = true then queue₁
      else
        {
          events :=
            merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
              merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                (Array.split queue₂.events fun x => decide (time x = bound)).snd,
          sorted :=
            (_ :
              Sorted
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
          bounded :=
            (_ :
              ∀ {event : ε},
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                          (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                        merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                          (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                    some event →
                  bound ≤ time event) }
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : isEmpty queue₁ = true
⊢ event ∈ queue₂
Tactic:
case inl => exact h
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
Tactic:
case inr.inl he =>
  rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
  simp [Membership.mem, he] at h
  contradiction
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inr.inr =>
  by_cases time event = bound
  case inl ht =>
    sorry
  case inr ht =>
    sorry
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : isEmpty queue₁ = true
⊢ event ∈ queue₂
Tactic:
exact h
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
Tactic:
rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
⊢ event ∈ queue₁
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
⊢ event ∈ queue₁
Tactic:
simp [Membership.mem, he] at h
Proof state after:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
h : List.Mem event []
⊢ event ∈ queue₁
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
h : List.Mem event []
⊢ event ∈ queue₁
Tactic:
contradiction
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inl ht =>
  sorry
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
case inr ht =>
  sorry
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
sorry
Proof state after:
no goals
Theorem: Queue.merge_mem₂
Proof state before:
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝¹ : ¬isEmpty queue₁ = true
h✝ : ¬isEmpty queue₂ = true
ht : ¬time event = bound
⊢ event ∈
    {
      events :=
        merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
            (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
          merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
            (Array.split queue₂.events fun x => decide (time x = bound)).snd,
      sorted :=
        (_ :
          Sorted
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                  (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                  (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
      bounded :=
        (_ :
          ∀ {event : ε},
            (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                some event →
              bound ≤ time event) }
Tactic:
sorry
Proof state after:
no goals
Theorem: ReactionT.setOutput_other_port
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ var' ≠ var → Output.ports (setOutput var val input).fst var' = none
Tactic:
simp [setOutput]
Proof state after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Theorem: ReactionT.setOutput_other_port
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Tactic:
first | done | rfl | intro h; simp [h]
Proof state after:
no goals
Theorem: ReactionT.setOutput_other_port
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Tactic:
done
Proof state after:
no goals
Theorem: ReactionT.setOutput_other_port
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Tactic:
intro h
Proof state after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
h : ¬var' = var
⊢ (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Theorem: ReactionT.setOutput_other_port
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
h : ¬var' = var
⊢ (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Tactic:
simp [h]
Proof state after:
no goals
Theorem: ReactionT.setState_other_state
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ var' ≠ var → Output.state (setState var val input).fst var' = Input.state input var'
Tactic:
simp [setState]
Proof state after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Theorem: ReactionT.setState_other_state
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
first | done | rfl | intro h; simp [h]
Proof state after:
no goals
Theorem: ReactionT.setState_other_state
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
done
Proof state after:
no goals
Theorem: ReactionT.setState_other_state
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
intro h
Proof state after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
h : ¬var' = var
⊢ (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Theorem: ReactionT.setState_other_state
Proof state before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
h : ¬var' = var
⊢ (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
simp [h]
Proof state after:
no goals
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
as bs : List α
⊢ sum (as ++ bs) = sum as + sum bs
Tactic:
induction as
Proof state after:
case nil
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs

case cons
α : Type u
inst✝ : AddMonoid α
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : sum (tail✝ ++ bs) = sum tail✝ + sum bs
⊢ sum (head✝ :: tail✝ ++ bs) = sum (head✝ :: tail✝) + sum bs
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs
Tactic:
case nil =>
  change sum bs = 0 + sum bs
  rw [AddMonoid.zero_add]
Proof state after:
no goals
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: as ++ bs) = sum (a :: as) + sum bs
Tactic:
case cons a as h_ind =>
  dsimp
  change a + sum (as++bs) = a + sum as + sum bs
  rw [h_ind]
  rw [AddSemigroup.add_assoc]
Proof state after:
no goals
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs
Tactic:
change sum bs = 0 + sum bs
Proof state after:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum bs = 0 + sum bs
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum bs = 0 + sum bs
Tactic:
rw [AddMonoid.zero_add]
Proof state after:
no goals
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: as ++ bs) = sum (a :: as) + sum bs
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: (as ++ bs)) = sum (a :: as) + sum bs
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: (as ++ bs)) = sum (a :: as) + sum bs
Tactic:
change a + sum (as++bs) = a + sum as + sum bs
Proof state after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + sum (as ++ bs) = a + sum as + sum bs
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + sum (as ++ bs) = a + sum as + sum bs
Tactic:
rw [h_ind]
Proof state after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + (sum as + sum bs) = a + sum as + sum bs
Theorem: List.sum_append
Proof state before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + (sum as + sum bs) = a + sum as + sum bs
Tactic:
rw [AddSemigroup.add_assoc]
Proof state after:
no goals
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
ass : List (List α)
⊢ sum (join ass) = sum (map sum ass)
Tactic:
induction ass
Proof state after:
case nil
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])

case cons
α : Type u
inst✝ : AddMonoid α
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : sum (join tail✝) = sum (map sum tail✝)
⊢ sum (join (head✝ :: tail✝)) = sum (map sum (head✝ :: tail✝))
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])
Tactic:
case nil => rfl
Proof state after:
no goals
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (join (n :: ns)) = sum (map sum (n :: ns))
Tactic:
case cons n ns h_ind =>
  dsimp
  rw [sum_append, sum_cons, h_ind]
Proof state after:
no goals
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])
Tactic:
rfl
Proof state after:
no goals
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (join (n :: ns)) = sum (map sum (n :: ns))
Tactic:
dsimp
Proof state after:
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (n ++ join ns) = sum (sum n :: map sum ns)
Theorem: List.sum_join
Proof state before:
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (n ++ join ns) = sum (sum n :: map sum ns)
Tactic:
rw [sum_append, sum_cons, h_ind]
Proof state after:
no goals