awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
x x' : WriterT ω M α
h : x.run = x'.run
⊢ x = x'

Tactic:
h

Premises used: WriterT
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
inst : Monad M
empty : ω
append : ω → ω → ω
a : α
⊢ Eq.{v + 1} (α := M (α × ω)) (WriterT.run (pure a)) (pure (a, empty))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α β ω : Type u
inst : Monad M
empty : ω
append : ω → ω → ω
f : α → β
cmd : WriterT ω M α
⊢ (f <$> cmd).run =
    (fun (x : α × ω) ↦
        match (motive := α × ω → β × ω) x with
        | (a, w) => (f a, w)) <$>
      cmd.run

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α β ω : Type u
inst : Monad M
empty : ω
append : ω → ω → ω
cmd : WriterT ω M α
f : α → WriterT ω M β
⊢ (cmd >>= f).run = do
    let x ← cmd.run
    match (motive := α × ω → M (β × ω)) x with
      | (a, w₁) =>
        (fun (x : β × ω) ↦
            match (motive := β × ω → β × ω) x with
            | (b, w₂) => (b, append w₁ w₂)) <$>
          (f a).run

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
inst : Monad M
empty : ω
cmd : M α
⊢ Eq (α := M (α × ω)) (WriterT.run (liftM cmd)) ((fun (a : α) ↦ (a, empty)) <$> cmd)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
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
h : (id <$> x).run = x.run
⊢ id <$> x = x

Tactic:
ext
-- Module: Mathlib.Control.Monad.Writer
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).run = x.run

Tactic:
simp
-- Module: Mathlib.Control.Monad.Writer
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
h : (pure x >>= x_1).run = (x_1 x).run
⊢ pure x >>= x_1 = x_1 x

Tactic:
ext
-- Module: Mathlib.Control.Monad.Writer
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).run = (x_1 x).run

Tactic:
simp
-- Module: Mathlib.Control.Monad.Writer
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 γ
h : (x >>= x_1 >>= x_2).run = WriterT.run (x >>= fun (x : α_1) ↦ x_1 x >>= x_2)
⊢ x >>= x_1 >>= x_2 = x >>= fun (x : α_1) ↦ x_1 x >>= x_2

Tactic:
ext
-- Module: Mathlib.Control.Monad.Writer
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).run = WriterT.run (x >>= fun (x : α_1) ↦ x_1 x >>= x_2)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Control.Monad.Writer
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
h :
  (WriterT.run do
      let y ← x_1
      pure (x y)) =
    (x <$> x_1).run
⊢ (do
      let y ← x_1
      pure (x y)) =
    x <$> x_1

Tactic:
ext
-- Module: Mathlib.Control.Monad.Writer
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
⊢ (WriterT.run do
      let y ← x_1
      pure (x y)) =
    (x <$> x_1).run

