Theorem: Array.size_modify (Algdata/Data/Array/Lemmas.lean)

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
⊢ ∀ (x : Array α) (n : Nat) (f : α → α), size (modify x n f) = size x
Tactic:
intro x n f
State after:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
⊢ size (modify x n f) = size x

State before:
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
⊢ size (modify x n f) = size x
Tactic:
cases size_modifyM (m:=Id) x n f with | intro w hw =>
dsimp at hw
conv at hw => rhs; change modify x n f
rw [←hw]
exact w.property
State after:
no goals

State before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : Subtype.val <$> w = modifyM x n f
⊢ size (modify x n f) = size x
Tactic:
dsimp at hw
State after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modifyM x n f
⊢ size (modify x n f) = size x

State before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modifyM x n f
⊢ size (modify x n f) = size x
Tactic:
conv at hw => rhs; change modify x n f
State after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size (modify x n f) = size x

State before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size (modify x n f) = size x
Tactic:
rw [←hw]
State after:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size w.val = size x

State before:
case intro
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → α
w : Id { a // (fun y => size y = size x) a }
hw : w.val = modify x n f
⊢ size w.val = size x
Tactic:
exact w.property
State after:
no goals