awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
a : α
m : Multiset α
rw :
  FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) ({a} + m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₁ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
rw₂ :
  FreeAbelianGroup.of
      (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
        ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
    HMul.hMul (α := FreeAbelianGroup (Multiplicative (Multiset α))) (β :=
      FreeAbelianGroup (Multiplicative (Multiset α)))
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a}) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
⊢ FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) (a ::ₘ m)) =
    HMul.hMul (β := FreeAbelianGroup (Multiplicative (Multiset α))) (of a)
      (FreeAbelianGroup.of ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m) :
        FreeAbelianGroup (Multiplicative (Multiset α)))
have rw₃ : FreeAbelianGroup.of
    (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α))) =
  FreeAbelianGroup.of
    (HMul.hMul (α := Multiplicative (Multiset α)) (β := Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) {a} : Multiplicative (Multiset α))
      ((Multiplicative.ofAdd : (a : Multiset α) → Multiplicative (Multiset α)) m : Multiplicative (Multiset α)))
Tactic: rw [← Multiset.singleton_add, ofAdd_add,
    of, FreeAbelianGroup.of_mul_of]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f_1 f : α → R
x y : Multiplicative (Multiset α)
⊢ (Multiset.map f ((Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) (x * y))).prod =
    (Multiset.map f x + Multiset.map f y).prod
have rw : (Multiset.map f ((Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) (x * y))).prod =
  (Multiset.map f (x + y)).prod
Tactic: rw [← Multiset.map_add]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : α → R
F : MonoidHom.{u, v} (Multiplicative (Multiset α)) R
x : Multiplicative (Multiset α)
F' : AddMonoidHom.{u, v} (Multiset α) (Additive R) :=
  (MonoidHom.toAdditiveRight : (a : Multiplicative (Multiset α) →* R) → Multiset α →+ Additive R) F
x' : Multiset α := (Multiplicative.toAdd : (a : Multiplicative (Multiset α)) → Multiset α) x
⊢ Eq.{v + 1} (α := Additive R)
    (Multiset.sum (Multiset.map (fun (a : α) ↦ (F' : (a : Multiset α) → Additive R) {a}) x') : Additive R)
    ((F' : (a : Multiset α) → Additive R) x' : Additive R)
have rw : Eq.{v + 1} (α := Additive R)
  ((F' : (a : Multiset α) → Additive R) (Multiset.sum (Multiset.map (fun (x : α) ↦ {x}) x')) : Additive R)
  ((F' : (a : Multiset α) → Additive R) x' : Additive R)
Tactic: rw [← Function.comp_def (fun x => F' x) (fun x => {x}), ← Multiset.map_map,
        ← AddMonoidHom.map_multiset_sum]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x : FreeCommRing α
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (-1) :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
have rw : Eq.{v + 1} (α := R)
  (-(((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        1 :
    R)
  ((f : (a : FreeCommRing α) → R) (-1) : R)
Tactic: rw [map_neg, map_one, f.map_neg, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x : FreeCommRing α
rw :
  Eq.{v + 1} (α := R)
    (-(((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          1 :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (-1) :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
have rw₁ : Eq.{v + 1} (α := R) (-1 : R) ((f : (a : FreeCommRing α) → R) (-1) : R)
Tactic: rw [map_neg, map_one, f.map_neg, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x : FreeCommRing α
rw :
  Eq.{v + 1} (α := R)
    (-(((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          1 :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
rw₁ : Eq.{v + 1} (α := R) (-1 : R) ((f : (a : FreeCommRing α) → R) (-1) : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (-1) :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
have rw₂ : Eq.{v + 1} (α := R) (-1 : R) (-(f : (a : FreeCommRing α) → R) 1 : R)
Tactic: rw [map_neg, map_one, f.map_neg, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x : FreeCommRing α
rw :
  Eq.{v + 1} (α := R)
    (-(((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          1 :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
rw₁ : Eq.{v + 1} (α := R) (-1 : R) ((f : (a : FreeCommRing α) → R) (-1) : R)
rw₂ : Eq.{v + 1} (α := R) (-1 : R) (-(f : (a : FreeCommRing α) → R) 1 : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (-1) :
      R)
    ((f : (a : FreeCommRing α) → R) (-1) : R)
have rw₃ : Eq.{v + 1} (α := R) (-1) (-1)
Tactic: rw [map_neg, map_one, f.map_neg, f.map_one]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x + y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x + y) : R)
have rw : HAdd.hAdd (α := R) (β := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  (f : (a : FreeCommRing α) → R) (x + y)
Tactic: rw [map_add, f.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x + y)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x + y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x + y) : R)
have rw₁ : HAdd.hAdd (α := R) (β := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_add, f.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x + y)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x + y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x + y) : R)
have rw₂ : HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_add, f.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x + y)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x + y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x + y) : R)
have rw₃ : HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R) =
  HAdd.hAdd (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_add, f.map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x * y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x * y) : R)
have rw : HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  (f : (a : FreeCommRing α) → R) (x * y)
Tactic: rw [map_mul, f.map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x * y)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x * y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x * y) : R)
have rw₁ : HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_mul, f.map_mul, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
R : Type v
inst : CommRing R
f : RingHom.{u, v} (FreeCommRing α) R
x_1 x y : FreeCommRing α
ihx :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        x :
      R)
    ((f : (a : FreeCommRing α) → R) x : R)
ihy :
  Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R)
    ((f : (a : FreeCommRing α) → R) y : R)
rw :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    (f : (a : FreeCommRing α) → R) (x * y)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
              RingHom.{u, v} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          y :
        R) =
    HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
⊢ Eq.{v + 1} (α := R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        (x * y) :
      R)
    ((f : (a : FreeCommRing α) → R) (x * y) : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R)
    ((((lift : (a : α → R) → FreeCommRing α →+* R) ((⇑f : (a : FreeCommRing α) → R) ∘ of) :
            RingHom.{u, v} (FreeCommRing α) R) :
          (a : FreeCommRing α) → R)
        y :
      R) =
  HMul.hMul (α := R) (β := R) ((f : (a : FreeCommRing α) → R) x : R) ((f : (a : FreeCommRing α) → R) y : R)
Tactic: rw [map_mul, f.map_mul, ihx, ihy]