Tactic:
simp
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
ω : Type u
inst : Monad M
w : ω
⊢ Eq.{v + 1} (α := M (PUnit × ω)) (WriterT.run (tell w)) (pure (PUnit.unit, w))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
inst : Monad M
cmd : WriterT ω M α
⊢ (listen cmd).run =
    (fun (x : α × ω) ↦
        match (motive := α × ω → (α × ω) × ω) x with
        | (a, w) => ((a, w), w)) <$>
      cmd.run

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
inst : Monad M
cmd : WriterT ω M (α × (ω → ω))
⊢ (pass cmd).run =
    (fun (x : (α × (ω → ω)) × ω) ↦
        match (motive := (α × (ω → ω)) × ω → α × ω) x with
        | ((a, f), w) => (a, f w)) <$>
      cmd.run

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
α ω : Type u
M : Type u → Type u_2
ε : Type u_1
inst : MonadExceptOf ε M
e : ε
⊢ Eq.{u_2 + 1} (α := M (α × ω)) (WriterT.run (throw e)) (throw e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Monad.Writer
Goal:
α ω : Type u
M : Type u → Type u_2
ε : Type u_1
inst : MonadExceptOf ε M
cmd : WriterT ω M α
c : ε → WriterT ω M α
⊢ (tryCatch cmd c).run = tryCatch cmd.run fun (e : ε) ↦ (c e).run

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
⊢ η.app = fun {α : Type u} ↦ η.app α

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
f : (α : Type u) → F α → G α
pp : ∀ {α : Type u} (x : α), f α (pure x) = pure x
ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (x <*> y) = f (α → β) x <*> f α y
⊢ (fun {α : Type u} ↦
      { app := f, preserves_pure' := @pp, preserves_seq' := @ps : ApplicativeTransformation F G }.app α) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η η' : ApplicativeTransformation F G
h : η = η'
α : Type u
x : F α
⊢ Eq.{w + 1} (α := G α) ((fun {α : Type u} ↦ η.app α) x) ((fun {α : Type u} ↦ η'.app α) x)

Tactic:
congrArg (fun η'' : ApplicativeTransformation F G => η'' x) h

Premises used: congrArg, ApplicativeTransformation.app
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
α : Type u
x y : F α
h : x = y
⊢ Eq.{w + 1} (α := G α) ((fun {α : Type u} ↦ η.app α) x) ((fun {α : Type u} ↦ η.app α) y)

Tactic:
congrArg (fun z : F α => η z) h

Premises used: congrArg, ApplicativeTransformation.app
-- Module: Mathlib.Control.Traversable.Basic
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 α
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 η
-- Module: Mathlib.Control.Traversable.Basic
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 α
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 }
⊢ { app := app, preserves_pure' := @preserves_pure', preserves_seq' := @preserves_seq' :
      ApplicativeTransformation F G } =
    η'

Tactic:
cases η'
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative 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
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:
congr
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), Eq.{w + 1} (α := G α) ((fun {α : Type u} ↦ η.app α) x) ((fun {α : Type u} ↦ η'.app α) x)
⊢ Eq (α := {α : Type u} → F α → G α) (fun {α : Type u} ↦ η.app α) fun {α : Type u} ↦ η'.app α

Tactic:
grind
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
α : Type u
⊢ ∀ (x : α), Eq.{w + 1} (α := G α) ((fun {α : Type u} ↦ η.app α) (pure x)) (pure x)

Tactic:
η.preserves_pure'

Premises used: ApplicativeTransformation.preserves_pure'
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
α β : Type u
⊢ ∀ (x : F (α → β)) (y : F α),
    Eq.{w + 1} (α := G β) ((fun {α : Type u} ↦ η.app α) (x <*> y))
      ((fun {α : Type u} ↦ η.app α) x <*> (fun {α : Type u} ↦ η.app α) y)

Tactic:
η.preserves_seq'

Premises used: ApplicativeTransformation.preserves_seq'
-- Module: Mathlib.Control.Traversable.Basic
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)
rw₃ rw₄ : Eq.{w + 1} (α := G β) (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)

Tactic:
rw [← pure_seq, η.preserves_seq, preserves_pure, pure_seq]

Premises used: ApplicativeTransformation.preserves_seq, LawfulApplicative.pure_seq, ApplicativeTransformation.preserves_pure
-- Module: Mathlib.Control.Traversable.Basic
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 : α → β
h :
  ∀ (y : F α),
    Eq.{w + 1} (α := G β) (((fun {α : Type u} ↦ η.app α) ∘ Functor.map x) y)
      ((Functor.map x ∘ fun {α : Type u} ↦ η.app α) y)
⊢ Eq (α := F α → G β) ((fun {α : Type u} ↦ η.app α) ∘ Functor.map x) (Functor.map x ∘ fun {α : Type u} ↦ η.app α)

Tactic:
ext y
-- Module: Mathlib.Control.Traversable.Basic
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 α) ∘ Functor.map x) y)
    ((Functor.map x ∘ fun {α : Type u} ↦ η.app α) y)

Tactic:
preserves_map η x y

Premises used: ApplicativeTransformation.preserves_map
-- Module: Mathlib.Control.Traversable.Basic
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 α) ∘ Functor.map x) y)
    ((Functor.map x ∘ fun {α : Type u} ↦ η.app α) y)

Tactic:
exact preserves_map η x y

Premises used: ApplicativeTransformation.preserves_map
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
⊢ ∀ {α : Type u} (x : α), Eq.{v + 1} (α := F α) (id (pure x)) (pure x)

Tactic:
simp
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
α β : Type u
x : F (α → β)
y : F α
⊢ id (x <*> y) = id x <*> id y

