awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ Eq.{u_2 + 1} (α := FreeMonoid β)
    (({
            toFun := fun (l : FreeMonoid α) ↦
              (ofList : (a : List β) → FreeMonoid β) (List.map f ((toList : (a : FreeMonoid α) → List α) l)),
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : FreeMonoid α) → FreeMonoid β)
        (({
              toFun := fun (l : FreeMonoid α₁) ↦
                (ofList : (a : List α) → FreeMonoid α) (List.map g ((toList : (a : FreeMonoid α₁) → List α₁) l)),
              map_one' := ⋯, map_mul' := ⋯ } :
            (a : FreeMonoid α₁) → FreeMonoid α)
          x) :
      FreeMonoid β)
    (({
            toFun := fun (l : FreeMonoid α₁) ↦
              (ofList : (a : List β) → FreeMonoid β) (List.map (f ∘ g) ((toList : (a : FreeMonoid α₁) → List α₁) l)),
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : FreeMonoid α₁) → FreeMonoid β)
        x :
      FreeMonoid β)

Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

Premises used: FreeMonoid.toList_ofList, OneHom.coe_mk, List.map_map, MonoidHom.coe_mk
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
xs : FreeMonoid α
⊢ (toList : (a : FreeMonoid β) → List β) ((map f : (a : FreeMonoid α) → FreeMonoid β) xs : FreeMonoid β) =
    List.map f ((toList : (a : FreeMonoid α) → List α) xs)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
⊢ Eq (α := FreeMonoid β) ((ofList : (a : List β) → FreeMonoid β) (List.map f xs) : FreeMonoid β)
    ((map f : (a : FreeMonoid α) → FreeMonoid β) ((ofList : (a : List α) → FreeMonoid α) xs) : FreeMonoid β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ ((lift : (a : α → FreeMonoid β) → FreeMonoid α →* FreeMonoid β) fun (x : α) ↦ of (f x)) = map f

Tactic:
hom_eq fun _ ↦ rfl

Premises used: rfl, FreeMonoid.hom_eq
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = (map g).comp (map f)

Tactic:
hom_eq fun _ ↦ rfl

Premises used: rfl, FreeMonoid.hom_eq
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α →* FreeMonoid α) (map id) (MonoidHom.id (FreeMonoid α))

Tactic:
hom_eq fun _ ↦ rfl

Premises used: rfl, FreeMonoid.hom_eq
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
x : FreeMonoid α
e : α ≃ β
⊢ (map (⇑e.symm : (a : β) → α) : (a : FreeMonoid β) → FreeMonoid α)
      ((map (⇑e : (a : α) → β) : (a : FreeMonoid α) → FreeMonoid β) x) =
    x

Tactic:
simp [map_map]

Premises used: FreeMonoid.map_map
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
x : FreeMonoid β
e : α ≃ β
⊢ (map (⇑e : (a : α) → β) : (a : FreeMonoid α) → FreeMonoid β)
      ((map (⇑e.symm : (a : β) → α) : (a : FreeMonoid β) → FreeMonoid α) x) =
    x

Tactic:
simp [map_map]

Premises used: FreeMonoid.map_map
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mp :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
      (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β) →
    Function.Surjective f
mpr :
  Function.Surjective f →
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
      (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
      (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β) ↔
    Function.Surjective f

Tactic:
constructor
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
mp : ∀ (b : FreeMonoid α) (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) b = of d), ∃ (a : α), f a = d
⊢ ∃ (a : α), f a = d

Tactic:
rcases fs (FreeMonoid.of d) with ⟨b, hb⟩

Premises used: FreeMonoid.of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
hb : (map f : (a : FreeMonoid α) → FreeMonoid β) 1 = of d
⊢ length.{u_2} (α := β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) = (of d).length

