awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ ({ re := TrivSqZeroExt.fst (x * y).re, imI := TrivSqZeroExt.fst (x * y).imI, imJ := TrivSqZeroExt.fst (x * y).imJ,
        imK := TrivSqZeroExt.fst (x * y).imK },
      { re := TrivSqZeroExt.snd (x * y).re, imI := TrivSqZeroExt.snd (x * y).imI, imJ := TrivSqZeroExt.snd (x * y).imJ,
        imK := TrivSqZeroExt.snd (x * y).imK }) =
    HMul.hMul (α := DualNumber ℍ[R])
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
      ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] })
have h1 : TrivSqZeroExt.fst (M := ℍ[R])
    ({ re := TrivSqZeroExt.fst (x * y).re, imI := TrivSqZeroExt.fst (x * y).imI, imJ := TrivSqZeroExt.fst (x * y).imJ,
        imK := TrivSqZeroExt.fst (x * y).imK },
      { re := TrivSqZeroExt.snd (x * y).re, imI := TrivSqZeroExt.snd (x * y).imI, imJ := TrivSqZeroExt.snd (x * y).imJ,
        imK := TrivSqZeroExt.snd (x * y).imK }) =
  TrivSqZeroExt.fst
    (HMul.hMul (α := DualNumber ℍ[R])
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] })
      ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] },
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ { re := TrivSqZeroExt.snd (x * y).re, imI := TrivSqZeroExt.snd (x * y).imI, imJ := TrivSqZeroExt.snd (x * y).imJ,
      imK := TrivSqZeroExt.snd (x * y).imK } =
    HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] } +
      HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }
have h2 : TrivSqZeroExt.snd (x * y).re =
  (HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).re +
    (HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).re
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
h2 :
  TrivSqZeroExt.snd (x * y).re =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).re +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).re
⊢ { re := TrivSqZeroExt.snd (x * y).re, imI := TrivSqZeroExt.snd (x * y).imI, imJ := TrivSqZeroExt.snd (x * y).imJ,
      imK := TrivSqZeroExt.snd (x * y).imK } =
    HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] } +
      HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }
have h2₁ : TrivSqZeroExt.snd (x * y).imI =
  (HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
          imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
          imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imI +
    (HMul.hMul (α := ℍ[R])
        { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
          imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
        { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
          imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imI
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x * y).re =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).re +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).re
have h2 : TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re -
        (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI) -
      (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ) -
    (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK) =
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.re - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imI -
        TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imJ -
      TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imK +
    (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.re - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imI -
        TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imJ -
      TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imK)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x * y).imI =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imI +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imI
have h2 : TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI +
        (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re) +
      (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK) -
    (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ) =
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.re +
        TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imK -
      TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imJ +
    (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imI + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.re +
        TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imK -
      TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imJ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x * y).imJ =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imJ +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imJ
have h2 : TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ -
        (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK) +
      (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re) +
    (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI) =
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imJ - TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imK +
        TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.re +
      TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.imI +
    (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imJ - TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imK +
        TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.re +
      TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.imI)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.DualQuaternion (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd (x * y).imK =
    (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK : ℍ[R,-1,-1] }).imK +
      (HMul.hMul (α := ℍ[R])
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK : ℍ[R,-1,-1] }
          { re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK : ℍ[R,-1,-1] }).imK
have h2 : TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK +
        (TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ) -
      (TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI + TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI) +
    (TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re + TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re) =
  TrivSqZeroExt.fst x.re * TrivSqZeroExt.snd y.imK + TrivSqZeroExt.fst x.imI * TrivSqZeroExt.snd y.imJ -
        TrivSqZeroExt.fst x.imJ * TrivSqZeroExt.snd y.imI +
      TrivSqZeroExt.fst x.imK * TrivSqZeroExt.snd y.re +
    (TrivSqZeroExt.snd x.re * TrivSqZeroExt.fst y.imK + TrivSqZeroExt.snd x.imI * TrivSqZeroExt.fst y.imJ -
        TrivSqZeroExt.snd x.imJ * TrivSqZeroExt.fst y.imI +
      TrivSqZeroExt.snd x.imK * TrivSqZeroExt.fst y.re)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
