awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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) (0 * (↑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
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
rw₃ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 * (↑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) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 : B) =
  ((↑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
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
rw₃ :
  HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 * (↑fe : (A →ₐ[R] B) × B).2) =
    ((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a
rw₄ :
  HAdd.hAdd (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B) (0 : B) =
    ((↑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₅ : Eq.{u_3 + 1} (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
  (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
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
ad : A[ε]
⊢ (((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)
      (a • ad) =
    HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
          ad :
        B)
have rw : (((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 * ad) =
  HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
        ad :
      B)
Tactic: rw [← inl_mul_eq_smul, map_mul, lift_apply_inl]
-- 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
ad : A[ε]
rw :
  (((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 * ad) =
    HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
          ad :
        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)
      (a • ad) =
    HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
          ad :
        B)
have rw₁ : HMul.hMul (α := B) (β := 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)
    ((((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)
        ad :
      B) =
  HMul.hMul (α := B) (β := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
        ad :
      B)
Tactic: rw [← inl_mul_eq_smul, map_mul, lift_apply_inl]
-- 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
ad : A[ε]
⊢ (((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)
      (MulOpposite.op a • ad) =
    HMul.hMul (α := B) (β := 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)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw : (((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)
    (ad * inl a) =
  HMul.hMul (α := B) (β := 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)
        ad :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
Tactic: rw [← mul_inl_eq_op_smul, map_mul, lift_apply_inl]
-- 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
ad : A[ε]
rw :
  (((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)
      (ad * inl a) =
    HMul.hMul (α := B) (β := 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)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : 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)
      (MulOpposite.op a • ad) =
    HMul.hMul (α := B) (β := 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)
          ad :
        B)
      (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
have rw₁ : HMul.hMul (α := B) (β := 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)
        ad :
      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) =
  HMul.hMul (α := B) (β := 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)
        ad :
      B)
    (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) a : B)
Tactic: rw [← mul_inl_eq_op_smul, map_mul, lift_apply_inl]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ⊤
have refine : ∀ (x : TrivSqZeroExt A A) (hx : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) ⊤ x),
  Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) x
Tactic: refine top_unique fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) x
have rw : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
  (inl x.fst + inl x.snd * ε)
Tactic: rw [← x.inl_fst_add_inr_snd_eq, inr_eq_smul_eps, ← inl_mul_eq_smul]
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)
have refine_1 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)
Tactic: refine add_mem ?_ (mul_mem ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
refine_1 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)
have refine_2 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.snd)
Tactic: refine add_mem ?_ (mul_mem ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : TrivSqZeroExt A A
refine_1 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.fst)
refine_2 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) (inl x.snd)
⊢ Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε])
    (inl x.fst + inl x.snd * ε)
have refine_3 : Membership.mem (γ := Subalgebra R (TrivSqZeroExt A A)) (AlgHom.range (inlAlgHom R A A) ⊔ R[ ε]) ε
Tactic: refine add_mem ?_ (mul_mem ?_ ?_)
-- 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) }
⊢ AlgHom.range.{u_1, u_4, u_3} (A := A[ε])
      ((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) =
    (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
have simp_rw : Subalgebra.map.{u_1, u_4, u_3} (A := A[ε])
    ((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)
    ⊤ =
  Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
Tactic: simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
    Algebra.map_top]
-- 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) }
simp_rw :
  Subalgebra.map.{u_1, u_4, u_3} (A := A[ε])
      ((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)
      ⊤ =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
⊢ AlgHom.range.{u_1, u_4, u_3} (A := A[ε])
      ((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) =
    (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
have simp_rw₁ : Subalgebra.map
    ((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.range (inlAlgHom R A A) ⊔ R[ ε]) =
  Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
Tactic: simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
    Algebra.map_top]
-- 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) }
simp_rw :
  Subalgebra.map.{u_1, u_4, u_3} (A := A[ε])
      ((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)
      ⊤ =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₁ :
  Subalgebra.map
      ((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.range (inlAlgHom R A A) ⊔ R[ ε]) =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
⊢ AlgHom.range.{u_1, u_4, u_3} (A := A[ε])
      ((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) =
    (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
have simp_rw₂ : Subalgebra.map
      ((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.range (inlAlgHom R A A)) ⊔
    Subalgebra.map (A := A[ε])
      ((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)
      R[ ε] =
  Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
Tactic: simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
    Algebra.map_top]
-- 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) }
simp_rw :
  Subalgebra.map.{u_1, u_4, u_3} (A := A[ε])
      ((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)
      ⊤ =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₁ :
  Subalgebra.map
      ((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.range (inlAlgHom R A A) ⊔ R[ ε]) =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
simp_rw₂ :
  Subalgebra.map
        ((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.range (inlAlgHom R A A)) ⊔
      Subalgebra.map (A := A[ε])
        ((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)
        R[ ε] =
    Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
⊢ AlgHom.range.{u_1, u_4, u_3} (A := A[ε])
      ((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) =
    (↑fe : (A →ₐ[R] B) × B).1.range ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
have simp_rw₃ : Subalgebra.map
      ((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.range (inlAlgHom R A A)) ⊔
    adjoin R
      (Set.image (α := A[ε])
        (⇑((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)
        {ε}) =
  Subalgebra.map (↑fe : (A →ₐ[R] B) × B).1 ⊤ ⊔ R[(↑fe : (A →ₐ[R] B) × B).2]
Tactic: simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup,
    AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
    Algebra.map_top]