awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := motive, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) (p := fun (x : FreeAlgebra R X) ↦ x ∈ s) grade1
of_id :
  ∀ (x : FreeAlgebra R X),
    x =
      (↑((((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of : FreeAlgebra R X →ₐ[R] ↥s) :
              (a : FreeAlgebra R X) → ↥s)
            x) :
        FreeAlgebra R X)
⊢ a =
    (↑((((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of : FreeAlgebra R X →ₐ[R] ↥s) : (a : FreeAlgebra R X) → ↥s)
          a) :
      FreeAlgebra R X)

Tactic:
exact of_id a
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
set :
  let S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R));
  S = ⊤
⊢ Eq (α := Subalgebra R (FreeAlgebra R X)) (Algebra.adjoin R (Set.range (ι R))) ⊤

Tactic:
set S := Algebra.adjoin R (Set.range (ι R : X → FreeAlgebra R X))

Premises used: FreeAlgebra.ι, Algebra.adjoin, Set.range
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
⊢ S = ⊤

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
refine : ∀ (x : FreeAlgebra R X) (hx : Membership.mem (γ := Subalgebra R (FreeAlgebra R X)) ⊤ x), x ∈ S
⊢ S = ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
r : R
⊢ Membership.mem (α := FreeAlgebra R X) S
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)

Tactic:
S.algebraMap_mem _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
r : R
⊢ Membership.mem (α := FreeAlgebra R X) S
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)

Tactic:
exact S.algebraMap_mem _

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
S.add_mem hx hy

Premises used: Set.Mem, Subalgebra.add_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
exact S.add_mem hx hy

Premises used: Subalgebra.add_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x * y ∈ S

Tactic:
S.mul_mem hx hy

Premises used: Subalgebra.mul_mem, Set.Mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x * y ∈ S

Tactic:
exact S.mul_mem hx hy

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : X
⊢ ι R x ∈ S

Tactic:
Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Set.Mem, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : X
⊢ ι R x ∈ S

Tactic:
exact Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x : FreeAlgebra R X
grade0 :
  ∀ (r : R),
    Membership.mem (α := FreeAlgebra R X) S
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)
add : ∀ (x y : FreeAlgebra R X) (hx : x ∈ S) (hy : y ∈ S), x + y ∈ S
mul : ∀ (x y : FreeAlgebra R X) (hx : x ∈ S) (hy : y ∈ S), x * y ∈ S
grade1 : ∀ (x : X), ι R x ∈ S
⊢ x ∈ S

Tactic:
induction x with
  | grade0 => exact S.algebraMap_mem _
  | add x y hx hy => exact S.add_mem hx hy
  | mul x y hx hy => exact S.mul_mem hx hy
  | grade1 x => exact Algebra.subset_adjoin (Set.mem_range_self _)

