awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Free
Goal:
α_1 β_1 : Type u
m : Type u → Type u
inst : Applicative m
F : α_1 → m β_1
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
η : ApplicativeTransformation F_1 G
α β : Type u
f : α → F_1 β
x_1 x y : FreeMagma α
ih1 :
  Eq (α := G (FreeMagma β)) ((fun {α : Type u} ↦ η.app α) (traverse f x))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) x)
ih2 :
  Eq (α := G (FreeMagma β)) ((fun {α : Type u} ↦ η.app α) (traverse f y))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) y)
⊢ Eq (α := G (FreeMagma β)) ((fun {α : Type u} ↦ η.app α) (traverse f (x * y)))
    (traverse ((fun {α : Type u} ↦ η.app α) ∘ f) (x * y))

Tactic:
simp only [traverse_mul, functor_norm, ih1, ih2]

Premises used: FreeMagma.traverse_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x : FreeMagma α
⊢ 0 < x.length

Tactic:
match x with
  | FreeMagma.of _ => Nat.succ_pos 0
  | mul y z => Nat.add_pos_left (length_pos y) z.length

Premises used: Nat.add_pos_left, FreeMagma.length, Nat.succ_pos, LT.lt, OfNat.ofNat, _private.0.FreeMagma.length_pos.match_1
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y z : α
⊢ Quot.mk (AssocRel α) (x * y * z) = Quot.mk (AssocRel α) (x * (y * z))

Tactic:
Quot.sound (AssocRel.intro _ _ _)

Premises used: Quot.sound, Magma.AssocRel.intro
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y z w : α
⊢ Quot.mk (AssocRel α) (x * (y * z * w)) = Quot.mk (AssocRel α) (x * (y * (z * w)))

Tactic:
Quot.sound (AssocRel.left _ _ _ _)

Premises used: Quot.sound, Magma.AssocRel.left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
refine_1 :
  ∀ (a b₁ b₂ : α),
    AssocRel α b₁ b₂ →
      Eq.{u + 1} (α := AssocQuotient α) ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₁)
        ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a b₂)
refine_2 :
  ∀ (a₁ a₂ b : α),
    AssocRel α a₁ a₂ →
      Eq.{u + 1} (α := AssocQuotient α) ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a₁ b)
        ((fun (x y : α) ↦ Quot.mk (AssocRel α) (x * y)) a₂ b)
⊢ AssocQuotient α

Tactic:
refine Quot.liftOn₂ x y (fun x y ↦ Quot.mk _ (x * y)) ?_ ?_

Premises used: HMul.hMul, Quot.liftOn₂, Quot.mk
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
a c d e : α
⊢ Quot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))

Tactic:
quot_mk_assoc_left _ _ _ _

Premises used: Magma.AssocQuotient, Magma.AssocQuotient.quot_mk_assoc_left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
a c d e : α
⊢ Quot.mk (AssocRel α) (a * (c * d * e)) = Quot.mk (AssocRel α) (a * (c * (d * e)))

Tactic:
exact quot_mk_assoc_left _ _ _ _

Premises used: Magma.AssocQuotient.quot_mk_assoc_left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
a c d e f : α
refine_1 : Quot.mk (AssocRel α) (a * c * (d * e * f)) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
refine_1₁ : Quot.mk (AssocRel α) (a * c * (d * (e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
refine_1₂ refine_1₃ : Quot.mk (AssocRel α) (a * (c * (d * (e * f)))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))
⊢ Quot.mk (AssocRel α) (a * (c * (d * e * f))) = Quot.mk (AssocRel α) (a * (c * (d * (e * f))))

Tactic:
rw [← quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc]

Premises used: Magma.AssocQuotient.quot_mk_assoc, Magma.AssocQuotient.quot_mk_assoc_left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e : α
⊢ Quot.mk (AssocRel α) (c * d * e * b) = Quot.mk (AssocRel α) (c * (d * e) * b)

Tactic:
simp only [quot_mk_assoc, quot_mk_assoc_left]

Premises used: Magma.AssocQuotient.quot_mk_assoc, Magma.AssocQuotient.quot_mk_assoc_left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
x y : AssocQuotient α
b c d e f : α
refine_2 : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)
refine_2₁ : Quot.mk (AssocRel α) (c * (d * e * f * b)) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₂ : Quot.mk (AssocRel α) (c * (d * e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₃ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f) * b))
refine_2₄ : Quot.mk (AssocRel α) (c * (d * (e * (f * b)))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
refine_2₅ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * (d * (e * f * b)))
refine_2₆ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * f * b))
refine_2₇ refine_2₈ : Quot.mk (AssocRel α) (c * d * (e * (f * b))) = Quot.mk (AssocRel α) (c * d * (e * (f * b)))
⊢ Quot.mk (AssocRel α) (c * (d * e * f) * b) = Quot.mk (AssocRel α) (c * (d * (e * f)) * b)

