awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : X
m : FreeMonoid X
⊢ Eq.{u_1 + 1} (α := R)
    ((((MonoidHom.comp
                  (↑(AlgHom.comp (B := FreeAlgebra R X)
                        ((lift R : (a : X → R[FreeMonoid X]) → FreeAlgebra R X →ₐ[R] R[FreeMonoid X]) fun (x : X) ↦
                          (MonoidAlgebra.of R (FreeMonoid X) : (a : FreeMonoid X) → R[FreeMonoid X]) (FreeMonoid.of x))
                        ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X) :
                            (a : FreeMonoid X →* FreeAlgebra R X) → R[FreeMonoid X] →ₐ[R] FreeAlgebra R X)
                          ((FreeMonoid.lift : (a : X → FreeAlgebra R X) → FreeMonoid X →* FreeAlgebra R X) (ι R)))) :
                    R[FreeMonoid X] →* R[FreeMonoid X])
                  (MonoidAlgebra.of R (FreeMonoid X)) :
                (a : FreeMonoid X) → R[FreeMonoid X])
              (FreeMonoid.of x) :
            MonoidAlgebra.{u_1, u_2} R (FreeMonoid X)) :
          (a : FreeMonoid X) → R)
        m :
      R)
    ((((MonoidHom.comp (↑(AlgHom.id R (MonoidAlgebra.{u_1, u_2} R (FreeMonoid X))) : R[FreeMonoid X] →* R[FreeMonoid X])
                  (MonoidAlgebra.of R (FreeMonoid X)) :
                (a : FreeMonoid X) → R[FreeMonoid X])
              (FreeMonoid.of x) :
            MonoidAlgebra.{u_1, u_2} R (FreeMonoid X)) :
          (a : FreeMonoid X) → R)
        m :
      R)

Tactic:
simp
-- 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
w :
  ∀ (x : X),
    Eq (α := FreeAlgebra R X)
      (Function.comp (β := FreeAlgebra R X)
        (⇑(AlgHom.comp (B := MonoidAlgebra.{u_1, u_2} R (FreeMonoid X))
              ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X) :
                  (a : FreeMonoid X →* FreeAlgebra R X) → R[FreeMonoid X] →ₐ[R] FreeAlgebra R X)
                ((FreeMonoid.lift : (a : X → FreeAlgebra R X) → FreeMonoid X →* FreeAlgebra R X) (ι R)))
              ((lift R : (a : X → R[FreeMonoid X]) → FreeAlgebra R X →ₐ[R] R[FreeMonoid X]) fun (x : X) ↦
                (MonoidAlgebra.of R (FreeMonoid X) : (a : FreeMonoid X) → R[FreeMonoid X]) (FreeMonoid.of x))) :
          (a : FreeAlgebra R X) → FreeAlgebra R X)
        (ι R) x)
      (Function.comp (β := FreeAlgebra R X) (⇑(AlgHom.id R (FreeAlgebra R X)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
        (ι R) x)
⊢ Eq (α := FreeAlgebra R X →ₐ[R] FreeAlgebra R X)
    (AlgHom.comp (B := MonoidAlgebra.{u_1, u_2} R (FreeMonoid X))
      ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X) :
          (a : FreeMonoid X →* FreeAlgebra R X) → R[FreeMonoid X] →ₐ[R] FreeAlgebra R X)
        ((FreeMonoid.lift : (a : X → FreeAlgebra R X) → FreeMonoid X →* FreeAlgebra R X) (ι R)))
      ((lift R : (a : X → R[FreeMonoid X]) → FreeAlgebra R X →ₐ[R] R[FreeMonoid X]) fun (x : X) ↦
        (MonoidAlgebra.of R (FreeMonoid X) : (a : FreeMonoid X) → R[FreeMonoid X]) (FreeMonoid.of x)))
    (AlgHom.id R (FreeAlgebra R X))

