Theorem: List.mapM'_eq_mapM'_of_eq (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
l : List α
hf : ∀ a ∈ l, f a = g a
⊢ mapM' f l = mapM' g l
Tactic:
induction' l with a as ih <;> simp
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
{ have : as.mapM' f = as.mapM' g := ih (fun a ha => hf a (by simp[ha]))
  have : f a = g a := hf a (by simp)
  simp[*] }
State after:
no goals

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
have : as.mapM' f = as.mapM' g := ih (fun a ha => hf a (by simp[ha]))
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
have : f a = g a := hf a (by simp)
State after:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this✝ : mapM' f as = mapM' g as
this : f a = g a
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)

State before:
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this✝ : mapM' f as = mapM' g as
this : f a = g a
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
Tactic:
simp[*]
State after:
no goals

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a✝ : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a ∈ a✝ :: as, f a = g a
a : α
ha : a ∈ as
⊢ a ∈ a✝ :: as
Tactic:
simp[ha]
State after:
no goals

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ a ∈ a :: as
Tactic:
simp
State after:
no goals