Tactic:
rw [quot_mk_assoc, quot_mk_assoc, quot_mk_assoc_left, quot_mk_assoc_left,
          quot_mk_assoc_left, ← quot_mk_assoc c d, ← quot_mk_assoc c d, quot_mk_assoc_left]

Premises used: Magma.AssocQuotient.quot_mk_assoc, Magma.AssocQuotient.quot_mk_assoc_left
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
C : AssocQuotient α → Prop
x : AssocQuotient α
ih : ∀ (x : α), C ((of : (a : α) → AssocQuotient α) x)
⊢ C x

Tactic:
Quot.induction_on x ih

Premises used: Quot.induction_on
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f g : MulHom.{u, v} (AssocQuotient α) β
h : f.comp of = g.comp of
⊢ f = g

Tactic:
(DFunLike.ext _ _) fun x => AssocQuotient.induction_on x <| DFunLike.congr_fun h

Premises used: DFunLike.ext, Magma.AssocQuotient.induction_on
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f_1 f : α →ₙ* β
x : AssocQuotient α
c d e : α
⊢ Eq.{v + 1} (α := β) ((f : (a : α) → β) (c * d * e) : β) ((f : (a : α) → β) (c * (d * e)) : β)

Tactic:
simp only [map_mul, mul_assoc]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f_1 f_2 : α →ₙ* β
x : AssocQuotient α
c d e f : α
⊢ Eq.{v + 1} (α := β) ((f_2 : (a : α) → β) (c * (d * e * f)) : β) ((f_2 : (a : α) → β) (c * (d * (e * f))) : β)