Premises used: Set.mem_range_self, Algebra.subset_adjoin, Subalgebra.algebraMap_mem
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
f : X → A
⊢ Eq (α := Subalgebra R A) (Algebra.adjoin R (Set.range f))
    (AlgHom.range (A := FreeAlgebra R X) ((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f))

Tactic:
simp only [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp,
    Function.comp_def, lift_ι_apply]

Premises used: Set.range_comp, FreeAlgebra.lift_ι_apply, AlgHom.map_adjoin, Function.comp_def, FreeAlgebra.adjoin_range_ι, Algebra.map_top
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
rw :
  Eq (α := Subalgebra R A) (Algebra.adjoin R s)
    (Algebra.adjoin R (Set.range (ι := { x : A // x ∈ s }) (Subtype.val (p := fun (x : A) ↦ x ∈ s))))
rw₁ rw₂ : Eq (α := Subalgebra R A) (Algebra.adjoin R s) (Algebra.adjoin R s)
⊢ Eq (α := Subalgebra R A) (Algebra.adjoin R s)
    (AlgHom.range (A := FreeAlgebra.{u_1, u_3} R { x : A // x ∈ s })
      ((lift R : (a : { x : A // x ∈ s } → A) → FreeAlgebra R { x : A // x ∈ s } →ₐ[R] A)
        (Subtype.val (p := fun (x : A) ↦ x ∈ s))))

Tactic:
rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]

Premises used: Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α ≃ FreeMonoid α) (Equiv.symm toList) ofList

Tactic:
rfl

Premises used: FreeMonoid, FreeMonoid.ofList, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α ≃ List α) (Equiv.symm ofList) toList

Tactic:
rfl

Premises used: FreeMonoid, FreeMonoid.toList, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
l : List α
⊢ (toList : (a : FreeMonoid α) → List α) ((ofList : (a : List α) → FreeMonoid α) l : FreeMonoid α) = l

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α → List α)
    (Function.comp (β := FreeMonoid α) (⇑toList : (a : FreeMonoid α) → List α) (⇑ofList : (a : List α) → FreeMonoid α))
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α → FreeMonoid α)
    (Function.comp (β := List α) (⇑ofList : (a : List α) → FreeMonoid α) (⇑toList : (a : FreeMonoid α) → List α)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) ((toList : (a : FreeMonoid α) → List α) 1 : List α) ([] : List α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α) ((ofList : (a : List α) → FreeMonoid α) [] : FreeMonoid α) (1 : FreeMonoid α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) ((toList : (a : FreeMonoid α) → List α) [] : List α) ([] : List α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
xs ys : FreeMonoid α
⊢ (toList : (a : FreeMonoid α) → List α) (xs * ys) =
    HAppend.hAppend (α := List α) (β := List α) ((toList : (a : FreeMonoid α) → List α) xs : List α)
      ((toList : (a : FreeMonoid α) → List α) ys : List α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
x : α
xs : FreeMonoid α
⊢ (toList : (a : FreeMonoid α) → List α) (x :: xs) = x :: (toList : (a : FreeMonoid α) → List α) xs

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
xs ys : List α
⊢ (ofList : (a : List α) → FreeMonoid α) (xs ++ ys) =
    HMul.hMul (α := FreeMonoid α) (β := FreeMonoid α) ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)
      ((ofList : (a : List α) → FreeMonoid α) ys : FreeMonoid α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
xs : List (FreeMonoid α)
nil :
  Eq.{u_1 + 1} (α := List α) ((toList : (a : FreeMonoid α) → List α) (List.prod []) : List α)
    (List.flatten (List.map (α := FreeMonoid α) (⇑toList : (a : FreeMonoid α) → List α) []) : List α)
cons :
  ∀ (head : FreeMonoid α) (tail : List (FreeMonoid α)),
    Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) tail.prod : List α)
        (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) tail) : List α) →
      Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) (head :: tail).prod : List α)
        (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) (head :: tail)) : List α)
⊢ Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) xs.prod : List α)
    (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) xs) : List α)

Tactic:
induction xs
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := List α) ((toList : (a : FreeMonoid α) → List α) (List.prod []) : List α)
    (List.flatten (List.map (α := FreeMonoid α) (⇑toList : (a : FreeMonoid α) → List α) []) : List α)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
head : FreeMonoid α
tail : List (FreeMonoid α)
tail_ih :
  Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) tail.prod : List α)
    (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) tail) : List α)
⊢ Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) (head :: tail).prod : List α)
    (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) (head :: tail)) : List α)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
xs : List (List α)
⊢ Eq (α := List α)
    ((toList : (a : FreeMonoid α) → List α) ((ofList : (a : List α) → FreeMonoid α) xs.flatten : FreeMonoid α) : List α)
    ((toList : (a : FreeMonoid α) → List α) (List.prod (List.map (⇑ofList : (a : List α) → FreeMonoid α) xs)) : List α)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
x : α
⊢ (toList : (a : FreeMonoid α) → List α) (of x) = [x]

Tactic:
rfl

Premises used: FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
x : α
⊢ (ofList : (a : List α) → FreeMonoid α) [x] = of x

Tactic:
rfl

