awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : StateT σ m α
next : Label ω (StateT σ m) γ → α → StateT σ m ω
⊢ Eq (α := StateT σ m ω)
    (StateT.mk fun (r : σ) ↦ do
      let x ← cmd.run r
      callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
    do
    let x ← cmd
    StateT.mk fun (r : σ) ↦ callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r
have h : ∀ (s : σ),
  Eq (α := m (ω × σ))
    (StateT.run
      (StateT.mk fun (r : σ) ↦ do
        let x ← cmd.run r
        callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
      s)
    (StateT.run
      (do
        let x ← cmd
        StateT.mk fun (r : σ) ↦
            callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r)
      s)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (StateT σ m) β → β → StateT σ m α
⊢ Eq (α := StateT σ m α) (callCC (β := β) fun (f : Label α (StateT σ m) β) ↦ goto f x >>= dead f) (pure x)
have simp : Eq (α := StateT σ m α) (StateT.mk fun (r : σ) ↦ pure (x, r)) (pure x)
Tactic: simp only [callCC, StateT.callCC, StateT.goto_mkLabel, StateT.run_bind, StateT.run_mk,
      callCC_bind_left]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (StateT σ m) β → β → StateT σ m α
⊢ Eq (α := StateT σ m α) (StateT.mk fun (r : σ) ↦ pure (x, r)) (pure x)
have h : ∀ (s : σ), Eq.{v + 1} (α := m (α × σ)) (StateT.run (StateT.mk fun (r : σ) ↦ pure (x, r)) s) (StateT.run (pure x) s)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : StateT σ m α
⊢ (callCC (β := β) fun (x : Label α (StateT σ m) β) ↦ dummy) = dummy
have simp : (StateT.mk fun (r : σ) ↦ dummy.run r) = dummy
Tactic: simp only [callCC, StateT.callCC, @callCC_dummy m _]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : StateT σ m α
⊢ (StateT.mk fun (r : σ) ↦ dummy.run r) = dummy
have h : ∀ (s : σ), StateT.run (StateT.mk fun (r : σ) ↦ dummy.run r) s = dummy.run s
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)
have mk : ∀ (apply : α → m β),
  goto (mkLabel ρ { apply := apply : Label α m β }) i = monadLift (goto { apply := apply : Label α m β } i)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ReaderT ρ m α
next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω
⊢ Eq (α := ReaderT ρ m ω) (callCC (β := γ) fun (f : Label ω (ReaderT ρ m) γ) ↦ cmd >>= next f) do
    let x ← cmd
    callCC (β := γ) fun (f : Label ω (ReaderT ρ m) γ) ↦ next f x
have simp : Eq (α := ReaderT ρ m ω)
  (ReaderT.mk fun (r : ρ) ↦ do
    let x ← cmd.run r
    callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
  do
  let x ← cmd
  ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r
Tactic: simp only [callCC, ReaderT.callCC, ReaderT.run_bind,
                                    callCC_bind_right]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ReaderT ρ m α
next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω
⊢ Eq (α := ReaderT ρ m ω)
    (ReaderT.mk fun (r : ρ) ↦ do
      let x ← cmd.run r
      callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
    do
    let x ← cmd
    ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r
have h : ∀ (ctx : ρ),
  Eq (α := m ω)
    (ReaderT.run
      (ReaderT.mk fun (r : ρ) ↦ do
        let x ← cmd.run r
        callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
      ctx)
    (ReaderT.run
      (do
        let x ← cmd
        ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r)
      ctx)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α
⊢ Eq (α := ReaderT ρ m α) (callCC (β := β) fun (f : Label α (ReaderT ρ m) β) ↦ goto f x >>= dead f) (pure x)
have simp : Eq (α := ReaderT ρ m α) (ReaderT.mk fun (r : ρ) ↦ pure x) (pure x)
Tactic: simp only [callCC, ReaderT.callCC, ReaderT.goto_mkLabel, ReaderT.run_bind,
      ReaderT.run_monadLift, monadLift_self, callCC_bind_left]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α
⊢ Eq (α := ReaderT ρ m α) (ReaderT.mk fun (r : ρ) ↦ pure x) (pure x)
have h : ∀ (ctx : ρ), Eq.{v + 1} (α := m α) (ReaderT.run (ReaderT.mk fun (r : ρ) ↦ pure x) ctx) (ReaderT.run (pure x) ctx)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ReaderT ρ m α
⊢ (callCC (β := β) fun (x : Label α (ReaderT ρ m) β) ↦ dummy) = dummy
have simp : (ReaderT.mk fun (r : ρ) ↦ dummy.run r) = dummy
Tactic: simp only [callCC, ReaderT.callCC, @callCC_dummy m _]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ReaderT ρ m α
⊢ (ReaderT.mk fun (r : ρ) ↦ dummy.run r) = dummy
have h : ∀ (ctx : ρ), ReaderT.run (ReaderT.mk fun (r : ρ) ↦ dummy.run r) ctx = dummy.run ctx
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
        ((F.symm : (a : m₂ r₂) → m₁ r₁) (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
          m₁ r₁))
      ((fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
          ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
            m₂ r₂))
        f) =
    f
have h : ∀ (r : α₁ → m₁ r₁),
  (fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
        ((F.symm : (a : m₂ r₂) → m₁ r₁) (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
          m₁ r₁))
      ((fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
          ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
            m₂ r₂))
        f)
      r =
    f r
Tactic: funext r
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
        ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
          m₂ r₂))
      ((fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
          ((F.symm : (a : m₂ r₂) → m₁ r₁)
              (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
            m₁ r₁))
        f) =
    f
have h : ∀ (r : α₂ → m₂ r₂),
  (fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
        ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
          m₂ r₂))
      ((fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
          ((F.symm : (a : m₂ r₂) → m₁ r₁)
              (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
            m₁ r₁))
        f)
      r =
    f r
Tactic: funext r
-- Lean 4 proof step from Mathlib.Control.Monad.Writer (goal)
Goal:
M : Type u → Type v
α β ω ρ σ : Type u
inst : Monad M
inst_1 : Monoid ω
inst_2 : LawfulMonad M
α_1 : Type u
x : WriterT ω M α_1
⊢ id <$> x = x
have h : (id <$> x).run = x.run
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Writer (goal)
Goal:
M : Type u → Type v
α β ω ρ σ : Type u
inst : Monad M
inst_1 : Monoid ω
inst_2 : LawfulMonad M
α_1 β_1 : Type u
x : α_1
x_1 : α_1 → WriterT ω M β_1
⊢ pure x >>= x_1 = x_1 x
have h : (pure x >>= x_1).run = (x_1 x).run
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Writer (goal)
Goal:
M : Type u → Type v
α β ω ρ σ : Type u
inst : Monad M
inst_1 : Monoid ω
inst_2 : LawfulMonad M
α_1 β_1 γ : Type u
x : WriterT ω M α_1
x_1 : α_1 → WriterT ω M β_1
x_2 : β_1 → WriterT ω M γ
⊢ x >>= x_1 >>= x_2 = x >>= fun (x : α_1) ↦ x_1 x >>= x_2
have h : (x >>= x_1 >>= x_2).run = WriterT.run (x >>= fun (x : α_1) ↦ x_1 x >>= x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Writer (goal)
Goal:
M : Type u → Type v
α β ω ρ σ : Type u
inst : Monad M
inst_1 : Monoid ω
inst_2 : LawfulMonad M
α_1 β_1 : Type u
x : α_1 → β_1
x_1 : WriterT ω M α_1
⊢ (do
      let y ← x_1
      pure (x y)) =
    x <$> x_1
have h : (WriterT.run do
    let y ← x_1
    pure (x y)) =
  (x <$> x_1).run
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η η' : ApplicativeTransformation F G
h : Eq (α := {α : Type u} → F α → G α) (fun {α : Type u} ↦ η.app α) fun {α : Type u} ↦ η'.app α
⊢ η = η'
have mk : ∀ (app : (α : Type u) → F α → G α) (preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x)
  (preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y)
  (h :
    Eq (α := {α : Type u} → F α → G α)
      (fun {α : Type u} ↦
        { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
              ApplicativeTransformation F G }.app
          α)
      fun {α : Type u} ↦ η'.app α),
  { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
      ApplicativeTransformation F G } =
    η'
Tactic: cases η
Cleared hypotheses: η, h
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η' : ApplicativeTransformation F G
app : (α : Type u) → F α → G α
preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x
preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y
h :
  Eq (α := {α : Type u} → F α → G α)
    (fun {α : Type u} ↦
      { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
            ApplicativeTransformation F G }.app
        α)
    fun {α : Type u} ↦ η'.app α
⊢ { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
      ApplicativeTransformation F G } =
    η'
have mk : ∀ (app_1 : (α : Type u) → F α → G α) (preserves_pure'_1 : ∀ {α : Type u} (x : α), app_1 α (pure x) = pure x)
  (preserves_seq'_1 : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app_1 β (x <*> y) = app_1 (α → β) x <*> app_1 α y)
  (h :
    Eq (α := {α : Type u} → F α → G α)
      (fun {α : Type u} ↦
        { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
              ApplicativeTransformation F G }.app
          α)
      fun {α : Type u} ↦
      { app := app_1, preserves_pure' := @preserves_pure'_1, preserves_seq' := @preserves_seq'_1 :
            ApplicativeTransformation F G }.app
        α),
  { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
      ApplicativeTransformation F G } =
    { app := app_1, preserves_pure' := @preserves_pure'_1, preserves_seq' := @preserves_seq'_1 }
Tactic: cases η'
Cleared hypotheses: η', h
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (x <$> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
have rw : Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x <*> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
Tactic: rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type u
x : α → β
y : F α
rw : Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x <*> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
⊢ Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (x <$> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
have rw₁ : Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x) <*> (fun {α : Type u} ↦ η.app α) y)
  (x <$> (fun {α : Type u} ↦ η.app α) y)
Tactic: rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type u
x : α → β
y : F α
rw : Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x <*> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
rw₁ :
  Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x) <*> (fun {α : Type u} ↦ η.app α) y)
    (x <$> (fun {α : Type u} ↦ η.app α) y)
⊢ Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (x <$> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
have rw₂ : Eq.{w + 1} (α := G β) (pure x <*> (fun {α : Type u} ↦ η.app α) y) (x <$> (fun {α : Type u} ↦ η.app α) y)
Tactic: rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type u
x : α → β
y : F α
rw : Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x <*> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
rw₁ :
  Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (pure x) <*> (fun {α : Type u} ↦ η.app α) y)
    (x <$> (fun {α : Type u} ↦ η.app α) y)
rw₂ : Eq.{w + 1} (α := G β) (pure x <*> (fun {α : Type u} ↦ η.app α) y) (x <$> (fun {α : Type u} ↦ η.app α) y)
⊢ Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (x <$> y)) (x <$> (fun {α : Type u} ↦ η.app α) y)
have rw₃ : Eq.{w + 1} (α := G β) (x <$> (fun {α : Type u} ↦ η.app α) y) (x <$> (fun {α : Type u} ↦ η.app α) y)
Tactic: rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]
-- Lean 4 proof step from Mathlib.Control.Traversable.Basic (goal)
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type u
x : α → β
⊢ Eq (α := F α → G β) ((fun {α : Type u} ↦ η.app α) ∘ Functor.map x) (Functor.map x ∘ fun {α : Type u} ↦ η.app α)
have h : ∀ (y : F α),
  Eq.{w + 1} (α := G β) (((fun {α : Type u} ↦ η.app α) ∘ Functor.map x) y)
    ((Functor.map x ∘ fun {α : Type u} ↦ η.app α) y)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ F = Equiv.functor eqv
have mk : ∀ (map : {α β : Type u} → (α → β) → t' α → t' β) (mapConst : {α β : Type u} → α → t' β → t' α)
  (h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f)
  (h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f),
  { map := @map, mapConst := @mapConst : Functor t' } = Equiv.functor eqv
Tactic: cases F
Cleared hypotheses: F, h₀, h₁
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := @map, mapConst := @mapConst : Functor t' } = Equiv.functor eqv
have mk : { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
Tactic: dsimp [Equiv.functor]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
have mk : @map = fun {α β : Type u} ↦ Equiv.map eqv
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
mk : @map = fun {α β : Type u} ↦ Equiv.map eqv
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
have mk₁ : @mapConst = fun {α β : Type u} ↦ Equiv.map eqv ∘ Function.const β
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ @map = fun {α β : Type u} ↦ Equiv.map eqv
have mk : ∀ (x x_1 : Type u) (x_2 : x → x_1) (x_3 : t' x), map x_2 x_3 = Equiv.map eqv x_2 x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ @mapConst = fun {α β : Type u} ↦ Equiv.map eqv ∘ Function.const β
have mk : ∀ (x x_1 : Type u) (x_2 : x) (x_3 : t' x_1), mapConst x_2 x_3 = (Equiv.map eqv ∘ Function.const x_1) x_2 x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
x x_1 : Type u
x_2 : x → x_1
x_3 : t' x
⊢ map x_2 x_3 = Equiv.map eqv x_2 x_3
have mk : map x_2 x_3 = x_2 <$> x_3
Tactic: rw [← h₀]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
x x_1 : Type u
x_2 : x
x_3 : t' x_1
⊢ mapConst x_2 x_3 = (Equiv.map eqv ∘ Function.const x_1) x_2 x_3
have mk : mapConst x_2 x_3 = Functor.mapConst x_2 x_3
Tactic: rw [← h₁]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
have mk : ∀ (x x_1 : Type u) (x_2 : x → x_1) (x_3 : t' x), map x_2 x_3 = x_2 <$> x_3
Tactic: congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
map : {α β : Type u} → (α → β) → t' α → t' β
mapConst : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f
mk : ∀ (x x_1 : Type u) (x_2 : x → x_1) (x_3 : t' x), map x_2 x_3 = x_2 <$> x_3
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
have mk₁ : ∀ (x x_1 : Type u) (x_2 : x) (x_3 : t' x_1), mapConst x_2 x_3 = Functor.mapConst x_2 x_3
Tactic: congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]]
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (hypothesis)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'
have this : F = Equiv.functor eqv
Tactic: have : F = Equiv.functor eqv := by
    cases F
    dsimp [Equiv.functor]
    congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]] <;> rfl
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
this : F = Equiv.functor eqv
⊢ LawfulFunctor t'
have subst : ∀ (h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f)
  (h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f), LawfulFunctor t'
Tactic: subst this
Cleared hypotheses: F, h₀, h₁, this
-- Lean 4 proof step from Mathlib.Control.Traversable.Equiv (goal)
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Traversable t
inst_1 : LawfulTraversable t
α : Type u
x : t' α
⊢ Eq (α := Id (t' α)) (Equiv.traverse eqv pure x) (pure x)
have rw : Eq (α := Id (t' α)) (map (α := t α) (⇑(eqv α) : (a : t α) → t' α) (traverse pure (((eqv α).symm : (a : t' α) → t α) x)))
  (pure x)
Tactic: rw [Equiv.traverse, id_traverse, map_pure, apply_symm_apply]