Tactic:
simp only [map_mul, mul_assoc]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f : α →ₙ* β
x : α
⊢ Eq.{v + 1} (α := β)
    ((((lift : (a : α →ₙ* β) → AssocQuotient α →ₙ* β) f : MulHom.{u, v} (AssocQuotient α) β) :
          (a : AssocQuotient α) → β)
        ((of : (a : α) → AssocQuotient α) x : AssocQuotient α) :
      β)
    ((f : (a : α) → β) x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f : α →ₙ* β
⊢ MulHom.comp ((lift : (a : α →ₙ* β) → AssocQuotient α →ₙ* β) f) of = f

Tactic:
lift.symm_apply_apply f

Premises used: Equiv.symm_apply_apply, Magma.AssocQuotient.lift
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Semigroup β
f : MulHom.{u, v} (AssocQuotient α) β
⊢ (lift : (a : α →ₙ* β) → AssocQuotient α →ₙ* β) (f.comp of) = f

Tactic:
lift.apply_symm_apply f

Premises used: Equiv.apply_symm_apply, Magma.AssocQuotient.lift
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
inst : Mul α
β : Type v
inst_1 : Mul β
f : α →ₙ* β
x : α
⊢ Eq (α := AssocQuotient β)
    ((map f : (a : AssocQuotient α) → AssocQuotient β) ((of : (a : α) → AssocQuotient α) x) : AssocQuotient β)
    ((of : (a : β) → AssocQuotient β) ((f : (a : α) → β) x) : AssocQuotient β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x y : FreeSemigroup α
⊢ (x * y).head = x.head

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x y : FreeSemigroup α
⊢ (x * y).tail = x.tail ++ y.head :: y.tail

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x y : α
L1 L2 : List α
⊢ { head := x, tail := L1 : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α } =
    { head := x, tail := L1 ++ y :: L2 }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x y : FreeSemigroup α
⊢ (x * y).length = x.length + y.length

Tactic:
simp [length, Nat.add_right_comm]

Premises used: FreeSemigroup.length, Nat.add_right_comm
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
x : α
⊢ (of x).length = 1

Tactic:
rfl

Premises used: FreeSemigroup.length, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Mul β
f g : MulHom.{u, v} (FreeSemigroup α) β
h : Eq (α := α → β) ((⇑f : (a : FreeSemigroup α) → β) ∘ of) ((⇑g : (a : FreeSemigroup α) → β) ∘ of)
x_1 : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : Eq.{v + 1} (α := β) ((f : (a : FreeSemigroup α) → β) (of x) : β) ((g : (a : FreeSemigroup α) → β) (of x) : β)
hy : Eq.{v + 1} (α := β) ((f : (a : FreeSemigroup α) → β) y : β) ((g : (a : FreeSemigroup α) → β) y : β)
⊢ Eq.{v + 1} (α := β) ((f : (a : FreeSemigroup α) → β) (of x * y) : β) ((g : (a : FreeSemigroup α) → β) (of x * y) : β)

Tactic:
simp only [map_mul, *]

Premises used: map_mul
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f_1 f : α → β
⊢ ∀ (x y : FreeSemigroup α),
    List.foldl (fun (a : β) (b : α) ↦ a * f b) (f (x * y).head) (x * y).tail =
      List.foldl (fun (a : β) (b : α) ↦ a * f b) (f x.head) x.tail *
        List.foldl (fun (a : β) (b : α) ↦ a * f b) (f y.head) y.tail

Tactic:
simp [← List.foldl_map, List.foldl_assoc]

Premises used: List.foldl_map, List.foldl_assoc
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
x : α
xs : List α
⊢ (((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
      { head := x, tail := xs : FreeSemigroup α } =
    List.foldl (fun (x1 : β) (x2 : α) ↦ x1 * f x2) (f x) xs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
x : α
⊢ (((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
      (of x) =
    f x

Tactic:
rfl

Premises used: List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
⊢ (⇑((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β) ∘
      of =
    f

Tactic:
rfl

Premises used: List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : MulHom.{u, v} (FreeSemigroup α) β
⊢ (lift : (a : α → β) → FreeSemigroup α →ₙ* β) ((⇑f : (a : FreeSemigroup α) → β) ∘ of) = f

Tactic:
hom_ext rfl

Premises used: FreeSemigroup.hom_ext, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
inst : Semigroup β
f : α → β
x : α
y : FreeSemigroup α
rw :
  HMul.hMul (α := β) (β := β)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          (of x) :
        β)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)
rw₁ rw₂ :
  HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)
⊢ (((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) : (a : FreeSemigroup α) → β)
      (of x * y) =
    HMul.hMul (β := β) (f x)
      ((((lift : (a : α → β) → FreeSemigroup α →ₙ* β) f : MulHom.{u, v} (FreeSemigroup α) β) :
            (a : FreeSemigroup α) → β)
          y :
        β)

Tactic:
rw [map_mul, lift_of]

Premises used: map_mul, FreeSemigroup.lift_of
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
x : α
⊢ (map f : (a : FreeSemigroup α) → FreeSemigroup β) (of x) = of (f x)

Tactic:
rfl

Premises used: FreeSemigroup.of, List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α : Type u
β : Type v
f : α → β
x_1 : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : length.{v} (α := β) ((map f : (a : FreeSemigroup α) → FreeSemigroup β) (of x)) = (of x).length
hy : length.{v} (α := β) ((map f : (a : FreeSemigroup α) → FreeSemigroup β) y) = y.length
⊢ length.{v} (α := β) ((map f : (a : FreeSemigroup α) → FreeSemigroup β) (of x * y)) = (of x * y).length

Tactic:
simp only [map_mul, length_mul, *]

Premises used: map_mul, FreeSemigroup.length_mul
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x : α
⊢ Eq (α := FreeSemigroup β) (f <$> pure x) (pure (f x))

Tactic:
rfl

Premises used: FreeSemigroup.of, List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x y : FreeSemigroup α
⊢ f <$> (x * y) = f <$> x * f <$> y

Tactic:
map_mul (map f) _ _

Premises used: map_mul, FreeSemigroup.map
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → FreeSemigroup β
x : α
⊢ pure x >>= f = f x

Tactic:
rfl

Premises used: List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → FreeSemigroup β
x y : FreeSemigroup α
⊢ x * y >>= f = (x >>= f) * (y >>= f)

Tactic:
map_mul (lift f) _ _

Premises used: FreeSemigroup.lift, map_mul, DFunLike.coe
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f : α → β
x : FreeSemigroup α
⊢ pure f <*> x = f <$> x

Tactic:
rfl

Premises used: List.foldl, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
f g : FreeSemigroup (α → β)
x : FreeSemigroup α
⊢ f * g <*> x = (f <*> x) * (g <*> x)

Tactic:
mul_bind _ _ _

Premises used: FreeSemigroup.mul_bind
-- Module: Mathlib.Algebra.Free
Goal:
α β α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := FreeSemigroup α_1) (id <$> pure x) (pure x)
ih2 : id <$> y = y
rw : id <$> pure x * id <$> y = pure x * y
rw₁ : pure x * id <$> y = pure x * y
rw₂ rw₃ : pure x * y = pure x * y
⊢ id <$> (pure x * y) = pure x * y

Tactic:
rw [map_mul', ih1, ih2]

Premises used: FreeSemigroup.map_mul'
-- Module: Mathlib.Algebra.Free
Goal:
α β α_1 β_1 γ : Type u
x_1 : FreeSemigroup α_1
g : α_1 → FreeSemigroup β_1
f : β_1 → FreeSemigroup γ
x : α_1
y : FreeSemigroup α_1
ih1 : pure x >>= g >>= f = pure x >>= fun (x : α_1) ↦ g x >>= f
ih2 : y >>= g >>= f = y >>= fun (x : α_1) ↦ g x >>= f
rw : (pure x >>= g) * (y >>= g) >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₁ : (pure x >>= g >>= f) * (y >>= g >>= f) = pure x * y >>= fun (x : α_1) ↦ g x >>= f
rw₂ :
  (pure x >>= g >>= f) * (y >>= g >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
rw₃ :
  (pure x >>= fun (x : α_1) ↦ g x >>= f) * (y >>= g >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
rw₄ rw₅ :
  HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f) =
    HMul.hMul (α := FreeSemigroup γ) (pure x >>= fun (x : α_1) ↦ g x >>= f) (y >>= fun (x : α_1) ↦ g x >>= f)
⊢ pure x * y >>= g >>= f = pure x * y >>= fun (x : α_1) ↦ g x >>= f

Tactic:
rw [mul_bind, mul_bind, mul_bind, ih1, ih2]

Premises used: FreeSemigroup.mul_bind
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
x : α
⊢ Eq (α := m (FreeSemigroup β)) (traverse F (pure x)) (pure <$> F x)

Tactic:
rfl

Premises used: FreeSemigroup.recOnMul, FreeSemigroup.traverse, FreeSemigroup.recOnPure, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
⊢ Eq (α := α → m (FreeSemigroup β)) (traverse F ∘ pure) fun (x : α) ↦ pure <$> F x

Tactic:
rfl

Premises used: FreeSemigroup.recOnMul, FreeSemigroup.traverse, FreeSemigroup.recOnPure, rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
inst_1 : LawfulApplicative m
x_1 y_1 : FreeSemigroup α
x_2 : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α }) =
      (fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := x, tail := tl : FreeSemigroup α } <*>
        traverse F { head := y, tail := L2 }
x : α
rw :
  Eq (α := m (FreeSemigroup β))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := hd, tail := tl : FreeSemigroup α } <*>
        traverse F { head := y, tail := L2 }))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$>
        ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 })
⊢ Eq (α := m (FreeSemigroup β))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*>
      traverse F ({ head := hd, tail := tl : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α }))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$>
        ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 })