Tactic:
ext
-- 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
x : X
⊢ Eq (α := FreeAlgebra R X)
    (Function.comp (β := FreeAlgebra R X)
      (⇑(AlgHom.comp (B := MonoidAlgebra.{u_1, u_2} R (FreeMonoid X))
            ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X) :
                (a : FreeMonoid X →* FreeAlgebra R X) → R[FreeMonoid X] →ₐ[R] FreeAlgebra R X)
              ((FreeMonoid.lift : (a : X → FreeAlgebra R X) → FreeMonoid X →* FreeAlgebra R X) (ι R)))
            ((lift R : (a : X → R[FreeMonoid X]) → FreeAlgebra R X →ₐ[R] R[FreeMonoid X]) fun (x : X) ↦
              (MonoidAlgebra.of R (FreeMonoid X) : (a : FreeMonoid X) → R[FreeMonoid X]) (FreeMonoid.of x))) :
        (a : FreeAlgebra R X) → FreeAlgebra R X)
      (ι R) x)
    (Function.comp (β := FreeAlgebra R X) (⇑(AlgHom.id R (FreeAlgebra R X)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
      (ι R) x)

Tactic:
simp
-- 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
inst_3 : Nontrivial R
⊢ Nontrivial (FreeAlgebra R X)

Tactic:
equivMonoidAlgebraFreeMonoid.surjective.nontrivial

Premises used: Function.Surjective.nontrivial, FreeAlgebra.equivMonoidAlgebraFreeMonoid, AlgEquiv.surjective
-- 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
inst_3 : NoZeroDivisors R
⊢ NoZeroDivisors (FreeAlgebra R X)

Tactic:
equivMonoidAlgebraFreeMonoid.toMulEquiv.noZeroDivisors

Premises used: AlgEquiv.toMulEquiv, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MulEquiv.noZeroDivisors
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R_1 : Type u_1
X_1 : Type u_2
inst : CommSemiring R_1
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R_1 A
R : Type u_4
X : Type u_5
inst_3 : CommRing R
inst_4 : IsDomain R
⊢ IsDomain (FreeAlgebra R X)

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x : R
⊢ (algebraMapInv : (a : FreeAlgebra R X) → R)
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x y : R
⊢ Eq (α := FreeAlgebra R X) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X)
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) y : FreeAlgebra R X) ↔
    x = y

Tactic:
algebraMap_leftInverse.injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, FreeAlgebra.algebraMap_leftInverse
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x : R
⊢ Eq (α := FreeAlgebra R X) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X)
      (0 : FreeAlgebra R X) ↔
    x = 0

Tactic:
map_eq_zero_iff (algebraMap _ _) algebraMap_leftInverse.injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_zero_iff, FreeAlgebra.algebraMap_leftInverse
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
x : R
⊢ Eq (α := FreeAlgebra R X) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X)
      (1 : FreeAlgebra R X) ↔
    x = 1

Tactic:
map_eq_one_iff (algebraMap _ _) algebraMap_leftInverse.injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_one_iff, FreeAlgebra.algebraMap_leftInverse
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x y : X
hoxy : Eq (α := FreeAlgebra R X) (ι R x) (ι R y)
⊢ ¬x = y → False

Tactic:
fun hxy : x ≠ y ↦
        let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0

Premises used: FreeAlgebra.lift_ι_apply, Eq.rec, if_pos, FreeAlgebra.lift, one_ne_zero, OfNat.ofNat, Eq.symm, Eq, if_neg, DFunLike.coe, rfl, Eq.trans, ite
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x y : X
hoxy : Eq (α := FreeAlgebra R X) (ι R x) (ι R y)
⊢ ¬x = y → False

Tactic:
exact fun hxy : x ≠ y ↦
        let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0

Premises used: FreeAlgebra.lift_ι_apply, Eq.rec, if_pos, FreeAlgebra.lift, one_ne_zero, OfNat.ofNat, Eq.symm, Eq, if_neg, DFunLike.coe, rfl, Eq.trans, ite
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x y : X
hoxy : Eq (α := FreeAlgebra R X) (ι R x) (ι R y)
⊢ ¬x = y → False

