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
f : X → A
h :
  ∀ (x : X),
    (fun (F : FreeAlgebra R X →ₐ[R] A) ↦
          (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
        (liftAux R f) x =
      f x
⊢ (fun (F : FreeAlgebra R X →ₐ[R] A) ↦
        (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
      (liftAux R f) =
    f

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
f : X → A
x : X
h : (liftAux R f : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of x)) = f x
⊢ (fun (F : FreeAlgebra R X →ₐ[R] A) ↦
        (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
      (liftAux R f) x =
    f x

Tactic:
simp only [Function.comp_apply, ι_def]

Premises used: FreeAlgebra.ι_def, Function.comp_apply
-- 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
x : X
⊢ (liftAux R f : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of x)) = f x

Tactic:
rfl
-- 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 : FreeAlgebra R X →ₐ[R] A
H :
  ∀ (t : FreeAlgebra R X),
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          t :
        A)
      ((F : (a : FreeAlgebra R X) → A) t : A)
⊢ liftAux R
      ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
          (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
        F) =
    F

Tactic:
ext t
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
H :
  ∀ (x : Pre R X),
    Eq.{u_3 + 1} (α := A)
      ((liftAux R
              ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
                F) :
            (a : FreeAlgebra R X) → A)
          (Quot.mk (Rel R X) x) :
        A)
      ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) x) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        t :
      A)
    ((F : (a : FreeAlgebra R X) → A) t : A)

Tactic:
rcases t with ⟨x⟩
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a : X
H :
  Eq.{u_3 + 1} (α := A) (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) a : A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of a)) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) (Pre.of a)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of a)) : A)

Tactic:
change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _

Premises used: FreeAlgebra.ι, Function.comp, DFunLike.coe
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a : X
⊢ Eq.{u_3 + 1} (α := A) (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) a : A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of a)) : A)

Tactic:
simp only [Function.comp_apply, ι_def]

Premises used: FreeAlgebra.ι_def, Function.comp_apply
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
H :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((F : (a : FreeAlgebra R X) → A)
        ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X) :
      A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) (Pre.ofScalar x)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.ofScalar x)) : A)

Tactic:
change algebraMap _ _ x = F (algebraMap _ _ x)

Premises used: Algebra.algebraMap, DFunLike.coe
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
H H₁ : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A)
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A)
    ((F : (a : FreeAlgebra R X) → A)
        ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) x : FreeAlgebra R X) :
      A)

Tactic:
rw [AlgHom.commutes F _]

Premises used: AlgHom.commutes
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) a) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A)
hb :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) b) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
H :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R)) :
          (a : FreeAlgebra R X) → A)
        (fa + fb) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (fa + fb) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) (a.add b)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (a.add b)) : A)

Tactic:
change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)

Premises used: FreeAlgebra.ι, Function.comp, HAdd.hAdd, _private.0.FreeAlgebra.liftAux, DFunLike.coe
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) a) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A)
hb :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) b) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R)) :
          (a : FreeAlgebra R X) → A)
        (fa + fb) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (fa + fb) : A)

Tactic:
grind
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) a) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A)
hb :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) b) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
H :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R)) :
          (a : FreeAlgebra R X) → A)
        (fa * fb) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (fa * fb) : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) (a.mul b)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (a.mul b)) : A)

Tactic:
change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)

Premises used: FreeAlgebra.ι, HMul.hMul, Function.comp, _private.0.FreeAlgebra.liftAux, DFunLike.coe
-- 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 : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) a) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) a) : A)
hb :
  Eq.{u_3 + 1} (α := A)
    ((liftAux R
            ((fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A))
              F) :
          (a : FreeAlgebra R X) → A)
        (Quot.mk (Rel R X) b) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) b) : A)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ Eq.{u_3 + 1} (α := A)
    ((liftAux R (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R)) :
          (a : FreeAlgebra R X) → A)
        (fa * fb) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (fa * fb) : A)

Tactic:
grind
-- 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
rw :
  Eq (α := FreeAlgebra R X →ₐ[R] A) (liftAux R f)
    (({ toFun := liftAux R,
          invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
            Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : X → A) → FreeAlgebra R X →ₐ[R] A)
      f)
⊢ Eq (α := FreeAlgebra R X →ₐ[R] A) (liftAux R f) ((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f)

Tactic:
rw [lift]

Premises used: FreeAlgebra.lift
-- 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 (α := FreeAlgebra R X →ₐ[R] A) (liftAux R f)
    (({ toFun := liftAux R,
          invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
            Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : X → A) → FreeAlgebra R X →ₐ[R] A)
      f)

Tactic:
rfl
-- 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 : FreeAlgebra R X →ₐ[R] A
rw :
  Eq (α := X → A)
    ((Equiv.symm
            { toFun := liftAux R,
              invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
              left_inv := ⋯, right_inv := ⋯ } :
          (a : FreeAlgebra R X →ₐ[R] A) → X → A)
        F :
      X → A)
    (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A)
⊢ Eq (α := X → A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) F : X → A)
    (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A)

Tactic:
rw [lift]

Premises used: FreeAlgebra.lift
-- 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 : FreeAlgebra R X →ₐ[R] A
⊢ Eq (α := X → A)
    ((Equiv.symm
            { toFun := liftAux R,
              invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
              left_inv := ⋯, right_inv := ⋯ } :
          (a : FreeAlgebra R X →ₐ[R] A) → X → A)
        F :
      X → A)
    (Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R) : X → A)

