awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : DecompositionMonoid G₁
inst_4 : DecompositionMonoid G₂
a b c : G₁ × G₂
h : a.1 ∣ (b * c).1 ∧ a.2 ∣ (b * c).2
a₁ a₁' : G₁
h₁ : a₁ ∣ b.1
h₁' : a₁' ∣ c.1
eq₁ : a.1 = a₁ * a₁'
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂
have obtain : ∀ (a₂ a₂' : G₂) (h₂ : a₂ ∣ b.2) (h₂' : a₂' ∣ c.2) (eq₂ : a.2 = a₂ * a₂'),
  ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂
Tactic: obtain ⟨a₂, a₂', h₂, h₂', eq₂⟩ := DecompositionMonoid.primal a.2 h.2
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i
have simp_rw : (∃ (c : (i : ι) → G i), ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ (f : (x : ι) → G x), ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
Tactic: simp_rw [dvd_def, funext_iff, Classical.skolem]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : a ∣ b * c
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
have simp_rw : ∀ (h : ∀ (i : ι), a i ∣ (b * c) i),
  ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
Tactic: simp_rw [pi_dvd_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Prod (goal)
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
have choose : ∀ (a₁ a₂ : (i : ι) → G i) (h₁ : ∀ (i : ι), a₁ i ∣ b i) (h₂ : ∀ (i : ι), a₂ i ∣ c i) (eq : ∀ (i : ι), a i = a₁ i * a₂ i),
  ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
Tactic: choose a₁ a₂ h₁ h₂ eq using fun i ↦ DecompositionMonoid.primal _ (h i)
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b * (↑u : α)
c : α
eq : b * (↑u : α) = a * c
⊢ b = a * (c * (↑u⁻¹ : α))
have rw : b = a * c * (↑u⁻¹ : α)
Tactic: rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b * (↑u : α)
c : α
eq : b * (↑u : α) = a * c
rw : b = a * c * (↑u⁻¹ : α)
⊢ b = a * (c * (↑u⁻¹ : α))
have rw₁ : b = b * (↑u : α) * (↑u⁻¹ : α)
Tactic: rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b * (↑u : α)
c : α
eq : b * (↑u : α) = a * c
rw : b = a * c * (↑u⁻¹ : α)
rw₁ : b = b * (↑u : α) * (↑u⁻¹ : α)
⊢ b = a * (c * (↑u⁻¹ : α))
have rw₂ : b = b
Tactic: rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b
⊢ a * (↑u : α) * (↑u⁻¹ : α) = a
have rw : a * ((↑u : α) * (↑u⁻¹ : α)) = a
Tactic: rw [mul_assoc, u.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b
rw : a * ((↑u : α) * (↑u⁻¹ : α)) = a
⊢ a * (↑u : α) * (↑u⁻¹ : α) = a
have rw₁ : a * 1 = a
Tactic: rw [mul_assoc, u.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b
rw : a * ((↑u : α) * (↑u⁻¹ : α)) = a
rw₁ : a * 1 = a
⊢ a * (↑u : α) * (↑u⁻¹ : α) = a
have rw₂ : a = a
Tactic: rw [mul_assoc, u.mul_inv, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ (↑u : α) * b ↔ a ∣ b
have rw : a ∣ b * (↑u : α) ↔ a ∣ b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ (↑u : α) * a ∣ b ↔ a ∣ b
have rw : a * (↑u : α) ∣ b ↔ a ∣ b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a u : α
hu : IsUnit u
⊢ u ∣ a
have rcases : ∀ (u : αˣ), (↑u : α) ∣ a
Tactic: rcases hu with ⟨u, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b
have rcases : ∀ (u : αˣ), a ∣ b * (↑u : α) ↔ a ∣ b
Tactic: rcases hu with ⟨u, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b
have rcases : ∀ (u : αˣ), a * (↑u : α) ∣ b ↔ a ∣ b
Tactic: rcases hu with ⟨u, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b
have rcases : ∀ (u : αˣ), a ∣ (↑u : α) * b ↔ a ∣ b
Tactic: rcases hu with ⟨u, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b
have rcases : ∀ (u : αˣ), (↑u : α) * a ∣ b ↔ a ∣ b
Tactic: rcases hu with ⟨u, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x : α
h_1 : x ∣ 1
y : α
h : 1 = x * y
⊢ y * x = 1
have rw : y * x = x * y
Tactic: rw [h, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x : α
h_1 : x ∣ 1
y : α
h : 1 = x * y
rw : y * x = x * y
⊢ y * x = 1
have rw₁ : x * y = x * y
Tactic: rw [h, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x : α
n : ℕ
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
have inl : x ∣ HPow.hPow (β := ℕ) x 0 ↔ Ne (α := ℕ) 0 0 ∨ IsUnit x
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x : α
n : ℕ
inl : x ∣ HPow.hPow (β := ℕ) x 0 ↔ Ne (α := ℕ) 0 0 ∨ IsUnit x
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
have inr : ∀ (hn : n ≠ 0), x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
⊢ IsRelPrime x y
have rw : ∀ (H : IsRelPrime (y * z) x), IsRelPrime y x
Tactic: rw [isRelPrime_comm] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
h : IsRelPrime y z
dvd : x ∣ y
⊢ IsRelPrime x z
have obtain : ∀ (d : α) (h : IsRelPrime (x * d) z), IsRelPrime x z
Tactic: obtain ⟨d, rfl⟩ := dvd
Cleared hypotheses: y, h, dvd
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z
have rw : IsRelPrime (x * z) y ↔ IsRelPrime y z
Tactic: rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime (x * z) y ↔ IsRelPrime y z
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z
have rw₁ : IsRelPrime z y ↔ IsRelPrime y z
Tactic: rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime (x * z) y ↔ IsRelPrime y z
rw₁ : IsRelPrime z y ↔ IsRelPrime y z
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z
have rw₂ : IsRelPrime y z ↔ IsRelPrime y z
Tactic: rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z
have rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
Tactic: rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z
have rw₁ : IsRelPrime y z ↔ IsRelPrime y z
Tactic: rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) z ↔ IsRelPrime y z
have rw : IsRelPrime (x * y) z ↔ IsRelPrime y z
Tactic: rw [mul_comm, isRelPrime_mul_unit_left_left hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime (x * y) z ↔ IsRelPrime y z
⊢ IsRelPrime (y * x) z ↔ IsRelPrime y z
have rw₁ : IsRelPrime y z ↔ IsRelPrime y z
Tactic: rw [mul_comm, isRelPrime_mul_unit_left_left hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z
have rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
Tactic: rw [mul_comm, isRelPrime_mul_unit_left_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z
have rw₁ : IsRelPrime y z ↔ IsRelPrime y z
Tactic: rw [mul_comm, isRelPrime_mul_unit_left_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z
have rw : IsRelPrime y (z * x) ↔ IsRelPrime y z
Tactic: rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (z * x) ↔ IsRelPrime y z
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z
have rw₁ : IsRelPrime y z ↔ IsRelPrime y z
Tactic: rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ y
have obtain : ∀ (a b : α) (ha : a ∣ y) (hb : b ∣ z) (H1 : IsRelPrime (a * b) z) (H2 : a * b ∣ y * z) (h : IsPrimal (a * b)), a * b ∣ y
Tactic: obtain ⟨a, b, ha, hb, rfl⟩ := h H2
Cleared hypotheses: x, H1, H2, h
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hy : IsPrimal y
⊢ x * y ∣ z
have obtain : ∀ (w : α) (H2 : y ∣ x * w), x * y ∣ x * w
Tactic: obtain ⟨w, rfl⟩ := H1
Cleared hypotheses: z, H1, H2
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ x * y ∣ z
have rw : y * x ∣ z
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x_1 : α
h : x_1 ∣ x * y
hz : x_1 ∣ z
⊢ IsUnit x_1
have obtain : ∀ (a b : α) (ha : a ∣ x) (hb : b ∣ y) (h : a * b ∣ x * y) (hz : a * b ∣ z), IsUnit (a * b)
Tactic: obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
Cleared hypotheses: x_1, h, hz
-- Lean 4 proof step from Mathlib.Algebra.Divisibility.Units (goal)
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
⊢ IsRelPrime x (y * z)
have rw : ∀ (H1 : IsRelPrime y x) (H2 : IsRelPrime z x), IsRelPrime (y * z) x
Tactic: rw [isRelPrime_comm] at H1 H2 ⊢
Cleared hypotheses: H1, H2
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
⊢ Commute ε x
have h1 : fst (ε * x) = fst (x * ε)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.DualNumber (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R[ε]
h1 : fst (ε * x) = fst (x * ε)
⊢ Commute ε x
have h2 : snd (ε * x) = snd (x * ε)
Tactic: ext
-- 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
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.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)
have h : Eq.{u_3 + 1} (α := B) ((f : (a : A[ε]) → B) (inr a) : B) ((g : (a : A[ε]) → B) (inr a) : B)
Tactic: change f (inr a) = g (inr a)
-- 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
f g : R[ε] →ₐ[R] A
hε : Eq.{u_4 + 1} (α := A) ((f : (a : R[ε]) → A) ε : A) ((g : (a : R[ε]) → A) ε : A)
⊢ f = g
have 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)
Tactic: ext
-- 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
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.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)
have 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)
Tactic: dsimp
-- 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 : (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
have 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) }
Tactic: refine Equiv.trans ?_ TrivSqZeroExt.liftEquiv
-- 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) }
x y : A
⊢ 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
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) y : B) *
    ((↑fe : (A →ₐ[R] B) × B).2 * (↑fe : (A →ₐ[R] B) × B).2) =
  0
Tactic: rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero]
-- 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) }
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
⊢ 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
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) y : B) *
    0 =
  0
Tactic: rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero]
-- 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) }
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
⊢ 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
have rw₂ : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero]
-- 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) (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) (β := 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)
Tactic: rw [map_mul, mul_assoc]