awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : DivisionRing R
⊢ Eq.{u_1 + 1} (α := R[ε]) ε⁻¹ 0

Tactic:
TrivSqZeroExt.inv_inr 1

Premises used: OfNat.ofNat, TrivSqZeroExt.inv_inr
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : MulZeroOneClass R
r : R
⊢ inr r = HSMul.hSMul (β := R[ε]) r ε

Tactic:
ext (mul_zero r).symm (mul_one r).symm

Premises used: TrivSqZeroExt.ext, MulZeroClass.mul_zero, mul_one, Eq.symm
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
h1 : fst (ε * x) = fst (x * ε)
h2 : snd (ε * x) = snd (x * ε)
⊢ Commute ε x

Tactic:
ext
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
⊢ fst (ε * x) = fst (x * ε)

Tactic:
simp
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
⊢ snd (ε * x) = snd (x * ε)

Tactic:
simp
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
⊢ Commute x ε

Tactic:
(commute_eps_left x).symm

Premises used: Commute.symm, DualNumber.commute_eps_left
-- Module: Mathlib.Algebra.DualNumber
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
f g : AlgHom.{u_1, u_4, u_3} R A[ε] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  Eq (α := A →ₗ[R] B)
    (f.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
    (g.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
a : A
h : Eq.{u_3 + 1} (α := B) ((f : (a : A[ε]) → B) (inr a) : B) ((g : (a : A[ε]) → B) (inr a) : B)
⊢ Eq.{u_3 + 1} (α := B)
    ((f.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (inrHom A A) :
          (a : A) → B)
        a :
      B)
    ((g.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_4} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (inrHom A A) :
          (a : A) → B)
        a :
      B)

Tactic:
change f (inr a) = g (inr a)

Premises used: TrivSqZeroExt.inr, DFunLike.coe
-- Module: Mathlib.Algebra.DualNumber
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
f g : AlgHom.{u_1, u_4, u_3} R A[ε] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  Eq (α := A →ₗ[R] B)
    (f.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
    (g.toLinearMap ∘ₗ
      (↑R :
          {S M M₂ : Type u_4} →
            [inst : Semiring R] →
              [inst_5 : Semiring S] →
                [inst_6 : AddCommMonoid M] →
                  [inst_7 : AddCommMonoid M₂] →
                    [inst_8 : Module R M] →
                      [inst_9 : Module R M₂] →
                        [inst_10 : Module S M] →
                          [inst_11 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (LinearMap.toSpanSingleton A A[ε] ε))
a : A
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A[ε]) → B) (inr a) : B) ((g : (a : A[ε]) → B) (inr a) : B)

Tactic:
simpa only [inr_eq_smul_eps] using DFunLike.congr_fun hinr a

Premises used: DFunLike.congr_fun, DualNumber.inr_eq_smul_eps
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f g : R[ε] →ₐ[R] A
hε : Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) ε : A) ((g : (a : R[ε]) → A) ε : A)
hinr :
  Eq.{u_4 + 1} (α := A)
    ((f.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LinearMap.toSpanSingleton R R[ε] ε) :
          (a : R) → A)
        1 :
      A)
    ((g.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LinearMap.toSpanSingleton R R[ε] ε) :
          (a : R) → A)
        1 :
      A)
⊢ f = g

Tactic:
ext
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f g : R[ε] →ₐ[R] A
hε : Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) ε : A) ((g : (a : R[ε]) → A) ε : A)
hinr :
  Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) (HSMul.hSMul (α := R) (β := R[ε]) 1 ε) : A)
    ((g : (a : R[ε]) → A) (HSMul.hSMul (α := R) (β := R[ε]) 1 ε) : A)
