Theorem: Array.size_mapM' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ Subtype.val <$> pure { val := #[], property := (_ : size #[] = size #[]) } = mapM f #[]
Tactic:
rw [map_pure]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ pure { val := #[], property := (_ : size #[] = size #[]) }.val = mapM f #[]

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
⊢ pure { val := #[], property := (_ : size #[] = size #[]) }.val = mapM f #[]
Tactic:
rfl
State after:
no goals

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    mapM f (push x a)
Tactic:
rw [mapM_push, ← h]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    do
    let y ← Subtype.val <$> y
    let b ← f a
    pure (push y b)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    do
    let y ← Subtype.val <$> y
    let b ← f a
    pure (push y b)
Tactic:
simp only [map_eq_pure_bind, bind_assoc]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (do
      let x_1 ← y
      let x_2 ← f a
      let a_1 ← pure { val := push x_1.val x_2, property := (_ : size (push x_1.val x_2) = size (push x a)) }
      pure a_1.val) =
    do
    let x_1 ← y
    let y ← pure x_1.val
    let b ← f a
    pure (push y b)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (do
      let x_1 ← y
      let x_2 ← f a
      let a_1 ← pure { val := push x_1.val x_2, property := (_ : size (push x_1.val x_2) = size (push x a)) }
      pure a_1.val) =
    do
    let x_1 ← y
    let y ← pure x_1.val
    let b ← f a
    pure (push y b)
Tactic:
apply bind_congr
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ ∀ (a_1 : { a // size a = size x }),
    (do
        let x_1 ← f a
        let a_2 ← pure { val := push a_1.val x_1, property := (_ : size (push a_1.val x_1) = size (push x a)) }
        pure a_2.val) =
      do
      let y ← pure a_1.val
      let b ← f a
      pure (push y b)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ ∀ (a_1 : { a // size a = size x }),
    (do
        let x_1 ← f a
        let a_2 ← pure { val := push a_1.val x_1, property := (_ : size (push a_1.val x_1) = size (push x a)) }
        pure a_2.val) =
      do
      let y ← pure a_1.val
      let b ← f a
      pure (push y b)
Tactic:
intro y
State after:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y✝ : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y✝ = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
y : { a // size a = size x }
⊢ (do
      let x_1 ← f a
      let a_1 ← pure { val := push y.val x_1, property := (_ : size (push y.val x_1) = size (push x a)) }
      pure a_1.val) =
    do
    let y ← pure y.val
    let b ← f a
    pure (push y b)

State before:
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y✝ : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y✝ = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
y : { a // size a = size x }
⊢ (do
      let x_1 ← f a
      let a_1 ← pure { val := push y.val x_1, property := (_ : size (push y.val x_1) = size (push x a)) }
      pure a_1.val) =
    do
    let y ← pure y.val
    let b ← f a
    pure (push y b)
Tactic:
simp only [pure_bind]
State after:
no goals