awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (hypothesis)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x : X
r : R
h : Eq (α := FreeAlgebra R X) (ι R x) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
f0 : FreeAlgebra R X →ₐ[R] R := (lift R : (a : X → R) → FreeAlgebra R X →ₐ[R] R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R : (a : X → R) → FreeAlgebra R X →ₐ[R] R) 1
hf0 : Eq.{u_1 + 1} (α := R) ((f0 : (a : FreeAlgebra R X) → R) (ι R x) : R) (0 : R)
hf1 : Eq.{u_1 + 1} (α := R) ((f1 : (a : FreeAlgebra R X) → R) (ι R x) : R) (1 : R)
⊢ False
have hf0₁ : r = 0
Tactic: rw [h, f0.commutes, Algebra.algebraMap_self_apply] at hf0
Cleared hypotheses: hf0, hf1
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (hypothesis)
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x : X
r : R
h : Eq (α := FreeAlgebra R X) (ι R x) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
f0 : FreeAlgebra R X →ₐ[R] R := (lift R : (a : X → R) → FreeAlgebra R X →ₐ[R] R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R : (a : X → R) → FreeAlgebra R X →ₐ[R] R) 1
hf0 : r = 0
hf1 : Eq.{u_1 + 1} (α := R) ((f1 : (a : FreeAlgebra R X) → R) (ι R x) : R) (1 : R)
⊢ False
have hf1₁ : r = 1
Tactic: rw [h, f1.commutes, Algebra.algebraMap_self_apply] at hf1
Cleared hypotheses: hf1
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
have w : ∀ (x : X),
  Eq (α := FreeAlgebra R X)
    (Function.comp (β := FreeAlgebra R X) (⇑(AlgHom.id R (FreeAlgebra R X)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
      (ι R) x)
    (Function.comp (β := FreeAlgebra R X)
      (⇑(s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
      (ι R) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (hypothesis)
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
⊢ motive a
have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
Tactic: have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) := by
    ext
    simp [of]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
this :
  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)
⊢ motive a
have rw : motive
  (↑((((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: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
⊢ motive a
have suffices : 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: suffices a = lift R of a by
    rw [this]
    exact Subtype.prop (lift R of a)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (hypothesis)
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 : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
⊢ 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)
have 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)
Tactic: simp only [AlgHom.ext_iff, AlgHom.coe_id, id_eq, AlgHom.coe_comp, Subalgebra.coe_val,
    Function.comp_apply] at of_id
Cleared hypotheses: of_id
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 = ⊤
have refine : ∀ (x : FreeAlgebra R X) (hx : Membership.mem (γ := Subalgebra R (FreeAlgebra R X)) ⊤ x), x ∈ S
Tactic: refine top_unique fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ x ∈ S
have grade0 : ∀ (r : R),
  Membership.mem (α := FreeAlgebra R X) S
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)
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 _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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)
⊢ x ∈ S
have add : ∀ (x y : FreeAlgebra R X) (hx : x ∈ S) (hy : y ∈ S), x + y ∈ 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 _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ x ∈ S
have mul : ∀ (x y : FreeAlgebra R X) (hx : x ∈ S) (hy : y ∈ S), x * y ∈ 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 _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ x ∈ S
have grade1 : ∀ (x : X), ι R 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 _)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
s : Set A
⊢ 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))))
have 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))))
Tactic: rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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))))
⊢ 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))))
have rw₁ : Eq (α := Subalgebra R A) (Algebra.adjoin R s) (Algebra.adjoin R s)
Tactic: rw [← Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
xs : List (FreeMonoid α)
⊢ Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) xs.prod : List α)
    (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) xs) : List α)
have nil : Eq.{u_1 + 1} (α := List α) ((toList : (a : FreeMonoid α) → List α) (List.prod []) : List α)
  (List.flatten (List.map (α := FreeMonoid α) (⇑toList : (a : FreeMonoid α) → List α) []) : List α)
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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 α)
⊢ Eq (α := List α) ((toList : (a : FreeMonoid α) → List α) xs.prod : List α)
    (List.flatten (List.map (⇑toList : (a : FreeMonoid α) → List α) xs) : List α)
have 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 α)
Tactic: induction xs
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
Goal:
α : Type u_1
a : α
h : of a = 1
⊢ False
have this : (of a).length = length.{u_1} (α := α) 1
Tactic: have := congrArg FreeMonoid.length h
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Monoid M
N : Type u_5
inst_1 : Monoid N
g : M →* N
f : α → M
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
      (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β) ↔
    Function.Surjective f
have mp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β) →
  Function.Surjective f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
      (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β) ↔
    Function.Surjective f
have mpr : Function.Surjective f →
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := FreeMonoid α) (β := FreeMonoid β)
    (⇑(map f) : (a : FreeMonoid α) → FreeMonoid β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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 : β
⊢ ∃ (a : α), f a = d
have mp : ∀ (b : FreeMonoid α) (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) b = of d), ∃ (a : α), f a = d
Tactic: rcases fs (FreeMonoid.of d) with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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
⊢ ∃ (a : α), f a = d
have H : length.{u_2} (α := β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) = (of d).length
Tactic: have H := congr_arg length hb
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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
⊢ ∃ (a : α), f a = d
have hb₁ : HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) = of d
Tactic: simp only [map_mul, map_of] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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
⊢ ∃ (a : α), f a = d
have h : f head = d
Tactic: use head
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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
⊢ f head = d
have H : (HMul.hMul (β := FreeMonoid β) (of (f head)) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β)).length =
  (of d).length
Tactic: have H := congr_arg length hb
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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
⊢ f head = d
have H₁ : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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 β)
⊢ f head = d
have hb₁ : of (f head) = of d
Tactic: rw [H, mul_one] at hb
Cleared hypotheses: hb, H
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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
⊢ ∃ (a : α), f a = d
have mp : ∀ (hb : (map f : (a : FreeMonoid α) → FreeMonoid β) 1 = of 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
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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
⊢ ∃ (a : α), f a = d
have 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
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
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ ∃ (a : FreeMonoid α),
    Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
have h : Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) 1) 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (hypothesis)
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 : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = of head * tail
have fs₁ : ∃ (a : α), f a = head
Tactic: specialize fs head
Cleared hypotheses: fs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
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
⊢ ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = of head * tail
have mpr : ∀ (a : α), ∃ (a_1 : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 = of (f a) * tail
Tactic: rcases fs with ⟨a, rfl⟩
Cleared hypotheses: head, fs
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
tail : FreeMonoid β
ih : ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = tail
a : α
⊢ ∃ (a_1 : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a_1 = of (f a) * tail
have 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 β)
Tactic: rcases ih with ⟨b, rfl⟩
Cleared hypotheses: tail, ih
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
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 β)
have h : (map f : (a : FreeMonoid α) → FreeMonoid β) (of a * b) =
  HMul.hMul (β := FreeMonoid β) (of (f a)) ((map f : (a : FreeMonoid α) → FreeMonoid β) b : FreeMonoid β)
Tactic: use FreeMonoid.of a * b
-- Lean 4 proof step from Mathlib.Algebra.FreeMonoid.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
d : FreeMonoid β
⊢ ∃ (a : FreeMonoid α), (map f : (a : FreeMonoid α) → FreeMonoid β) a = d
have mpr : ∃ (a : FreeMonoid α),
  Eq.{u_2 + 1} (α := FreeMonoid β) ((map f : (a : FreeMonoid α) → FreeMonoid β) a : FreeMonoid β) (1 : FreeMonoid β)
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
Cleared hypotheses: d