Premises used: FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
x : α
xs : List α
⊢ (ofList : (a : List α) → FreeMonoid α) (x :: xs) =
    HMul.hMul (β := FreeMonoid α) (of x) ((ofList : (a : List α) → FreeMonoid α) xs : FreeMonoid α)

Tactic:
rfl

Premises used: List.append, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
x : α
xs : FreeMonoid α
⊢ (toList : (a : FreeMonoid α) → List α) (of x * xs) = x :: (toList : (a : FreeMonoid α) → List α) xs

Tactic:
rfl

Premises used: List.append, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := α) of

Tactic:
List.singleton_injective

Premises used: FreeMonoid, List.singleton_injective, FreeMonoid.of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
⊢ length.{u_1} (α := α) 1 = 0

Tactic:
rfl

Premises used: FreeMonoid.length, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : FreeMonoid α
⊢ a.length = 0 ↔ a = 1

Tactic:
List.length_eq_zero_iff

Premises used: FreeMonoid, FreeMonoid.length, List.length_eq_zero_iff
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
m : α
⊢ (of m).length = 1

Tactic:
rfl

Premises used: FreeMonoid.length, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : FreeMonoid α
⊢ a.length = 1 ↔ ∃ (m : α), a = of m

Tactic:
List.length_eq_one_iff

Premises used: FreeMonoid, List.length_eq_one_iff, FreeMonoid.of, FreeMonoid.length
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
v : FreeMonoid α
⊢ v.length = 2 ↔ ∃ (c : α), ∃ (d : α), v = of c * of d

Tactic:
List.length_eq_two

Premises used: FreeMonoid, List.append, FreeMonoid.of, List.length_eq_two, FreeMonoid.length
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
v : FreeMonoid α
⊢ v.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), v = of a * of b * of c

Tactic:
List.length_eq_three

Premises used: FreeMonoid, List.append, FreeMonoid.of, FreeMonoid.length, List.length_eq_three
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
v : FreeMonoid α
⊢ v.length = 4 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), ∃ (d : α), v = of a * of b * of c * of d

Tactic:
List.length_eq_four

Premises used: List.length_eq_four, FreeMonoid, List.append, FreeMonoid.of, FreeMonoid.length
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a b : FreeMonoid α
⊢ (a * b).length = a.length + b.length

Tactic:
List.length_append

Premises used: List.length_append, FreeMonoid.length
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : α
h : of a = 1
⊢ (of a).length = length.{u_1} (α := α) 1

Tactic:
have := congrArg FreeMonoid.length h
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : α
h : of a = 1
this : (of a).length = length.{u_1} (α := α) 1
⊢ False

Tactic:
simp only [length_of, length_one, Nat.succ_ne_self] at this

Premises used: Nat.succ_ne_self, FreeMonoid.length_of, FreeMonoid.length_one
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
a : α
⊢ 1 ≠ of a

Tactic:
of_ne_one _ |>.symm

Premises used: FreeMonoid.of_ne_one, Ne.symm
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
m : α
⊢ ¬Membership.mem (γ := FreeMonoid α) 1 m

Tactic:
List.not_mem_nil

Premises used: FreeMonoid.mem, List.not_mem_nil
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
m n : α
⊢ m ∈ of n ↔ m = n

Tactic:
List.mem_singleton

Premises used: List.mem_singleton, FreeMonoid.mem, FreeMonoid.of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
m : α
⊢ m ∈ of m

Tactic:
List.mem_singleton_self _

Premises used: List.mem_singleton_self, FreeMonoid.mem, FreeMonoid.of
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
m : α
a b : FreeMonoid α
⊢ m ∈ a * b ↔ m ∈ a ∨ m ∈ b

Tactic:
List.mem_append

Premises used: List.mem_append, FreeMonoid.mem
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
C : FreeMonoid α → Sort u_6
h0 : C 1
ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)
⊢ recOn (C := C) 1 h0 ih = h0

Tactic:
rfl