⊢ Eq.{u_4 + 1} (α := A)
    ((f.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LinearMap.toSpanSingleton R R[ε] ε) :
          (a : R) → A)
        1 :
      A)
    ((g.toLinearMap ∘ₗ
            (↑R :
                {S M M₂ : Type u_1} →
                  [inst : Semiring R] →
                    [inst_3 : Semiring S] →
                      [inst_4 : AddCommMonoid M] →
                        [inst_5 : AddCommMonoid M₂] →
                          [inst_6 : Module R M] →
                            [inst_7 : Module R M₂] →
                              [inst_8 : Module S M] →
                                [inst_9 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (LinearMap.toSpanSingleton R R[ε] ε) :
          (a : R) → A)
        1 :
      A)

Tactic:
dsimp
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
f g : R[ε] →ₐ[R] A
hε : Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) ε : A) ((g : (a : R[ε]) → A) ε : A)
⊢ Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) (HSMul.hSMul (α := R) (β := R[ε]) 1 ε) : A)
    ((g : (a : R[ε]) → A) (HSMul.hSMul (α := R) (β := R[ε]) 1 ε) : A)

Tactic:
simp only [one_smul, hε]

Premises used: one_smul
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_5
inst_1 : CommSemiring R'
f g : RingHom.{u_1, u_5} R[ε] R'
h₀ : Eq (α := R →+* R') (f.comp (algebraMap R R[ε])) (g.comp (algebraMap R R[ε]))
hε : Eq.{u_5 + 1} (α := R') ((f : (a : R[ε]) → R') ε : R') ((g : (a : R[ε]) → R') ε : R')
this : Algebra.{u_1, u_5} R[ε] R' := f.toAlgebra
⊢ Algebra R R'

Tactic:
exact Algebra.compHom _ (algebraMap R R[ε])

Premises used: Algebra.algebraMap, DualNumber, Algebra.compHom
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_5
inst_1 : CommSemiring R'
f g : RingHom.{u_1, u_5} R[ε] R'
h₀ : Eq (α := R →+* R') (f.comp (algebraMap R R[ε])) (g.comp (algebraMap R R[ε]))
hε : Eq.{u_5 + 1} (α := R') ((f : (a : R[ε]) → R') ε : R') ((g : (a : R[ε]) → R') ε : R')
this : Algebra R R' := compHom (R := R[ε]) R' (algebraMap R R[ε])
f' : R[ε] →ₐ[R] R' := { toRingHom := f, commutes' := ⋯ }
g' : R[ε] →ₐ[R] R' := { toRingHom := g, commutes' := ⋯ }
⊢ f = g

Tactic:
congr_arg AlgHom.toRingHom (show f' = g' from algHom_ext hε)

Premises used: DualNumber.algHom_ext, congr_arg, AlgHom.toRingHom
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_5
inst_1 : CommSemiring R'
f g : RingHom.{u_1, u_5} R[ε] R'
h₀ : Eq (α := R →+* R') (f.comp (algebraMap R R[ε])) (g.comp (algebraMap R R[ε]))
hε : Eq.{u_5 + 1} (α := R') ((f : (a : R[ε]) → R') ε : R') ((g : (a : R[ε]) → R') ε : R')
this : Algebra R R' := compHom (R := R[ε]) R' (algebraMap R R[ε])
f' : R[ε] →ₐ[R] R' := { toRingHom := f, commutes' := ⋯ }
g' : R[ε] →ₐ[R] R' := { toRingHom := g, commutes' := ⋯ }
⊢ f = g

Tactic:
exact congr_arg AlgHom.toRingHom (show f' = g' from algHom_ext hε)

Premises used: DualNumber.algHom_ext, congr_arg, AlgHom.toRingHom
-- Module: Mathlib.Algebra.DualNumber
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
refine :
  { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) } ≃
    { 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) }
⊢ { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) } ≃
    AlgHom.{u_1, u_4, u_3} R A[ε] B

Tactic:
refine Equiv.trans ?_ TrivSqZeroExt.liftEquiv

Premises used: Equiv.trans, TrivSqZeroExt.liftEquiv
-- Module: Mathlib.Algebra.DualNumber
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) }
x y : 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) y : B) *
      ((↑fe : (A →ₐ[R] B) × B).2 * (↑fe : (A →ₐ[R] B) × B).2) =
    0
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) y : B) *
      0 =
    0