Tactic:
rw [ih]
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
inst_1 : LawfulApplicative m
x_1 y_1 : FreeSemigroup α
x_2 : α
L1 : List α
y : α
L2 : List α
hd : α
tl : List α
ih :
  ∀ (x : α),
    traverse F ({ head := x, tail := tl : FreeSemigroup α } * { head := y, tail := L2 : FreeSemigroup α }) =
      (fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := x, tail := tl : FreeSemigroup α } <*>
        traverse F { head := y, tail := L2 }
x : α
⊢ Eq (α := m (FreeSemigroup β))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*>
      ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F { head := hd, tail := tl : FreeSemigroup α } <*>
        traverse F { head := y, tail := L2 }))
    ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$>
        ((fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> pure <$> F x <*> traverse F { head := hd, tail := tl }) <*>
      traverse F { head := y, tail := L2 })

Tactic:
simp only [Function.comp_def, (mul_assoc _ _ _).symm, functor_norm]

Premises used: mul_assoc, Function.comp_def, Eq.symm
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
inst_1 : LawfulApplicative m
⊢ Eq (α := FreeSemigroup α → FreeSemigroup α → m (FreeSemigroup β)) (Function.comp (traverse F) ∘ HMul.hMul)
    fun (x y : FreeSemigroup α) ↦ (fun (x1 x2 : FreeSemigroup β) ↦ x1 * x2) <$> traverse F x <*> traverse F y