Tactic:
classical exact fun hxy : x ≠ y ↦
        let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
        have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
        have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
        have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
        one_ne_zero <| hfy1.symm.trans hfy0
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x y : X
⊢ Eq (α := FreeAlgebra R X) (ι R x) (ι R y) ↔ x = y

Tactic:
ι_injective.eq_iff

Premises used: Function.Injective.eq_iff, FreeAlgebra.ι_injective
-- Module: Mathlib.Algebra.FreeAlgebra
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
⊢ Eq.{u_1 + 1} (α := R) ((f0 : (a : FreeAlgebra R X) → R) (ι R x) : R) (0 : R)

Tactic:
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
-- Module: Mathlib.Algebra.FreeAlgebra
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)
⊢ Eq.{u_1 + 1} (α := R) ((f1 : (a : FreeAlgebra R X) → R) (ι R x) : R) (1 : R)

Tactic:
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
-- Module: Mathlib.Algebra.FreeAlgebra
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)
⊢ r = 0

Tactic:
rw [h, f0.commutes, Algebra.algebraMap_self_apply] at hf0

Premises used: Algebra.algebraMap_self_apply, AlgHom.commutes
-- Module: Mathlib.Algebra.FreeAlgebra
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)
hf0₁ : r = 0
⊢ Eq.{u_1 + 1} (α := R) ((f1 : (a : FreeAlgebra R X) → R) (ι R x) : R) (1 : R)

Tactic:
rw [h, f0.commutes, Algebra.algebraMap_self_apply] at hf0

Premises used: Algebra.algebraMap_self_apply, AlgHom.commutes
-- Module: Mathlib.Algebra.FreeAlgebra
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)
⊢ r = 1

Tactic:
rw [h, f1.commutes, Algebra.algebraMap_self_apply] at hf1

Premises used: Algebra.algebraMap_self_apply, AlgHom.commutes
-- Module: Mathlib.Algebra.FreeAlgebra
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 : r = 1
⊢ False

Tactic:
zero_ne_one (hf0.symm.trans hf1)

Premises used: zero_ne_one, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.FreeAlgebra
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 : r = 1
⊢ False

Tactic:
exact zero_ne_one (hf0.symm.trans hf1)

Premises used: zero_ne_one, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x : X
⊢ Ne (α := FreeAlgebra R X) (ι R x) 0

Tactic:
ι_ne_algebraMap x 0

Premises used: FreeAlgebra.ι_ne_algebraMap, OfNat.ofNat
-- Module: Mathlib.Algebra.FreeAlgebra
Goal:
R : Type u_1
X : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
x : X
⊢ Ne (α := FreeAlgebra R X) (ι R x) 1

Tactic:
ι_ne_algebraMap x 1

Premises used: FreeAlgebra.ι_ne_algebraMap, OfNat.ofNat
-- 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
let : motive a
⊢ motive a

Tactic:
let s : Subalgebra R (FreeAlgebra R X) :=
    { carrier := motive
      mul_mem' := mul _ _
      add_mem' := add _ _
      algebraMap_mem' := grade0 }
-- 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
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)
⊢ AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)

Tactic:
ext
-- 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
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:
simp [of]
-- 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
⊢ 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]
-- 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 : 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)
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)
⊢ motive a

Tactic:
rw [this]
-- 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 : 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
    (↑((((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:
Subtype.prop (lift R of a)

Premises used: Set.Mem, Subtype.prop, FreeAlgebra.lift, DFunLike.coe
-- 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 : 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
    (↑((((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 Subtype.prop (lift R of a)

Premises used: Subtype.prop, FreeAlgebra.lift, DFunLike.coe
-- 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 : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
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)
⊢ motive a

Tactic:
suffices a = lift R of a by
    rw [this]
    exact Subtype.prop (lift R of a)
-- 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 : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R : (a : X → ↥s) → FreeAlgebra R X →ₐ[R] ↥s) of)
⊢ ∀ (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

Premises used: AlgHom.coe_id, AlgHom.ext_iff, Subalgebra.coe_val, AlgHom.coe_comp, Function.comp_apply, id_eq
-- 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:
of_id a

Premises used: Set.Mem