internlm/Lean-Github huggingface dataset:
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = do
    let b ← fish f g head
    let bs ← mapM (fish f g) tail
    pure (b :: bs)
Tactic:
simp[fish]
Proof state after:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (do
      let x ← f head
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    do
    let x ← f head
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (do
      let x ← f head
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    do
    let x ← f head
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
congr
Proof state after:
case e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (fun x => do
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    fun x => do
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (fun x => do
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    fun x => do
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
funext x'
Proof state after:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let x ← mapM f tail
      let __do_lift ← g x'
      let __do_lift_1 ← mapM g x
      pure (__do_lift :: __do_lift_1)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let x ← mapM f tail
      let __do_lift ← g x'
      let __do_lift_1 ← mapM g x
      pure (__do_lift :: __do_lift_1)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
rewrite [commute_implies_mapM_commute]
Proof state after:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let r2 ← g x'
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let r2 ← g x'
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
congr
Proof state after:
case e_a.h.e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (fun r2 => do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    fun b => do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h.e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (fun r2 => do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    fun b => do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
funext x'
Proof state after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
simp [fish] at IH
Proof state after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
rewrite [<- IH]
Proof state after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM f tail >>= mapM g
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM f tail >>= mapM g
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
simp[bind_assoc]
Proof state after:
case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Theorem: mapMCommute.mapM_commute
Proof state before:
case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
Tactic:
apply COMMUTE
Proof state after:
no goals
Theorem: SCF_SELECT.equivalent
Proof state before:
b : FinInt 1
n m : FinInt 32
⊢ run (denoteOp Δ LHS) (INPUT b n m) = run (denoteOp Δ RHS) (INPUT b n m)
Tactic:
simp [LHS, RHS, INPUT]
Proof state after:
b : FinInt 1
n m : FinInt 32
⊢ run
      (denoteOp Δ
        (Op.mk "scf.if" [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)]
          [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
          [Region.mk "entry" []
              [Op.mk "scf.yield" [] [(SSAVal.SSAVal "n", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk [])],
            Region.mk "entry" []
              [Op.mk "scf.yield" [] [(SSAVal.SSAVal "m", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk [])]]
          (AttrDict.mk [])))
      (SSAEnv.One
        [(SSAVal.SSAVal "b", { fst := MLIRType.i1, snd := b }), (SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })]) =
    run
      (denoteOp Δ
        (Op.mk "arith.select" [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)]
          [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1),
            (SSAVal.SSAVal "n", MLIRType.int Signedness.Signless 32),
            (SSAVal.SSAVal "m", MLIRType.int Signedness.Signless 32)]
          [] (AttrDict.mk [])))
      (SSAEnv.One
        [(SSAVal.SSAVal "b", { fst := MLIRType.i1, snd := b }), (SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })])
Theorem: reverse_mkSymm
Proof state before:
α : Type u_1
xs : List α
⊢ List.reverse (mkSymm xs) = mkSymm xs
Tactic:
simp [mkSymm]
Proof state after:
no goals
Theorem: MyNat.one_add_add
Proof state before:
m n : MyNat
⊢ m + 1 + n = m + n + 1
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  dsimp
  congr 1
Proof state after:
no goals
Theorem: MyNat.one_add_add
Proof state before:
case zero
m : MyNat
⊢ m + 1 + zero = m + zero + 1
Tactic:
rfl
Proof state after:
no goals
Theorem: MyNat.one_add_add
Proof state before:
case succ
m n : MyNat
ih : m + 1 + n = m + n + 1
⊢ m + 1 + succ n = m + succ n + 1
Tactic:
dsimp
Proof state after:
case succ
m n : MyNat
ih : m + 1 + n = m + n + 1
⊢ m + 1 + n + 1 = m + n + 1 + 1
Theorem: MyNat.one_add_add
Proof state before:
case succ
m n : MyNat
ih : m + 1 + n = m + n + 1
⊢ m + 1 + n + 1 = m + n + 1 + 1
Tactic:
congr 1
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
m : MyNat
⊢ 0 + m = m
Tactic:
induction m with
| zero => dsimp
| succ m ih =>
  dsimp
  rw [ih]
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case zero

⊢ 0 + zero = zero
Tactic:
dsimp
Proof state after:
no goals
Theorem: MyNat.zero_add
Proof state before:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + succ m = succ m
Tactic:
dsimp
Proof state after:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + m + 1 = m + 1
Theorem: MyNat.zero_add
Proof state before:
case succ
m : MyNat
ih : 0 + m = m
⊢ 0 + m + 1 = m + 1
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
m n o : MyNat
⊢ m + (n + o) = m + n + o
Tactic:
induction o with
| zero => simp
| succ o ih => simp [ih]
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case zero
m n : MyNat
⊢ m + (n + zero) = m + n + zero
Tactic:
simp
Proof state after:
no goals
Theorem: MyNat.add_assoc
Proof state before:
case succ
m n o : MyNat
ih : m + (n + o) = m + n + o
⊢ m + (n + succ o) = m + n + succ o
Tactic:
simp [ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
m n : MyNat
⊢ m + n = n + m
Tactic:
induction n with
| zero =>
  dsimp
  rw [zero_add]
| succ n ih =>
  dsimp
  rw [one_add_add]
  rw [ih]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ m + zero = zero + m
Tactic:
dsimp
Proof state after:
case zero
m : MyNat
⊢ m = 0 + m
Theorem: MyNat.add_comm
Proof state before:
case zero
m : MyNat
⊢ m = 0 + m
Tactic:
rw [zero_add]
Proof state after:
no goals
Theorem: MyNat.add_comm
Proof state before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + succ n = succ n + m
Tactic:
dsimp
Proof state after:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + 1 + m
Theorem: MyNat.add_comm
Proof state before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + 1 + m
Tactic:
rw [one_add_add]
Proof state after:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + m + 1
Theorem: MyNat.add_comm
Proof state before:
case succ
m n : MyNat
ih : m + n = n + m
⊢ m + n + 1 = n + m + 1
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: ne_nil_of_mem
Proof state before:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ l ≠ []
Tactic:
aesop
Proof state after:
no goals
Theorem: not_mem_cons_of_ne_of_not_mem
Proof state before:
α : Type u_1
a y : α
l : List α
⊢ a ≠ y → ¬a ∈ l → ¬a ∈ y :: l
Tactic:
aesop
Proof state after:
no goals
Theorem: mem_map
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
b : β
l : List α
⊢ b ∈ List.map f l ↔ ∃ a, a ∈ l ∧ f a = b
Tactic:
induction l <;> aesop
Proof state after:
no goals
Theorem: mem_map_of_mem
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
a : α
l : List α
h : a ∈ l
⊢ f a ∈ List.map f l
Tactic:
aesop
Proof state after:
no goals
Theorem: eq_nil_of_subset_nil
Proof state before:
α : Type u_1
l : List α
⊢ l ⊆ [] → l = []
Tactic:
aesop (add 1% cases List)
Proof state after:
no goals
Theorem: MiniChess.foo
Proof state before:
p : Piece
n✝ : ℕ
start stop : Pos n✝
⊢ Piece.LegalMove start stop p → start ≠ stop
Tactic:
intro legal
Proof state after:
p : Piece
n✝ : ℕ
start stop : Pos n✝
legal : Piece.LegalMove start stop p
⊢ start ≠ stop
Theorem: MiniChess.foo
Proof state before:
p : Piece
n✝ : ℕ
start stop : Pos n✝
legal : Piece.LegalMove start stop p
⊢ start ≠ stop
Tactic:
cases legal with
| rookHorizontal h _ => exact h
| rookVertical h _ => exact h
| king h _ _ => exact h
Proof state after:
no goals
Theorem: MiniChess.foo
Proof state before:
case rookHorizontal
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝ : start.y = stop.y
⊢ start ≠ stop
Tactic:
exact h
Proof state after:
no goals
Theorem: MiniChess.foo
Proof state before:
case rookVertical
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝ : start.x = stop.x
⊢ start ≠ stop
Tactic:
exact h
Proof state after:
no goals
Theorem: MiniChess.foo
Proof state before:
case king
n✝ : ℕ
start stop : Pos n✝
h : start ≠ stop
a✝¹ : Nat.dist ↑start.x ↑stop.x ≤ 1
a✝ : Nat.dist ↑start.y ↑stop.y ≤ 1
⊢ start ≠ stop
Tactic:
exact h
Proof state after:
no goals
Theorem: MiniChess.Board.set_same
Proof state before:
n : ℕ
pos : Pos n
p? : Option PPiece
b : Board n
⊢ set b pos p? pos = p?
Tactic:
simp [set]
Proof state after:
no goals
Theorem: MiniChess.Board.set_different
Proof state before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
⊢ pos' ≠ pos → set b pos p? pos' = b pos'
Tactic:
intro h
Proof state after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ set b pos p? pos' = b pos'
Theorem: MiniChess.Board.set_different
Proof state before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ set b pos p? pos' = b pos'
Tactic:
simp [set]
Proof state after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ pos = pos' → p? = b pos'
Theorem: MiniChess.Board.set_different
Proof state before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
⊢ pos = pos' → p? = b pos'
Tactic:
intros
Proof state after:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
a✝ : pos = pos'
⊢ p? = b pos'