awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y

Tactic:
(seqRight_eq1 _ (y Unit.unit)).trans (seqRight_eq2 _ (y Unit.unit)).symm

Premises used: Unit.unit, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x)
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor_1 : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), Eq (α := F β) (x *> y) (const α id <$> x <*> y)
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure_1 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
seq_assoc_1 : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y

Tactic:
exact (seqRight_eq1 _ (y Unit.unit)).trans (seqRight_eq2 _ (y Unit.unit)).symm

Premises used: Unit.unit, Eq.symm, Eq.trans
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type v
f : α → β
x : α
⊢ Eq.{w + 1} (α := F (G β)) (run (f <$> pure x)) (run (pure (f x)))

Tactic:
simp
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type v
f : Comp F G (α → β)
x : α
⊢ (f <*> pure x).run = run ((fun (g : α → β) ↦ g x) <$> f)

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
x : Comp F G α
f : Comp F G (α → β)
g : Comp F G (β → γ)
⊢ (g <*> (f <*> x)).run = (Function.comp <$> g <*> f <*> x).run

Tactic:
simp [comp_def, functor_norm]

Premises used: Function.comp_def
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β : Type v
f : α → β
x : Comp F G α
⊢ run (pure f <*> x) = (f <$> x).run

Tactic:
simp [functor_norm]
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ α_1 β_1 : Type v
x : Comp F G α_1
y : Comp F G β_1
⊢ x <* y = const β_1 <$> x <*> y

Tactic:
rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ α_1 β_1 : Type v
x : Comp F G α_1
y : Comp F G β_1
⊢ Eq (α := Comp F G β_1) (x *> y) (const α_1 id <$> x <*> y)

Tactic:
rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u_1 → Type u_2
AF : Applicative F
inst : LawfulApplicative F
⊢ instApplicativeComp = AF

Tactic:
@Applicative.ext F _ _ (instLawfulApplicativeComp (F := Id)) _
    (fun _ => rfl) (fun _ _ => rfl)

Premises used: Id, Functor.Comp, Applicative.ext, rfl
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u_1 → Type u_2
AF : Applicative F
inst : LawfulApplicative F
α β : Type u_1
f : F (α → β)
x : F α
rw rw₁ : f <*> x = f <*> x
⊢ id <$> f <*> x = f <*> x

Tactic:
rw [id_map]

Premises used: LawfulFunctor.id_map
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x : Comp f g α_1
x_1 : Comp f g β_1
simp! :
  Eq (α := Comp f g (α_1 × β_1))
    (mk
        (map (α := g (β_1 → α_1 × β_1)) (fun (x1 : g (β_1 → α_1 × β_1)) (x2 : g β_1) ↦ x1 <*> x2)
            (mk ((fun (x : g α_1) ↦ Prod.mk <$> x) <$> x) : Comp f g (β_1 → α_1 × β_1)) <*>
          x_1) :
      Comp f g (α_1 × β_1))
    (mk
        (map (α := g (α_1 → α_1 × β_1)) (fun (x1 : g (α_1 → α_1 × β_1)) (x2 : g α_1) ↦ x1 <*> x2)
            (mk ((fun (x : g β_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x) <$> x_1) : Comp f g (α_1 → α_1 × β_1)) <*>
          x) :
      Comp f g (α_1 × β_1))
⊢ Eq (α := Comp f g (α_1 × β_1)) (Prod.mk <$> x <*> x_1) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x_1 <*> x)

Tactic:
simp! [map, Seq.seq]