rw₂ rw₃ : Eq.{u_3 + 1} (α := B) 0 0
⊢ 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) y : B) (↑fe : (A →ₐ[R] B) × B).2 =
    0

Tactic:
rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero]

Premises used: Commute.mul_mul_mul_comm, MulZeroClass.mul_zero, And.right, And.left, Subtype.prop
-- Module: Mathlib.Algebra.DualNumber
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [map_mul, mul_assoc]

Premises used: mul_assoc, map_mul
-- Module: Mathlib.Algebra.DualNumber
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)
rw₁ 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
⊢ 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)

Tactic:
rw [map_mul, (fe.prop.2 _).right_comm]

Premises used: map_mul, And.right, Commute.right_comm, Subtype.prop
-- Module: Mathlib.Algebra.DualNumber
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)
rw₅ 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)
⊢ 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)

Tactic:
rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]

Premises used: op_smul_eq_mul, And.right, And.left, Subtype.prop, smul_eq_mul, mul_one, one_mul
-- Module: Mathlib.Algebra.DualNumber
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
rw₁ rw₂ : (↑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

Tactic:
rw [map_one, one_mul]

Premises used: map_one, one_mul
-- Module: Mathlib.Algebra.DualNumber
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)
rw₂ 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)
⊢ 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

Tactic:
rw [← fg.prop.2.1, smul_eq_mul, mul_one]

Premises used: And.right, And.left, Subtype.prop, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.DualNumber
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 : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) } ≃
    { 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) }

Tactic:
exact {
    toFun := fun fe => ⟨
      (fe.val.1, MulOpposite.op fe.val.2 • fe.val.1.toLinearMap),
      fun x y => show (fe.val.1 x * fe.val.2) * (fe.val.1 y * fe.val.2) = 0 by
        rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero],
      fun r x => show fe.val.1 (r * x) * fe.val.2 = fe.val.1 r * (fe.val.1 x * fe.val.2) by
        rw [map_mul, mul_assoc],
      fun r x => show fe.val.1 (x * r) * fe.val.2 = (fe.val.1 x * fe.val.2) * fe.val.1 r by
        rw [map_mul, (fe.prop.2 _).right_comm]⟩
    invFun := fun fg => ⟨
      (fg.val.1, fg.val.2 1),
      fg.prop.1 _ _,
      fun a => show fg.val.2 1 * fg.val.1 a = fg.val.1 a * fg.val.2 1 by
        rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]⟩
    left_inv := fun fe => Subtype.ext <| Prod.ext rfl <|
      show fe.val.1 1 * fe.val.2 = fe.val.2 by
        rw [map_one, one_mul]
    right_inv := fun fg => Subtype.ext <| Prod.ext rfl <| LinearMap.ext fun x =>
      show fg.val.1 x * fg.val.2 1 = fg.val.2 x by
        rw [← fg.prop.2.1, smul_eq_mul, mul_one] }
-- Module: Mathlib.Algebra.DualNumber
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[ε]
⊢ (((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 =
    HAdd.hAdd (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (fst a) : B)
      (HMul.hMul (α := B) (((↑fe : (A →ₐ[R] B) × B).1 : (a : A) → B) (snd a) : B) (↑fe : (A →ₐ[R] B) × B).2)

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.fst, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.DualNumber
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
F : AlgHom.{u_1, u_4, u_3} R A[ε] B
⊢ Eq (α := (A →ₐ[R] B) × B)
    ((↑((Equiv.symm lift :
              (a : A[ε] →ₐ[R] B) →
                { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 ((fe.1 : (a : A) → B) a) })
            F) :
        (A →ₐ[R] B) × B) :
      (A →ₐ[R] B) × B)
    ((F.comp (inlAlgHom R A A), (F : (a : A[ε]) → B) ε) : (A →ₐ[R] B) × B)

Tactic:
rfl

Premises used: TrivSqZeroExt.inr, AlgHom.comp, DualNumber.eps, rfl