Tactic:
rfl
-- 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
h :
  ∀ (x : X),
    Function.comp (β := FreeAlgebra R X)
        (⇑((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f : FreeAlgebra R X →ₐ[R] A) : (a : FreeAlgebra R X) → A)
        (ι R) x =
      f x
⊢ Function.comp (β := FreeAlgebra R X)
      (⇑((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f : FreeAlgebra R X →ₐ[R] A) : (a : FreeAlgebra R X) → A)
      (ι R) =
    f

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
f : X → A
x : X
h :
  ((({ toFun := liftAux R,
                invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : X → A) → FreeAlgebra R X →ₐ[R] A)
            f :
          FreeAlgebra R X →ₐ[R] A) :
        (a : FreeAlgebra R X) → A)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x
⊢ Function.comp (β := FreeAlgebra R X)
      (⇑((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f : FreeAlgebra R X →ₐ[R] A) : (a : FreeAlgebra R X) → A)
      (ι R) x =
    f x

Tactic:
rw [Function.comp_apply, ι_def, lift]

Premises used: FreeAlgebra.ι_def, Function.comp_apply, FreeAlgebra.lift
-- 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
x : X
⊢ ((({ toFun := liftAux R,
                invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : X → A) → FreeAlgebra R X →ₐ[R] A)
            f :
          FreeAlgebra R X →ₐ[R] A) :
        (a : FreeAlgebra R X) → A)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x

Tactic:
rfl
-- 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
x : X
rw :
  ((({ toFun := liftAux R,
                invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                  Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
                left_inv := ⋯, right_inv := ⋯ } :
              (a : X → A) → FreeAlgebra R X →ₐ[R] A)
            f :
          FreeAlgebra R X →ₐ[R] A) :
        (a : FreeAlgebra R X) → A)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x
⊢ (((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f : FreeAlgebra R X →ₐ[R] A) : (a : FreeAlgebra R X) → A) (ι R x) =
    f x

Tactic:
rw [ι_def, lift]

Premises used: FreeAlgebra.ι_def, FreeAlgebra.lift
-- 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
g : FreeAlgebra R X →ₐ[R] A
rw :
  Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R) = f ↔
    (Equiv.symm
            { toFun := liftAux R,
              invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
              left_inv := ⋯, right_inv := ⋯ } :
          (a : FreeAlgebra R X →ₐ[R] A) → X → A)
        g =
      f
⊢ Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R) = f ↔
    g = (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f

Tactic:
rw [← (lift R).symm_apply_eq, lift]

Premises used: Equiv.symm_apply_eq, FreeAlgebra.lift
-- 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
g : FreeAlgebra R X →ₐ[R] A
⊢ Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R) = f ↔
    (Equiv.symm
            { toFun := liftAux R,
              invFun := fun (F : FreeAlgebra R X →ₐ[R] A) ↦
                Function.comp (β := FreeAlgebra R X) (⇑F : (a : FreeAlgebra R X) → A) (ι R),
              left_inv := ⋯, right_inv := ⋯ } :
          (a : FreeAlgebra R X →ₐ[R] A) → X → A)
        g =
      f

Tactic:
rfl
-- 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
g : FreeAlgebra R X →ₐ[R] A
rw :
  (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g) = g
⊢ (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A)
      (Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R)) =
    g

Tactic:
rw [← lift_symm_apply]

Premises used: FreeAlgebra.lift_symm_apply
-- 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
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g) = g

Tactic:
(lift R).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, FreeAlgebra.lift
-- 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
g : FreeAlgebra R X →ₐ[R] A
⊢ (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g) = g

Tactic:
exact (lift R).apply_symm_apply g

Premises used: Equiv.apply_symm_apply, FreeAlgebra.lift
-- 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 g : FreeAlgebra R X →ₐ[R] A
w :
  Eq (α := X → A) (Function.comp (β := FreeAlgebra R X) (⇑f : (a : FreeAlgebra R X) → A) (ι R))
    (Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R))
⊢ Eq (α := X → A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) f : X → A)
    ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g : X → A)

Tactic:
rw [← lift_symm_apply, ← lift_symm_apply] at w

Premises used: FreeAlgebra.lift_symm_apply
-- 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 g : FreeAlgebra R X →ₐ[R] A
w :
  Eq (α := X → A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) f : X → A)
    ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g : X → A)
⊢ f = g

Tactic:
(lift R).symm.injective w

Premises used: Equiv.injective, FreeAlgebra.lift, Equiv.symm
-- 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 g : FreeAlgebra R X →ₐ[R] A
w :
  Eq (α := X → A) ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) f : X → A)
    ((Equiv.symm (lift R) : (a : FreeAlgebra R X →ₐ[R] A) → X → A) g : X → A)
⊢ f = g

Tactic:
exact (lift R).symm.injective w

Premises used: Equiv.injective, FreeAlgebra.lift, Equiv.symm
-- 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
h :
  ∀ (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)
⊢ Eq (α := MonoidAlgebra.{u_1, u_2} R (FreeMonoid X) →ₐ[R] MonoidAlgebra.{u_1, u_2} R (FreeMonoid X))
    (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))))
    (AlgHom.id R (MonoidAlgebra.{u_1, u_2} R (FreeMonoid X)))

Tactic:
ext