⊢ a * b / b = a
have refine : a - a * b / b = 0
Tactic: refine (eq_of_sub_eq_zero ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
⊢ a - a * b / b = 0
have by_contra : ∀ (h : ¬a - a * b / b = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
⊢ False
have this : ¬(a - a * b / b) * b ≺ b
Tactic: have := mul_right_not_lt b h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
h : ¬a - a * b / b = 0
this : ¬(a - a * b / b) * b ≺ b
⊢ False
have this₁ : ¬a * b % b ≺ b
Tactic: rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)
have rw : a - b * (a / b) = a - b * (a / b)
Tactic: rw [div_add_mod]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ a
have rw : b ∣ b * (a / b)
Tactic: rw [← div_add_mod a b, h, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0
have rw : b * c = b * (b * c / b)
Tactic: rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
have haveI : ∀ (this : (p : Prop) → Decidable p), b * c = b * (b * c / b)
Tactic: haveI := Classical.dec
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
have pos : ∀ (b0 : b = 0), b * c = b * (b * c / b)
Tactic: by_cases b0 : b = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
pos : ∀ (b0 : b = 0), b * c = b * (b * c / b)
⊢ b * c = b * (b * c / b)
have neg : ∀ (b0 : ¬b = 0), b * c = b * (b * c / b)
Tactic: by_cases b0 : b = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
h : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
have neg : b * c = b * c
Tactic: rw [mul_div_cancel_left₀ _ b0]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a % b ↔ c ∣ a
have rw : c ∣ b * (a / b) + a % b ↔ c ∣ a
Tactic: rw [← dvd_add_right (h.mul_right _), div_add_mod]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : c ∣ b
rw : c ∣ b * (a / b) + a % b ↔ c ∣ a
rw₁ : R
⊢ c ∣ a % b ↔ c ∣ a
have rw₂ : c ∣ a ↔ c ∣ a
Tactic: rw [← dvd_add_right (h.mul_right _), div_add_mod]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b
have rw : a = a * b / b
Tactic: rw [← h, mul_div_cancel_right₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
rw : a = a * b / b
⊢ a = c / b
have rw₁ : a = a
Tactic: rw [← h, mul_div_cancel_right₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = c / a
have rw : b = a * b / a
Tactic: rw [← h, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
rw : b = a * b / a
⊢ b = c / a
have rw₁ : b = b
Tactic: rw [← h, mul_div_cancel_left₀ _ ha]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
⊢ x * y / z = x * (y / z)
have pos : ∀ (hz : z = 0), x * y / z = x * (y / z)
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
pos : ∀ (hz : z = 0), x * y / z = x * (y / z)
⊢ x * y / z = x * (y / z)
have neg : ∀ (hz : ¬z = 0), x * y / z = x * (y / z)
Tactic: by_cases hz : z = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)
have pos : ∀ (h : 0 ∣ y), x * y / 0 = x * (y / 0)
Tactic: subst hz
Cleared hypotheses: z, h, hz
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ x * y / 0 = x * (y / 0)
have pos : 0 = x * (y / 0)
Tactic: rw [div_zero, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y : R
h : 0 ∣ y
pos : 0 = x * (y / 0)
⊢ x * y / 0 = x * (y / 0)
have pos₁ : 0 = x * 0
Tactic: rw [div_zero, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y : R
h : 0 ∣ y
pos : 0 = x * (y / 0)
pos₁ : 0 = x * 0
⊢ x * y / 0 = x * (y / 0)
have pos₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [div_zero, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)
have neg : ∀ (p : R), x * (z * p) / z = x * (z * p / z)
Tactic: rcases h with ⟨p, rfl⟩
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * (z * p / z)
have neg : x * (z * p) / z = x * p
Tactic: rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
neg : x * (z * p) / z = x * p
⊢ x * (z * p) / z = x * (z * p / z)
have neg₁ : z * (x * p) / z = x * p
Tactic: rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
neg : x * (z * p) / z = x * p
neg₁ : z * (x * p) / z = x * p
⊢ x * (z * p) / z = x * (z * p / z)
have neg₂ : x * p = x * p
Tactic: rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a
have rw : b * a / b = a
Tactic: rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
rw : b * a / b = a
⊢ b * (a / b) = a
have rw₁ : a = a
Tactic: rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
⊢ p / q ∣ p
have pos : ∀ (hq : q = 0), p / q ∣ p
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
pos : ∀ (hq : q = 0), p / q ∣ p
⊢ p / q ∣ p
have neg : ∀ (hq : ¬q = 0), p / q ∣ p
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (hypothesis)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p
have hpq₁ : p = 0
Tactic: rw [hq, zero_dvd_iff] at hpq
Cleared hypotheses: hpq, hq
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p
have pos : 0 / q ∣ 0
Tactic: rw [hpq]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p
have h : p = p / q * q
Tactic: use q
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q
have h : p = q * (p / q)
Tactic: rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
h : p = q * (p / q)
⊢ p = p / q * q
have h₁ : p = q * p / q
Tactic: rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
h : p = q * (p / q)
h₁ : p = q * p / q
⊢ p = p / q * q
have h₂ : p = p * q / q
Tactic: rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
h : p = q * (p / q)
h₁ : p = q * p / q
h₂ : p = p * q / q
⊢ p = p / q * q
have h₃ : p = p
Tactic: rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a
have inl : ∀ (h : 0 * b ∣ c), b ∣ c / 0
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : a * b ∣ c
inl : ∀ (h : 0 * b ∣ c), b ∣ c / 0
⊢ b ∣ c / a
have inr : ∀ (ha : a ≠ 0), b ∣ c / a
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Algebra.EuclideanDomain.Basic (goal)
Goal:
R : Type u
inst : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
have inr : ∀ (d : R), b ∣ a * b * d / a
Tactic: rcases h with ⟨d, rfl⟩
Cleared hypotheses: c, h