Premises used: FreeMonoid.recOn, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
C : FreeMonoid α → Sort u_6
x : α
xs : FreeMonoid α
h0 : C 1
ih : (x : α) → (xs : FreeMonoid α) → C xs → C (of x * xs)
⊢ (of x * xs).recOn (C := C) h0 ih = ih x xs (xs.recOn (C := fun (x : FreeMonoid α) ↦ C x) h0 ih)

Tactic:
rfl

Premises used: List.append, FreeMonoid.recOn, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
C : FreeMonoid α → Prop
z : FreeMonoid α
one : C 1
of : ∀ (x : α), C (FreeMonoid.of x)
mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)
⊢ C z

Tactic:
List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z

Premises used: List.rec
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
p : FreeMonoid α → Prop
a : FreeMonoid α
one : p 1
mul_of : ∀ (b : α) (a : FreeMonoid α), p a → p (of b * a)
⊢ p a

Tactic:
List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a

Premises used: List.rec
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
C : FreeMonoid α → Sort u_6
h0 : C 1
ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)
⊢ casesOn (C := C) 1 h0 ih = h0

Tactic:
rfl

Premises used: FreeMonoid.casesOn, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
C : FreeMonoid α → Sort u_6
x : α
xs : FreeMonoid α
h0 : C 1
ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)
⊢ (of x * xs).casesOn (C := C) h0 ih = ih x xs

Tactic:
rfl

Premises used: List.append, FreeMonoid.casesOn, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f g : MonoidHom.{u_1, u_4} (FreeMonoid α) M
h : ∀ (x : α), Eq.{u_4 + 1} (α := M) ((f : (a : FreeMonoid α) → M) (of x) : M) ((g : (a : FreeMonoid α) → M) (of x) : M)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : Eq.{u_4 + 1} (α := M) ((f : (a : FreeMonoid α) → M) xs : M) ((g : (a : FreeMonoid α) → M) xs : M)
⊢ Eq.{u_4 + 1} (α := M) ((f : (a : FreeMonoid α) → M) (of x * xs) : M) ((g : (a : FreeMonoid α) → M) (of x * xs) : M)

Tactic:
simp only [h, hxs, map_mul]

Premises used: map_mul
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
M : Type u_4
inst : Monoid M
head : M
xs : List M
⊢ prodAux (head :: xs) = (head :: xs).prod

Tactic:
simp [prodAux, List.prod_eq_foldl]

Premises used: FreeMonoid.prodAux, List.prod_eq_foldl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
f : α → M
x x_1 : FreeMonoid α
⊢ prodAux (List.map f ((toList : (a : FreeMonoid α) → List α) (x * x_1))) =
    prodAux (List.map f ((toList : (a : FreeMonoid α) → List α) x)) *
      prodAux (List.map f ((toList : (a : FreeMonoid α) → List α) x_1))

Tactic:
simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append]

Premises used: List.prod_append, FreeMonoid.toList_mul, FreeMonoid.prodAux_eq, List.map_append
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
l : List α
⊢ (((lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_1, u_4} (FreeMonoid α) M) : (a : FreeMonoid α) → M)
      ((ofList : (a : List α) → FreeMonoid α) l : FreeMonoid α) =
    (List.map f l).prod

Tactic:
prodAux_eq _

