awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.Applicative (hypothesis)
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 β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L2 : LawfulApplicative F
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_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_1 : ∀ {α β : 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
toLawfulFunctor : 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 : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have seq_assoc : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
Tactic: obtain ⟨seqLeft_eq2, seqRight_eq2, pure_seq2, -⟩ := L2
Cleared hypotheses: L2
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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 β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
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 : 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
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
⊢ F1 = F2
have a : ∀ (α β : Type u) (f : α → β) (x : F α), f <$> x = f <$> x
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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 β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
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 : 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
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F2, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have obtain : ∀ (H1 : ∀ {α : Type u} (x : α), Eq.{u_1 + 1} (α := F α) (pure x) (pure x))
  (H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x) [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),
  (∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun (h : α → β) ↦ h x) <$> g) →
    (∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x) →
      Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
        { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
Tactic: obtain rfl : F1 = F2 := by
      apply Functor.ext
      intros
      exact (pure_seq1 _ _).symm.trans (pure_seq2 _ _)
Cleared hypotheses: F2, H1, H2, toLawfulFunctor_1, seqLeft_eq2, seqRight_eq2, pure_seq2, seq_pure_1, seq_assoc_1
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have e_toSeqLeft : @sl1 = @sl2
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
e_toSeqLeft : @sl1 = @sl2
⊢ Eq (α := Applicative F) { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl1, seqRight := sr1 }
    { toFunctor := F1, pure := p1, seq := s1, seqLeft := sl2, seqRight := sr2 }
have e_toSeqRight : @sr1 = @sr2
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ @sl1 = @sl2
have e_toSeqLeft : ∀ (α β : Type u) (x : F α) (y : Unit → F β), sl1 x y = sl2 x y
Tactic: funext α β x y
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ @sr1 = @sr2
have e_toSeqRight : ∀ (α β : Type u) (x : F α) (y : Unit → F β), sr1 x y = sr2 x y
Tactic: funext α β x y
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
Goal:
F : Type u_1 → Type u_2
AF : Applicative F
inst : LawfulApplicative F
α β : Type u_1
f : F (α → β)
x : F α
⊢ id <$> f <*> x = f <*> x
have rw : f <*> x = f <*> x
Tactic: rw [id_map]
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ Eq (α := Comp f g (α_1 × β_1)) (Prod.mk <$> x <*> x_1) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x_1 <*> x)
have 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))
Tactic: simp! [map, Seq.seq]
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ 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))
have 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))
Tactic: rw [commutative_map]
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ 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))
have 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)
Tactic: simp only [mk, flip, seq_map_assoc, Function.comp_def, map_map]
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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
⊢ 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
have 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)
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Control.Applicative (goal)
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)) (Prod.mk <$> y <*> x) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)
have e_a : Eq (α := g (α_1 × β_1)) (flip Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> x <*> y)
Tactic: rw [commutative_map]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> f <$> y = (fun (x : α → β) ↦ x ∘ f) <$> x <*> y
have simp : x <*> (pure f <*> y) = (pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y
Tactic: simp only [← pure_seq]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ x <*> (pure f <*> y) = (pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y
have simp : Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y)
  ((pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y)
Tactic: simp only [seq_assoc, seq_pure, ← comp_map]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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)
    ((pure fun (x : α → β) ↦ x ∘ f) <*> x <*> y)
have simp : Eq (α := F β) (((fun (h : (γ → α) → γ → β) ↦ h f) ∘ Function.comp) <$> x <*> y) ((fun (x : α → β) ↦ x ∘ f) <$> x <*> y)
Tactic: simp [pure_seq]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
F : Type u → Type v
inst : Applicative F
inst_1 : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ f <$> (x <*> y) = (fun (x : α → β) ↦ f ∘ x) <$> x <*> y
have simp : Eq.{v + 1} (α := F γ) (pure f <*> (x <*> y)) ((pure fun (x : α → β) ↦ f ∘ x) <*> x <*> y)
Tactic: simp only [← pure_seq]
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)
have map_const : ∀ {α β : Type u}, Eq (α := α → e ⊕ β → e ⊕ α) Functor.mapConst (Functor.map ∘ Function.const β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
map_const : ∀ {α β : Type u}, Eq (α := α → e ⊕ β → e ⊕ α) Functor.mapConst (Functor.map ∘ Function.const β)
⊢ LawfulFunctor (Sum e)
have id_map : ∀ {α : Type u} (x : e ⊕ α), id <$> x = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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
⊢ LawfulFunctor (Sum e)
have comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : e ⊕ α_1
⊢ id <$> x = x
have id_map : ∀ (x : e), Eq (α := e ⊕ α_1) (id <$> inl x) (inl x)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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 <$> x = x
have id_map₁ : ∀ (x : α_1), Eq (α := e ⊕ α_1) (id <$> inr x) (inr x)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 : Type u
x : e ⊕ α_1
⊢ id <$> x = x
have id_map : ∀ (x : e), Eq (α := e ⊕ α_1) (id <$> inl x) (inl x)
Tactic: try casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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 <$> x = x
have id_map₁ : ∀ (x : α_1), Eq (α := e ⊕ α_1) (id <$> inr x) (inr x)
Tactic: try casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : e ⊕ α_1
⊢ (h ∘ g) <$> x = h <$> g <$> x
have comp_map : ∀ (x : e), (h ∘ g) <$> inl x = h <$> g <$> inl x
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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
⊢ (h ∘ g) <$> x = h <$> g <$> x
have comp_map₁ : ∀ (x : α_1), Eq (α := e ⊕ γ_1) ((h ∘ g) <$> inr x) (h <$> g <$> inr x)
Tactic: casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
Goal:
α β γ : Type u
e : Type v
α_1 β_1 γ_1 : Type u
g : α_1 → β_1
h : β_1 → γ_1
x : e ⊕ α_1
⊢ (h ∘ g) <$> x = h <$> g <$> x
have comp_map : ∀ (x : e), (h ∘ g) <$> inl x = h <$> g <$> inl x
Tactic: try casesm Sum _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Basic (goal)
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
⊢ (h ∘ g) <$> x = h <$> g <$> x
have comp_map₁ : ∀ (x : α_1), Eq (α := e ⊕ γ_1) ((h ∘ g) <$> inr x) (h <$> g <$> inr x)
Tactic: try casesm Sum _ _
Cleared hypotheses: x