Tactic:
simp
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
H : Type u → Type s
inst_2 : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α : Type u
x : α
⊢ Eq.{s + 1} (α := H α) ((fun {α : Type u} ↦ η'.app α) ((fun {α : Type u} ↦ η.app α) (pure x))) (pure x)

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
H : Type u → Type s
inst_2 : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α β : Type u
x : F (α → β)
y : F α
⊢ Eq.{s + 1} (α := H β) ((fun {α : Type u} ↦ η'.app α) ((fun {α : Type u} ↦ η.app α) (x <*> y)))
    ((fun {α : Type u} ↦ η'.app α) ((fun {α : Type u} ↦ η.app α) x) <*>
      (fun {α : Type u} ↦ η'.app α) ((fun {α : Type u} ↦ η.app α) y))

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
H : Type u → Type s
inst_2 : Applicative H
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
α : Type u
x : F α
⊢ Eq.{s + 1} (α := H α) ((fun {α : Type u} ↦ (η'.comp η).app α) x)
    ((fun {α : Type u} ↦ η'.app α) ((fun {α : Type u} ↦ η.app α) x))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
H : Type u → Type s
inst_2 : Applicative H
I : Type u → Type t
inst_3 : Applicative I
η'' : ApplicativeTransformation H I
η' : ApplicativeTransformation G H
η : ApplicativeTransformation F G
⊢ (η''.comp η').comp η = η''.comp (η'.comp η)

Tactic:
rfl

Premises used: ApplicativeTransformation.comp, rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
⊢ η.comp idTransformation = η

Tactic:
ext fun _ _ => rfl

Premises used: ApplicativeTransformation.ext, rfl
-- Module: Mathlib.Control.Traversable.Basic
Goal:
F : Type u → Type v
inst : Applicative F
G : Type u → Type w
inst_1 : Applicative G
η : ApplicativeTransformation F G
⊢ comp idTransformation η = η

Tactic:
ext fun _ _ => rfl

Premises used: ApplicativeTransformation.ext, rfl
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
α : Type u
x : t' α
⊢ Equiv.map eqv id x = x

Tactic:
simp [Equiv.map, id_map]

Premises used: Equiv.map, LawfulFunctor.id_map
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
α β γ : Type u
g : α → β
h : β → γ
x : t' α
⊢ Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)

Tactic:
simp [Equiv.map, Function.comp_def]

Premises used: Equiv.map, Function.comp_def
-- Module: Mathlib.Control.Traversable.Equiv
Goal:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst : Functor t
inst_1 : LawfulFunctor t
⊢ LawfulFunctor t'

Tactic:
let _inst := Equiv.functor eqv
  { map_const := fun {_ _} => rfl
    id_map := Equiv.id_map eqv
    comp_map := Equiv.comp_map eqv }

Premises used: LawfulFunctor.mk, Equiv.id_map, Equiv.functor, Equiv.comp_map, rfl
-- Module: Mathlib.Control.Traversable.Equiv
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
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
⊢ F = Equiv.functor eqv

Tactic:
cases F
-- Module: Mathlib.Control.Traversable.Equiv
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 := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }
⊢ { map := @map, mapConst := @mapConst : Functor t' } = Equiv.functor eqv

Tactic:
dsimp [Equiv.functor]

Premises used: Equiv.functor
-- Module: Mathlib.Control.Traversable.Equiv
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
mk₁ : @mapConst = fun {α β : Type u} ↦ Equiv.map eqv ∘ Function.const β
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }

Tactic:
congr
-- Module: Mathlib.Control.Traversable.Equiv
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 = Equiv.map eqv x_2 x_3
⊢ @map = fun {α β : Type u} ↦ Equiv.map eqv

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Equiv
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_3 : t' x_1), mapConst x_2 x_3 = (Equiv.map eqv ∘ Function.const x_1) x_2 x_3
⊢ @mapConst = fun {α β : Type u} ↦ Equiv.map eqv ∘ Function.const β

Tactic:
ext
-- Module: Mathlib.Control.Traversable.Equiv
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
mk : map x_2 x_3 = x_2 <$> x_3
⊢ map x_2 x_3 = Equiv.map eqv x_2 x_3

Tactic:
rw [← h₀]
-- Module: Mathlib.Control.Traversable.Equiv
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
mk : mapConst x_2 x_3 = Functor.mapConst x_2 x_3
⊢ mapConst x_2 x_3 = (Equiv.map eqv ∘ Function.const x_1) x_2 x_3

Tactic:
rw [← h₁]
-- Module: Mathlib.Control.Traversable.Equiv
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
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
⊢ { map := @map, mapConst := @mapConst : Functor t' } = { map := fun {α β : Type u} ↦ Equiv.map eqv }

Tactic:
congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]]
-- Module: Mathlib.Control.Traversable.Equiv
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 = x_2 <$> x_3

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Equiv
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 = Functor.mapConst x_2 x_3

Tactic:
rfl
-- Module: Mathlib.Control.Traversable.Equiv
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

Tactic:
have : F = Equiv.functor eqv := by
    cases F
    dsimp [Equiv.functor]
    congr <;> ext <;> dsimp only <;> [rw [← h₀]; rw [← h₁]] <;> rfl