Premises used: FreeMonoid.prodAux, FreeMonoid.prodAux_eq
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : MonoidHom.{u_1, u_4} (FreeMonoid α) M
⊢ Eq (α := α → M) ((Equiv.symm lift : (a : FreeMonoid α →* M) → α → M) f : α → M)
    ((⇑f : (a : FreeMonoid α) → M) ∘ of : α → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
l : FreeMonoid α
⊢ (((lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_1, u_4} (FreeMonoid α) M) : (a : FreeMonoid α) → M) l =
    (List.map f ((toList : (a : FreeMonoid α) → List α) l)).prod

Tactic:
prodAux_eq _

Premises used: FreeMonoid.prodAux, FreeMonoid.prodAux_eq
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
⊢ (⇑((lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_1, u_4} (FreeMonoid α) M) : (a : FreeMonoid α) → M) ∘
      of =
    f

Tactic:
rfl

Premises used: FreeMonoid.prodAux, List.foldl, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : α → M
x : α
⊢ (((lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_1, u_4} (FreeMonoid α) M) : (a : FreeMonoid α) → M)
      (of x) =
    f x

Tactic:
rfl

Premises used: FreeMonoid.prodAux, List.foldl, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
f : MonoidHom.{u_1, u_4} (FreeMonoid α) M
⊢ (lift : (a : α → M) → FreeMonoid α →* M) ((⇑f : (a : FreeMonoid α) → M) ∘ of) = f

Tactic:
lift.apply_symm_apply f

Premises used: FreeMonoid.lift, Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
g : M →* N
f : α → M
h :
  ∀ (x : α),
    Eq.{u_5 + 1} (α := N) ((g.comp ((lift : (a : α → M) → FreeMonoid α →* M) f) : (a : FreeMonoid α) → N) (of x) : N)
      ((((lift : (a : α → N) → FreeMonoid α →* N) ((⇑g : (a : M) → N) ∘ f) : MonoidHom.{u_1, u_5} (FreeMonoid α) N) :
            (a : FreeMonoid α) → N)
          (of x) :
        N)
⊢ Eq (α := MonoidHom.{u_1, u_5} (FreeMonoid α) N) (g.comp ((lift : (a : α → M) → FreeMonoid α →* M) f))
    ((lift : (a : α → N) → FreeMonoid α →* N) ((⇑g : (a : M) → N) ∘ f))

Tactic:
ext
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
g : M →* N
f : α → M
x : α
⊢ Eq.{u_5 + 1} (α := N) ((g.comp ((lift : (a : α → M) → FreeMonoid α →* M) f) : (a : FreeMonoid α) → N) (of x) : N)
    ((((lift : (a : α → N) → FreeMonoid α →* N) ((⇑g : (a : M) → N) ∘ f) : MonoidHom.{u_1, u_5} (FreeMonoid α) N) :
          (a : FreeMonoid α) → N)
        (of x) :
      N)

Tactic:
simp
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
g : M →* N
f : α → M
x : FreeMonoid α
⊢ Eq.{u_5 + 1} (α := N)
    ((g : (a : M) → N)
        ((((lift : (a : α → M) → FreeMonoid α →* M) f : MonoidHom.{u_1, u_4} (FreeMonoid α) M) : (a : FreeMonoid α) → M)
            x :
          M) :
      N)
    ((((lift : (a : α → N) → FreeMonoid α →* N) ((⇑g : (a : M) → N) ∘ f) : MonoidHom.{u_1, u_5} (FreeMonoid α) N) :
          (a : FreeMonoid α) → N)
        x :
      N)

Tactic:
DFunLike.ext_iff.1 (comp_lift g f) x

Premises used: FreeMonoid.comp_lift, DFunLike.ext_iff, Iff.mp
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l : FreeMonoid α
b : β
⊢ l • b = List.foldr f b ((toList : (a : FreeMonoid α) → List α) l)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
l : List α
b : β
⊢ HSMul.hSMul (α := FreeMonoid α) ((ofList : (a : List α) → FreeMonoid α) l : FreeMonoid α) b = List.foldr f b l

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β → β
x : α
y : β
⊢ of x • y = f x y

Tactic:
rfl

Premises used: List.foldr, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ (map f : (a : FreeMonoid α) → FreeMonoid β) (of x) = of (f x)

Tactic:
rfl

Premises used: List.map, FreeMonoid.of, rfl
-- Module: Mathlib.Algebra.FreeMonoid.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : FreeMonoid α
m : β
⊢ Membership.mem (γ := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) m ↔
    ∃ (n : α), n ∈ a ∧ f n = m

Tactic:
List.mem_map

Premises used: FreeMonoid.mem, List.mem_map