Tactic:
have H := congr_arg length hb
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
hb : (map f : (a : FreeMonoid α) → FreeMonoid β) 1 = of d
H : length.{u_2} (α := β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) = (of d).length
⊢ ∃ (a : α), f a = d

Tactic:
simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H

Premises used: Nat.zero_ne_one, FreeMonoid.length_of, map_one, FreeMonoid.length_one
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : (map f : (a : FreeMonoid α) → FreeMonoid β) (of head * a) = of d
⊢ HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d

Tactic:
simp only [map_mul, map_of] at hb

Premises used: map_mul, FreeMonoid.map_of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h_1 : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
h : f head = d
⊢ ∃ (a : α), f a = d

Tactic:
use head
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
⊢ (HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β)).length =
    (of d).length

Tactic:
have H := congr_arg length hb
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
H :
  (HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β)).length =
    (of d).length
⊢ Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)

Tactic:
simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H

Premises used: FreeMonoid.length_eq_zero, FreeMonoid.length_of, add_eq_left, FreeMonoid.length_mul
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
H : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
⊢ of (f head) = of d

Tactic:
rw [H, mul_one] at hb

Premises used: mul_one
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
H : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
hb₁ : of (f head) = of d
⊢ Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)

Tactic:
rw [H, mul_one] at hb

Premises used: mul_one
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : of (f head) = of d
H : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
⊢ f head = d

Tactic:
FreeMonoid.of_injective hb

Premises used: FreeMonoid.of_injective
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
head : α
a : FreeMonoid α
h : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d
hb : of (f head) = of d
H : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
⊢ f head = d

Tactic:
exact FreeMonoid.of_injective hb

Premises used: FreeMonoid.of_injective
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
d : β
b : FreeMonoid α
hb : (map f : (a : FreeMonoid α) → FreeMonoid β) b = of d
mp : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) 1 = of d), ∃ (a : α), f a = d
mp₁ :
  ∀ (head : α) (a : FreeMonoid α),
    (∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) a = of d), ∃ (a : α), f a = d) →
      ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) (of head * a) = of d), ∃ (a : α), f a = d
⊢ ∃ (a : α), f a = d

Tactic:
induction b using FreeMonoid.inductionOn' with
    | one =>
      have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
    | mul_of head _ _ =>
      simp only [map_mul, map_of] at hb
      use head
      have H := congr_arg length hb
      simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
      rw [H, mul_one] at hb
      exact FreeMonoid.of_injective hb

Premises used: Nat.zero_ne_one, FreeMonoid.length_eq_zero, map_mul, FreeMonoid.length_of, add_eq_left, map_one, FreeMonoid.length_mul, mul_one, FreeMonoid.length_one, FreeMonoid.map_of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
h : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) 1
⊢ ∃ (a : FreeMonoid α),
    Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)

Tactic:
use 1
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
head : β
tail : FreeMonoid β
ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail
⊢ ∃ (a : α), f a = head

