awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
a_1 : FreeAlgebra R X
a b a_2 b_1 c : Pre R X
h : Rel R X a_2 b_1
a_ih : liftFun R X f a_2 = liftFun R X f b_1
mul_compat_left : liftFun R X f a_2 * liftFun R X f c = liftFun R X f (b_1 * c)
⊢ liftFun R X f (a_2 * c) = liftFun R X f (b_1 * c)
have mul_compat_left₁ : liftFun R X f b_1 * liftFun R X f c = liftFun R X f (b_1 * c)
Tactic: repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ Quot.liftOn (r := Rel R X) 1 (liftFun R X f) ⋯ = 1
have change : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 1 : A) (1 : A)
Tactic: change algebraMap _ _ _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ Quot.liftOn (r := Rel R X) 0 (liftFun R X f) ⋯ = 0
have change : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) 0 : A) (0 : A)
Tactic: change algebraMap _ _ _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ (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
have h : (liftAux R f : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of x)) = f x
Tactic: simp only [Function.comp_apply, ι_def]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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
have 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)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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)
have 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)
Tactic: rcases t with ⟨x⟩
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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)
    ((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)
have 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)
Tactic: change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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)
have 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)
Tactic: change algebraMap _ _ x = F (algebraMap _ _ x)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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)
have H : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) x : A) ((algebraMap R A : (a : R) → A) x : A)
Tactic: rw [AlgHom.commutes F _]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
            ((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)
have 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)
Tactic: change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
            ((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)
have 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)
Tactic: change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 : 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)
have H : ∀ (a : 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) (Pre.of a)) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) (Pre.of a)) : A)
Tactic: induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
        -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        grind
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        grind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 : Pre R X
H :
  ∀ (a : 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) (Pre.of 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) x) :
      A)
    ((F : (a : FreeAlgebra R X) → A) (Quot.mk (Rel R X) x) : A)
have H₁ : ∀ (x : R),
  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: induction x with
      | of =>
        change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
        simp only [Function.comp_apply, ι_def]
      | ofScalar x =>
        change algebraMap _ _ x = F (algebraMap _ _ x)
        rw [AlgHom.commutes F _]
      | add a b ha hb =>
        -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
        -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
        grind
      | mul a b ha hb =>
        let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        grind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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) ((lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f)
have 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 := sorry, right_inv := sorry } :
      (a : X → A) → FreeAlgebra R X →ₐ[R] A)
    f)
Tactic: rw [lift]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 (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)
have 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 := sorry, right_inv := sorry } :
        (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]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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
have 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 := sorry, right_inv := sorry } :
            (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: rw [Function.comp_apply, ι_def, lift]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ (((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
have 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 := sorry, right_inv := sorry } :
            (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: rw [ι_def, lift]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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 ↔
    g = (lift R : (a : X → A) → FreeAlgebra R X →ₐ[R] A) f
have 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 := sorry, right_inv := sorry } :
        (a : FreeAlgebra R X →ₐ[R] A) → X → A)
      g =
    f
Tactic: rw [← (lift R).symm_apply_eq, lift]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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)
      (Function.comp (β := FreeAlgebra R X) (⇑g : (a : FreeAlgebra R X) → A) (ι R)) =
    g
have 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
Tactic: rw [← lift_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (hypothesis)
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))
⊢ f = g
have 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)
Tactic: rw [← lift_symm_apply, ← lift_symm_apply] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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)))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.FreeAlgebra (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- 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
⊢ False
have hf0 : 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 _ _
-- 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)
⊢ False
have hf1 : 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 _ _