Premises used: Seq.seq, Functor.map
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x : Comp f g α_1
x_1 : Comp f g β_1
rw :
  Eq (α := Comp f g (α_1 × β_1))
    (mk
      ((flip fun (x1 : g (β_1 → α_1 × β_1)) (x2 : g β_1) ↦ x1 <*> x2) <$> x_1 <*>
        mk ((fun (x : g α_1) ↦ Prod.mk <$> x) <$> x)))
    (mk
      (map (α := g (α_1 → α_1 × β_1)) (fun (x1 : g (α_1 → α_1 × β_1)) (x2 : g α_1) ↦ x1 <*> x2)
          (mk ((fun (x : g β_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x) <$> x_1) : Comp f g (α_1 → α_1 × β_1)) <*>
        x))
⊢ Eq (α := Comp f g (α_1 × β_1))
    (mk
        (map (α := g (β_1 → α_1 × β_1)) (fun (x1 : g (β_1 → α_1 × β_1)) (x2 : g β_1) ↦ x1 <*> x2)
            (mk ((fun (x : g α_1) ↦ Prod.mk <$> x) <$> x) : Comp f g (β_1 → α_1 × β_1)) <*>
          x_1) :
      Comp f g (α_1 × β_1))
    (mk
        (map (α := g (α_1 → α_1 × β_1)) (fun (x1 : g (α_1 → α_1 × β_1)) (x2 : g α_1) ↦ x1 <*> x2)
            (mk ((fun (x : g β_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x) <$> x_1) : Comp f g (α_1 → α_1 × β_1)) <*>
          x) :
      Comp f g (α_1 × β_1))

Tactic:
rw [commutative_map]

Premises used: CommApplicative.commutative_map
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x : Comp f g α_1
x_1 : Comp f g β_1
simp :
  Eq (α := Comp f g (α_1 × β_1)) ((fun (a : g β_1) (x : g α_1) ↦ Prod.mk <$> x <*> a) <$> x_1 <*> x)
    ((fun (a : g β_1) (x2 : g α_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> a <*> x2) <$> x_1 <*> x)
⊢ Eq (α := Comp f g (α_1 × β_1))
    (mk
      ((flip fun (x1 : g (β_1 → α_1 × β_1)) (x2 : g β_1) ↦ x1 <*> x2) <$> x_1 <*>
        mk ((fun (x : g α_1) ↦ Prod.mk <$> x) <$> x)))
    (mk
      (map (α := g (α_1 → α_1 × β_1)) (fun (x1 : g (α_1 → α_1 × β_1)) (x2 : g α_1) ↦ x1 <*> x2)
          (mk ((fun (x : g β_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x) <$> x_1) : Comp f g (α_1 → α_1 × β_1)) <*>
        x))

Tactic:
simp only [mk, flip, seq_map_assoc, Function.comp_def, map_map]

Premises used: flip, Function.comp_def, Functor.Comp.mk, Functor.map_map, seq_map_assoc
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x : Comp f g α_1
x_1 : Comp f g β_1
e_a :
  Eq.{u + 1} (α := g β_1 → g α_1 → g (α_1 × β_1)) (fun (a : g β_1) (x : g α_1) ↦ Prod.mk <$> x <*> a)
    fun (a : g β_1) (x2 : g α_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> a <*> x2
⊢ Eq (α := Comp f g (α_1 × β_1)) ((fun (a : g β_1) (x : g α_1) ↦ Prod.mk <$> x <*> a) <$> x_1 <*> x)
    ((fun (a : g β_1) (x2 : g α_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> a <*> x2) <$> x_1 <*> x)

Tactic:
congr
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x : Comp f g α_1
x_1 : Comp f g β_1
e_a :
  ∀ (x : g β_1) (y : g α_1),
    Eq (α := g (α_1 × β_1)) (Prod.mk <$> y <*> x) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)
⊢ Eq.{u + 1} (α := g β_1 → g α_1 → g (α_1 × β_1)) (fun (a : g β_1) (x : g α_1) ↦ Prod.mk <$> x <*> a)
    fun (a : g β_1) (x2 : g α_1) ↦ (fun (b : β_1) (a : α_1) ↦ (a, b)) <$> a <*> x2

Tactic:
funext x y
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x_1 : Comp f g α_1
x_2 : Comp f g β_1
x : g β_1
y : g α_1
e_a : Eq (α := g (α_1 × β_1)) (flip Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)
⊢ Eq (α := g (α_1 × β_1)) (Prod.mk <$> y <*> x) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)

Tactic:
rw [commutative_map]

Premises used: CommApplicative.commutative_map
-- Module: Mathlib.Control.Applicative
Goal:
F : Type u → Type w
G : Type v → Type u
inst : Applicative F
inst_1 : Applicative G
inst_2 : LawfulApplicative F
inst_3 : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst_4 : Applicative f
inst_5 : Applicative g
inst_6 : CommApplicative f
inst_7 : CommApplicative g
α_1 β_1 : Type v
x_1 : Comp f g α_1
x_2 : Comp f g β_1
x : g β_1
y : g α_1
⊢ Eq (α := g (α_1 × β_1)) (flip Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)

Tactic:
congr
-- Module: Mathlib.Control.Applicative
Goal:
α β : Type w
f : Type u → Type v
g : Type w → Type u
inst : Applicative f
inst_1 : Applicative g
h : f (g (α → β))
x : f (g α)
⊢ Comp.mk h <*> Comp.mk x = Comp.mk ((fun (x1 : g (α → β)) (x2 : g α) ↦ x1 <*> x2) <$> h <*> x)

Tactic:
rfl

Premises used: Functor.Comp.seq, Functor.Comp.mk, rfl
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : Monoid α
α_1 β : Type u_2
x : Const α α_1
x_1 : Const α β
⊢ x <* x_1 = Function.const β <$> x <*> x_1

Tactic:
simp [Seq.seq, SeqLeft.seqLeft]

Premises used: Seq.seq, SeqLeft.seqLeft
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : Monoid α
α_1 β : Type u_2
x : Const α α_1
x_1 : Const α β
⊢ Eq (α := Const α β) (x *> x_1) (Function.const α_1 id <$> x <*> x_1)

Tactic:
simp [Seq.seq, SeqRight.seqRight]

Premises used: Seq.seq, SeqRight.seqRight
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : Monoid α
α_1 β : Type u_2
x : α_1 → β
x_1 : Const α α_1
⊢ pure x <*> x_1 = x <$> x_1

Tactic:
simp [Const.map, map, Seq.seq, pure, one_mul]

Premises used: Pure.pure, Functor.Const.map, Seq.seq, Functor.map, one_mul
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : Monoid α
α_1 β : Type u_2
x : Const.{u_1, u_2} α (α_1 → β)
x_1 : α_1
⊢ x <*> pure x_1 = (fun (h : α_1 → β) ↦ h x_1) <$> x

Tactic:
simp [Const.map, map, Seq.seq, pure, mul_one]

Premises used: Pure.pure, Functor.Const.map, Seq.seq, mul_one, Functor.map
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : Monoid α
α_1 β γ : Type u_2
x : Const α α_1
x_1 : Const.{u_1, u_2} α (α_1 → β)
x_2 : Const.{u_1, u_2} α (β → γ)
⊢ x_2 <*> (x_1 <*> x) = Function.comp <$> x_2 <*> x_1 <*> x

Tactic:
simp [Const.map, map, Seq.seq, mul_assoc]

Premises used: Functor.Const.map, mul_assoc, Seq.seq, Functor.map
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : AddMonoid α
α_1 β : Type u_2
x : AddConst α α_1
x_1 : AddConst α β
⊢ x <* x_1 = Function.const β <$> x <*> x_1

Tactic:
simp [Seq.seq, SeqLeft.seqLeft]

Premises used: Seq.seq, SeqLeft.seqLeft
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : AddMonoid α
α_1 β : Type u_2
x : AddConst α α_1
x_1 : AddConst α β
⊢ Eq (α := AddConst α β) (x *> x_1) (Function.const α_1 id <$> x <*> x_1)

Tactic:
simp [Seq.seq, SeqRight.seqRight]

Premises used: Seq.seq, SeqRight.seqRight
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : AddMonoid α
α_1 β : Type u_2
x : α_1 → β
x_1 : AddConst α α_1
⊢ pure x <*> x_1 = x <$> x_1

Tactic:
simp [Const.map, map, Seq.seq, pure, zero_add]

Premises used: Pure.pure, Functor.Const.map, Seq.seq, zero_add, Functor.map
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : AddMonoid α
α_1 β : Type u_2
x : AddConst.{u_1, u_2} α (α_1 → β)
x_1 : α_1
⊢ x <*> pure x_1 = (fun (h : α_1 → β) ↦ h x_1) <$> x

Tactic:
simp [Const.map, map, Seq.seq, pure, add_zero]

Premises used: Pure.pure, Functor.Const.map, Seq.seq, add_zero, Functor.map
-- Module: Mathlib.Control.Applicative
Goal:
α : Type u_1
inst : AddMonoid α
α_1 β γ : Type u_2
x : AddConst α α_1
x_1 : AddConst.{u_1, u_2} α (α_1 → β)
x_2 : AddConst.{u_1, u_2} α (β → γ)
⊢ x_2 <*> (x_1 <*> x) = Function.comp <$> x_2 <*> x_1 <*> x

Tactic:
simp [Const.map, map, Seq.seq, add_assoc]

Premises used: Functor.Const.map, add_assoc, Seq.seq, Functor.map
-- Module: Mathlib.Control.Basic
Goal:
α : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F α
⊢ (pure fun (x : α) ↦ x) <*> x = x

Tactic:
pure_id_seq x

Premises used: pure_id_seq
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
simp : x <*> (pure f <*> y) = (pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y
⊢ x <*> f <$> y = (fun (x : α → β) ↦ x ∘ f) <$> x <*> y

Tactic:
simp only [← pure_seq]

Premises used: LawfulApplicative.pure_seq
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
simp :
  Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y)
    ((pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y)
⊢ x <*> (pure f <*> y) = (pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y

Tactic:
simp only [seq_assoc, seq_pure, ← comp_map]

Premises used: LawfulApplicative.seq_pure, LawfulApplicative.seq_assoc, LawfulFunctor.comp_map
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
simp :
  Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y)
    ((fun (x : α → β) ↦ x ∘ f) <$> x <*> y)
⊢ Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y)
    ((pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y)

Tactic:
simp [pure_seq]

Premises used: LawfulApplicative.pure_seq
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y)
    ((fun (x : α → β) ↦ x ∘ f) <$> x <*> y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
simp : Eq.{v + 1} (α := F γ) (pure f <*> (x <*> y)) ((pure fun (x : α → β) ↦ f ∘ x) <*> x <*> y)
⊢ f <$> (x <*> y) = (fun (x : α → β) ↦ f ∘ x) <$> x <*> y

Tactic:
simp only [← pure_seq]

Premises used: LawfulApplicative.pure_seq
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ Eq.{v + 1} (α := F γ) (pure f <*> (x <*> y)) ((pure fun (x : α → β) ↦ f ∘ x) <*> x <*> y)

Tactic:
simp [seq_assoc]

Premises used: LawfulApplicative.seq_assoc
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ f <$> x >>= g = x >>= g ∘ f

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Premises used: Bind.kleisliRight
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Premises used: Bind.kleisliRight
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h

Tactic:
simp +unfoldPartialApp only [(· >=> ·), functor_norm]

Premises used: Bind.kleisliRight
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp, id, LawfulMonad.pure_bind, joinM
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp, id, LawfulMonad.pure_bind, joinM
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a

Tactic:
simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind, bind_pure]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp, id, bind_pure, LawfulMonad.pure_bind, joinM
-- Module: Mathlib.Control.Basic
Goal:
m : Type u → Type u
inst : Monad m
inst_1 : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure a) = a

Tactic:
LawfulMonad.pure_bind a id

Premises used: id, LawfulMonad.pure_bind, joinM
-- Module: Mathlib.Control.Basic
Goal:
F : Type → Type v
inst : Alternative F
h : Decidable True
⊢ Eq.{v + 1} (α := F Unit) (guard True) (pure ())

Tactic:
simp [guard]

Premises used: guard
-- Module: Mathlib.Control.Basic
Goal:
F : Type → Type v
inst : Alternative F
h : Decidable False
⊢ Eq.{v + 1} (α := F Unit) (guard False) failure

Tactic:
simp [guard]

Premises used: guard
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
map_const : ∀ {α β : Type u}, Eq (α := α → e ⊕ β → e ⊕ α) Functor.mapConst (Functor.map ∘ Function.const β)
id_map : ∀ {α : Type u} (x : e ⊕ α), id <$> x = x
comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
⊢ LawfulFunctor (Sum e)

Tactic:
constructor
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : e ⊕ α_1
id_map : ∀ (x : e), Eq (α := e ⊕ α_1) (id <$> inl x) (inl x)
id_map₁ : ∀ (x : α_1), Eq (α := e ⊕ α_1) (id <$> inr x) (inr x)
⊢ id <$> x = x

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : e ⊕ α_1
id_map : ∀ (x : e), Eq (α := e ⊕ α_1) (id <$> inl x) (inl x)
id_map₁ : ∀ (x : α_1), Eq (α := e ⊕ α_1) (id <$> inr x) (inr x)
⊢ id <$> x = x

Tactic:
try casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : e ⊕ α_1
comp_map : ∀ (x : e), (h ∘ g) <$> inl x = h <$> g <$> inl x
comp_map₁ : ∀ (x : α_1), Eq (α := e ⊕ γ_1) ((h ∘ g) <$> inr x) (h <$> g <$> inr x)
⊢ (h ∘ g) <$> x = h <$> g <$> x

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : e ⊕ α_1
comp_map : ∀ (x : e), (h ∘ g) <$> inl x = h <$> g <$> inl x
comp_map₁ : ∀ (x : α_1), Eq (α := e ⊕ γ_1) ((h ∘ g) <$> inr x) (h <$> g <$> inr x)
⊢ (h ∘ g) <$> x = h <$> g <$> x

Tactic:
try casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
⊢ Eq (α := α_1 → e ⊕ β_1 → e ⊕ α_1) Functor.mapConst (Functor.map ∘ Function.const β_1)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : e
⊢ Eq (α := e ⊕ α_1) (id <$> inl x) (inl x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : α_1
⊢ Eq (α := e ⊕ α_1) (id <$> inr x) (inr x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : e
⊢ (h ∘ g) <$> inl x = h <$> g <$> inl x

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : α_1
⊢ Eq (α := e ⊕ γ_1) ((h ∘ g) <$> inr x) (h <$> g <$> inr x)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
x : e ⊕ α_1
y : e ⊕ β_1
inl : ∀ (x : e), Eq (α := e ⊕ α_1) (Sum.inl x <* y) (Function.const β_1 <$> Sum.inl x <*> y)
inr : ∀ (x : α_1), Eq (α := e ⊕ α_1) (Sum.inr x <* y) (Function.const β_1 <$> Sum.inr x <*> y)
⊢ x <* y = Function.const β_1 <$> x <*> y

Tactic:
casesm Sum _ _

Premises used: Sum
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : e
⊢ Eq (α := e ⊕ α_1) (inl x <* y) (Function.const β_1 <$> inl x <*> y)

Tactic:
rfl
-- Module: Mathlib.Control.Basic
Goal:
α β γ : Type u
e : Type v
α_1 β_1 : Type u
y : e ⊕ β_1
x : α_1
⊢ Eq (α := e ⊕ α_1) (inr x <* y) (Function.const β_1 <$> inr x <*> y)

Tactic:
rfl