Tactic:
specialize fs head
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
head : β
tail : FreeMonoid β
ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail
fs : ∃ (a : α), f a = head
mpr : ∀ (a : α), ∃ (a_1 : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 = of (f a) * tail
⊢ ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = of head * tail

Tactic:
rcases fs with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail
a : α
mpr :
  ∀ (b : FreeMonoid α),
    ∃ (a_1 : FreeMonoid α),
      (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 =
        HMul.hMul (β := FreeMonoid β) (of (f a)) ((map f : (a : FreeMonoid α) → FreeMonoid β) b : FreeMonoid β)
⊢ ∃ (a_1 : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 = of (f a) * tail

Tactic:
rcases ih with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
h :
  (map f : (a : FreeMonoid α) → FreeMonoid β) (of a * b) =
    HMul.hMul (β := FreeMonoid β) (of (f a)) ((map f : (a : FreeMonoid α) → FreeMonoid β) b : FreeMonoid β)
⊢ ∃ (a_1 : FreeMonoid α),
    (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 =
      HMul.hMul (β := FreeMonoid β) (of (f a)) ((map f : (a : FreeMonoid α) → FreeMonoid β) b : FreeMonoid β)

Tactic:
use FreeMonoid.of a * b

Premises used: FreeMonoid.of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : FreeMonoid α
⊢ (map f : (a : FreeMonoid α) → FreeMonoid β) (of a * b) =
    HMul.hMul (β := FreeMonoid β) (of (f a)) ((map f : (a : FreeMonoid α) → FreeMonoid β) b : FreeMonoid β)

Tactic:
rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
mpr :
  ∃ (a : FreeMonoid α),
    Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
mpr₁ :
  ∀ (head : β) (tail : FreeMonoid β) (ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail),
    ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = of head * tail
⊢ ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = d

Tactic:
induction d using FreeMonoid.inductionOn' with
  | one => use 1; rfl
  | mul_of head tail ih =>
    specialize fs head
    rcases fs with ⟨a, rfl⟩
    rcases ih with ⟨b, rfl⟩
    use FreeMonoid.of a * b
    rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : α
⊢ (of a).reverse = of a

Tactic:
rfl

Premises used: List.reverseAux, FreeMonoid.reverse, FreeMonoid.of, List.reverse, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a b : FreeMonoid α
⊢ (a * b).reverse = b.reverse * a.reverse

Tactic:
List.reverse_append

Premises used: FreeMonoid, FreeMonoid.reverse, List.reverse, List.reverse_append
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : FreeMonoid α
⊢ a.reverse.reverse = a

Tactic:
apply List.reverse_reverse

Premises used: List.reverse_reverse
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : FreeMonoid α
⊢ a.reverse.length = a.length

Tactic:
List.length_reverse

Premises used: List.length_reverse, FreeMonoid.reverse, List.reverse, FreeMonoid.length
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
α : Type u_6
β : Type u_7
e : α ≃ β
⊢ ∀ (x y : FreeMonoid α),
    (map (⇑e : (a : α) → β) : (a : FreeMonoid α) → FreeMonoid β) (x * y) =
      HMul.hMul (α := FreeMonoid β) (β := FreeMonoid β)
        ((map (⇑e : (a : α) → β) : (a : FreeMonoid α) → FreeMonoid β) x : FreeMonoid β)
        ((map (⇑e : (a : α) → β) : (a : FreeMonoid α) → FreeMonoid β) y : FreeMonoid β)

Tactic:
simp [map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_6
β : Type u_7
e : α ≃ β
a : α
⊢ Eq.{u_7 + 1} (α := FreeMonoid β) ((freeMonoidCongr e : (a : FreeMonoid α) → FreeMonoid β) (of a) : FreeMonoid β)
    (of ((e : (a : α) → β) a) : FreeMonoid β)

Tactic:
rfl

Premises used: List.map, FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_6
β : Type u_7
e : α ≃ β
b : β
⊢ Eq.{u_6 + 1} (α := FreeMonoid α) ((freeMonoidCongr e.symm : (a : FreeMonoid β) → FreeMonoid α) (of b) : FreeMonoid α)
    (of ((e.symm : (a : β) → α) b) : FreeMonoid α)

Tactic:
rfl

Premises used: List.map, FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
⊢ (toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) = FreeMonoid.of x

Tactic:
rfl

Premises used: List.foldl, FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
xs : List α
this :
  ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
⊢ Eq (α := FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := x, tail := xs : FreeSemigroup α } : FreeMonoid α)
    ((ofList : (a : List α) → FreeMonoid α) (x :: xs) : FreeMonoid α)

Tactic:
simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)

Premises used: FreeSemigroup.lift, List.foldl_map, FreeSemigroup.toFreeMonoid, FreeMonoid.of, FreeSemigroup.lift_mk_eq_foldl
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
xs : List α
suffices :
  ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
⊢ Eq (α := FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := x, tail := xs : FreeSemigroup α } : FreeMonoid α)
    ((ofList : (a : List α) → FreeMonoid α) (x :: xs) : FreeMonoid α)

Tactic:
suffices ∀ x : FreeMonoid α, (xs.map FreeMonoid.of).foldl (· * ·) x = x * ofList xs by
    simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of []) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) [] : FreeMonoid α)

