awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
r x : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
        (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) *
      (↑fe : (A →ₐ[R] B) × B).2 =
    HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
⊢ HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (r * x) : B) (↑fe : (A →ₐ[R] B) × B).2 =
    HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
have rw₁ : HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
    (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2) =
  HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
    (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
Tactic: rw [map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
r x : A
⊢ HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (x * r) : B) (↑fe : (A →ₐ[R] B) × B).2 =
    HMul.hMul (β := B) (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
have rw : HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B) *
    (↑fe : (A →ₐ[R] B) × B).2 =
  HMul.hMul (β := B) (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
Tactic: rw [map_mul, (fe.prop.2 _).right_comm]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
r x : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B)
        (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B) *
      (↑fe : (A →ₐ[R] B) × B).2 =
    HMul.hMul (β := B) (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
⊢ HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (x * r) : B) (↑fe : (A →ₐ[R] B) × B).2 =
    HMul.hMul (β := B) (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B) (↑fe : (A →ₐ[R] B) × B).2)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B)
have rw₁ : HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B) *
    (↑fe : (A →ₐ[R] B) × B).2 =
  HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) x : B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) r : B) *
    (↑fe : (A →ₐ[R] B) × B).2
Tactic: rw [map_mul, (fe.prop.2 _).right_comm]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw : HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
  ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw₁ : Eq.{u_3 + 1} (α := B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1) : B)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
rw₁ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1) : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw₂ : Eq.{u_3 + 1} (α := B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
rw₁ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1) : B)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw₃ : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (1 * a) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
rw₁ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1) : B)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (1 * a) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw₄ : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (1 * a) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) a : B)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
a : A
rw :
  HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1)
rw₁ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) a 1) : B)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) (MulOpposite.op a) 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (1 * a) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (a * 1) : B)
rw₄ :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (1 * a) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) a : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B) =
    HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) a : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B)
have rw₅ : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) a : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) a : B)
Tactic: rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
⊢ HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) 1 : B) (↑fe : (A →ₐ[R] B) × B).2 =
    (↑fe : (A →ₐ[R] B) × B).2
have rw : 1 * (↑fe : (A →ₐ[R] B) × B).2 = (↑fe : (A →ₐ[R] B) × B).2
Tactic: rw [map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }
rw : 1 * (↑fe : (A →ₐ[R] B) × B).2 = (↑fe : (A →ₐ[R] B) × B).2
⊢ HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) 1 : B) (↑fe : (A →ₐ[R] B) × B).2 =
    (↑fe : (A →ₐ[R] B) × B).2
have rw₁ : (↑fe : (A →ₐ[R] B) × B).2 = (↑fe : (A →ₐ[R] B) × B).2
Tactic: rw [map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
x : A
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) x : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x
have rw : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) x 1) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
Tactic: rw [← fg.prop.2.1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
x : A
rw :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) x 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) x : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x
have rw₁ : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (x * 1) : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
Tactic: rw [← fg.prop.2.1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A_1 : Type u_2
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fg :
  { fg : (A →ₐ[R] B) × (A →ₗ[R] B) //
    (∀ (x y : A), HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.2 : (a : A) → B) y : B) = 0) ∧
      (∀ (r x : A),
          (fg.2 : (a : A) → B) (r • x) =
            HMul.hMul (α := B) (β := B) ((fg.1 : (a : A) → B) r : B) ((fg.2 : (a : A) → B) x : B)) ∧
        ∀ (r x : A),
          (fg.2 : (a : A) → B) (MulOpposite.op r • x) =
            HMul.hMul (α := B) (β := B) ((fg.2 : (a : A) → B) x : B) ((fg.1 : (a : A) → B) r : B) }
x : A
rw :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (HSMul.hSMul (β := A) x 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
rw₁ :
  Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) (x * 1) : B)
    (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
⊢ HMul.hMul (α := B) (β := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).1 : (a : A) → B) x : B)
      (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) 1 : B) =
    ((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x
have rw₂ : Eq.{u_3 + 1} (α := B) (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
  (((↑fg : (A →ₐ[R] B) × (A →ₗ[R] B)).2 : (a : A) → B) x : B)
Tactic: rw [← fg.prop.2.1, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
a : A
⊢ Eq.{u_3 + 1} (α := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        (inl a) :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw : HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (fst (M := A) (inl a)) : B)
    (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
  ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
Tactic: rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
a : A
rw :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (fst (M := A) (inl a)) : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
⊢ Eq.{u_3 + 1} (α := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        (inl a) :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw₁ : HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
    (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
  ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
Tactic: rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
B : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
fe : { _fe : (A →ₐ[R] B) × B // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 ((_fe.1 : (a : A) → B) a) }
a : A
rw :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (fst (M := A) (inl a)) : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₁ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd (inl a)) : B) (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
⊢ Eq.{u_3 + 1} (α := B)
    ((((lift :
                (a : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) }) →
                  A[ε] →ₐ[R] B)
              fe :
            AlgHom.{u_1, u_4, u_3} R A[ε] B) :
          (a : A[ε]) → B)
        (inl a) :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw₂ : HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
    (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) 0 : B) (↑fe : (A →ₐ[R] B) × B).2) =
  ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
Tactic: rw [lift_apply_apply, fst_inl, snd_inl, map_zero, zero_mul, add_zero]