Tactic:
funext fun x ↦ funext fun y ↦ traverse_mul F x y

Premises used: FreeSemigroup.traverse_mul, funext
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
x : FreeSemigroup α
⊢ FreeSemigroup.traverse F x = traverse F x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
α_1 : Type u
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x)) (pure (of x))
ih2 : Eq (α := Id (FreeSemigroup α_1)) (traverse pure y) (pure y)
rw :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> traverse pure (of x) <*> traverse pure y) (pure (of x * y))
rw₁ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> traverse pure y)
    (pure (of x * y))
rw₂ :
  Eq (α := Id (FreeSemigroup α_1)) ((fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x) <*> pure y)
    (pure (of x * y))
rw₃ :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$>
      (fun (x1 x2 : FreeSemigroup α_1) ↦ x1 * x2) <$> pure (of x))
    (pure (of x * y))
rw₄ :
  Eq (α := Id (FreeSemigroup α_1))
    ((fun (h : FreeSemigroup α_1 → FreeSemigroup α_1) ↦ h y) <$> pure fun (x2 : FreeSemigroup α_1) ↦ of x * x2)
    (pure (of x * y))
rw₅ rw₆ : Eq (α := Id (FreeSemigroup α_1)) (pure ((fun (x2 : FreeSemigroup α_1) ↦ of x * x2) y)) (pure (of x * y))
⊢ Eq (α := Id (FreeSemigroup α_1)) (traverse pure (of x * y)) (pure (of x * y))

Tactic:
rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]

Premises used: FreeSemigroup.traverse_mul, LawfulApplicative.seq_pure, LawfulApplicative.map_pure
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 : FreeSemigroup α_1
x : α_1
⊢ Eq (α := Functor.Comp G F_1 (FreeSemigroup γ)) (traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x))
    (Functor.Comp.mk (traverse f <$> traverse g (pure x)))

Tactic:
simp only [traverse_pure, functor_norm, Function.comp_def]

Premises used: FreeSemigroup.traverse_pure, Function.comp_def
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 :
  Eq (α := Functor.Comp G F_1 (FreeSemigroup γ)) (traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x))
    (Functor.Comp.mk (traverse f <$> traverse g (pure x)))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
rw :
  Eq (α := Functor.Comp G F_1 (FreeSemigroup γ))
    (Functor.Comp.mk
        ((fun (x : F_1 (FreeSemigroup γ)) ↦ (fun (x1 x2 : FreeSemigroup γ) ↦ x1 * x2) <$> x) <$>
          traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y))
    (Functor.Comp.mk
      (traverse f <$> ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y)))
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x * y) = Functor.Comp.mk (traverse f <$> traverse g (pure x * y))

Tactic:
rw [traverse_mul, ih1, ih2, traverse_mul, Functor.Comp.map_mk]

Premises used: FreeSemigroup.traverse_mul, Functor.Comp.map_mk
-- Module: Mathlib.Algebra.Free
Goal:
α β : Type u
m : Type u → Type u
inst : Applicative m
F : α → m β
F_1 G : Type u → Type u
inst_1 : Applicative F_1
inst_2 : Applicative G
inst_3 : LawfulApplicative F_1
inst_4 : LawfulApplicative G
α_1 β_1 γ : Type u
f : β_1 → F_1 γ
g : α_1 → G β_1
x_1 : FreeSemigroup α_1
x : α_1
y : FreeSemigroup α_1
ih1 :
  Eq (α := Functor.Comp G F_1 (FreeSemigroup γ)) (traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x))
    (Functor.Comp.mk (traverse f <$> traverse g (pure x)))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Eq (α := Functor.Comp G F_1 (FreeSemigroup γ))
    (Functor.Comp.mk
        ((fun (x : F_1 (FreeSemigroup γ)) ↦ (fun (x1 x2 : FreeSemigroup γ) ↦ x1 * x2) <$> x) <$>
          traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y))
    (Functor.Comp.mk
      (traverse f <$> ((fun (x1 x2 : FreeSemigroup β_1) ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y)))

Tactic:
simp only [Function.comp_def, functor_norm, traverse_mul]

Premises used: FreeSemigroup.traverse_mul, Function.comp_def