Tactic:
grind [ofList_nil, ofList_cons]

Premises used: FreeMonoid.ofList_nil, FreeMonoid.ofList_cons
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x head : α
tail : List α
tail_ih :
  ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of tail) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) tail : FreeMonoid α)
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of (head :: tail)) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) (head :: tail) : FreeMonoid α)

Tactic:
grind [ofList_nil, ofList_cons]

Premises used: FreeMonoid.ofList_nil, FreeMonoid.ofList_cons
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
xs : List α
nil :
  ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of []) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) [] : FreeMonoid α)
cons :
  ∀ (head : α) (tail : List α),
    (∀ (x : FreeMonoid α),
        List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of tail) =
          HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) tail : FreeMonoid α)) →
      ∀ (x : FreeMonoid α),
        List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of (head :: tail)) =
          HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) (head :: tail) : FreeMonoid α)
⊢ ∀ (x : FreeMonoid α),
    List.foldl (fun (x1 x2 : FreeMonoid α) ↦ x1 * x2) x (List.map FreeMonoid.of xs) =
      HMul.hMul (β := FreeMonoid α) x ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)

Tactic:
induction xs with grind [ofList_nil, ofList_cons]

Premises used: FreeMonoid.ofList_nil, FreeMonoid.ofList_cons
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h :
  Eq (α := FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := x, tail := xs : FreeSemigroup α } : FreeMonoid α)
    ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) { head := y, tail := ys : FreeSemigroup α } : FreeMonoid α)
⊢ x :: xs = y :: ys

Tactic:
simp only [toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq] at h

Premises used: FreeSemigroup.toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h : x :: xs = y :: ys
⊢ { head := x, tail := xs : FreeSemigroup α } = { head := y, tail := ys }

Tactic:
simpa using h
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
⊢ Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
    (1 : FreeMonoid α)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : α
y : FreeSemigroup α
h :
  Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
    (1 : FreeMonoid α)
h_1 : Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α) (1 : FreeMonoid α)
⊢ Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x * y) : FreeMonoid α)
    (1 : FreeMonoid α)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeSemigroup α
ih1 :
  ∀ (x : α),
    Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
      (1 : FreeMonoid α)
ih2 :
  ∀ (x : α) (y : FreeSemigroup α),
    Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x) : FreeMonoid α)
        (1 : FreeMonoid α) →
      Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α)
          (1 : FreeMonoid α) →
        Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of x * y) : FreeMonoid α)
          (1 : FreeMonoid α)
⊢ Ne (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) x : FreeMonoid α) (1 : FreeMonoid α)

Tactic:
induction x with simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
⊢ Eq.{u_1 + 1} (α := FreeMonoid α) 1 1 ∨
    ∃ (y : FreeSemigroup α),
      Eq (α := FreeMonoid α) ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α) (1 : FreeMonoid α)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
b : α
⊢ (toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of b) = FreeMonoid.of b * 1

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
b : α
⊢ FreeMonoid.of b * 1 = 1 ∨
    ∃ (y : FreeSemigroup α), (toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y = FreeMonoid.of b * 1

Tactic:
exact Or.inr ⟨of b, by simp⟩

Premises used: Or.inr
-- Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup
Goal:
α : Type u_1
x : FreeMonoid α
b : α
y : FreeSemigroup α
⊢ (toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) (of b * y) =
    HMul.hMul (β := FreeMonoid α) (FreeMonoid.of b)
      ((toFreeMonoid : (a : FreeSemigroup α) → FreeMonoid α) y : FreeMonoid α)

Tactic:
simp