awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw :
  (F : (a : A) → B) (q.j * q.i) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.i : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
have rw₁ : (F : (a : A) → B) (c₂ • q.j - q.k) =
  HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
Tactic: rw [← map_mul, q.j_mul_i, map_sub, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw :
  (F : (a : A) → B) (q.j * q.i) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₁ :
  (F : (a : A) → B) (c₂ • q.j - q.k) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.i : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
have rw₂ : HSub.hSub (α := B) (β := B) ((F : (a : A) → B) (c₂ • q.j) : B) ((F : (a : A) → B) q.k : B) =
  HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
Tactic: rw [← map_mul, q.j_mul_i, map_sub, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
F : A →ₐ[R] B
rw :
  (F : (a : A) → B) (q.j * q.i) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₁ :
  (F : (a : A) → B) (c₂ • q.j - q.k) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
rw₂ :
  HSub.hSub (α := B) (β := B) ((F : (a : A) → B) (c₂ • q.j) : B) ((F : (a : A) → B) q.k : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
⊢ HMul.hMul (α := B) (β := B) ((F : (a : A) → B) q.j : B) ((F : (a : A) → B) q.i : B) =
    HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
have rw₃ : HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B) =
  HSub.hSub (β := B) (HSMul.hSMul (β := B) c₂ ((F : (a : A) → B) q.j : B)) ((F : (a : A) → B) q.k : B)
Tactic: rw [← map_mul, q.j_mul_i, map_sub, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ Basis.compHom (Basis.self R) q.liftHom = q
have hi : (Basis.compHom (Basis.self R) q.liftHom).i = q.i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
hi : (Basis.compHom (Basis.self R) q.liftHom).i = q.i
⊢ Basis.compHom (Basis.self R) q.liftHom = q
have hj : (Basis.compHom (Basis.self R) q.liftHom).j = q.j
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
⊢ (Basis.compHom (Basis.self R) F).liftHom = F
have H : ∀ (x : ℍ[R,c₁,c₂,c₃]),
  Eq.{u_2 + 1} (α := A) (((Basis.compHom (Basis.self R) F).liftHom : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
⊢ Eq.{u_2 + 1} (α := A) (((Basis.compHom (Basis.self R) F).liftHom : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
have H : HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A)
        (HSMul.hSMul (β := A) x.imI
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
      HSMul.hSMul (β := A) x.imJ
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
    HSMul.hSMul (β := A) x.imK
      ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
  (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
Tactic: dsimp [Basis.lift]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
⊢ HAdd.hAdd (α := A) ((algebraMap R A : (a : R) → A) x.re : A)
          (HSMul.hSMul (β := A) x.imI
            ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
        HSMul.hSMul (β := A) x.imJ
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
      HSMul.hSMul (β := A) x.imK
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
    (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
have H : HAdd.hAdd (α := A)
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) x.re : ℍ[R,c₁,c₂,c₃]) :
          A)
        (HSMul.hSMul (β := A) x.imI
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
      HSMul.hSMul (β := A) x.imJ
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
    HSMul.hSMul (β := A) x.imK
      ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
  (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
Tactic: rw [← F.commutes]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
⊢ HAdd.hAdd (α := A)
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) ((algebraMap R ℍ[R,c₁,c₂,c₃] : (a : R) → ℍ[R,c₁,c₂,c₃]) x.re : ℍ[R,c₁,c₂,c₃]) :
            A)
          (HSMul.hSMul (β := A) x.imI
            ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 1, imJ := 0, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A)) +
        HSMul.hSMul (β := A) x.imJ
          ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 1, imK := 0 : ℍ[R,c₁,c₂,c₃] } : A) +
      HSMul.hSMul (β := A) x.imK
        ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) { re := 0, imI := 0, imJ := 0, imK := 1 : ℍ[R,c₁,c₂,c₃] } : A) =
    (F : (a : ℍ[R,c₁,c₂,c₃]) → A) x
have H : Eq.{u_2 + 1} (α := A)
  ((F : (a : ℍ[R,c₁,c₂,c₃]) → A)
      { re := x.re + 0 + 0 + 0, imI := 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0,
        imJ := HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0,
        imK := HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 } :
    A)
  ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
Tactic: simp only [← map_smul, ← map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
⊢ Eq.{u_2 + 1} (α := A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A)
        { re := x.re + 0 + 0 + 0, imI := 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0,
          imJ := HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0,
          imK := HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 } :
      A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
have H : x.re + 0 + 0 + 0 = x.re
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
H : x.re + 0 + 0 + 0 = x.re
⊢ Eq.{u_2 + 1} (α := A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A)
        { re := x.re + 0 + 0 + 0, imI := 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0,
          imJ := HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0,
          imK := HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 } :
      A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
have H₁ : 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0 = x.imI
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
H : x.re + 0 + 0 + 0 = x.re
H₁ : 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0 = x.imI
⊢ Eq.{u_2 + 1} (α := A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A)
        { re := x.re + 0 + 0 + 0, imI := 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0,
          imJ := HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0,
          imK := HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 } :
      A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
have H₂ : HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0 = x.imJ
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.QuaternionBasis (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Ring B
inst_3 : Algebra R A
inst_4 : Algebra R B
c₁ c₂ c₃ : R
F : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
x : ℍ[R,c₁,c₂,c₃]
H : x.re + 0 + 0 + 0 = x.re
H₁ : 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0 = x.imI
H₂ : HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0 = x.imJ
⊢ Eq.{u_2 + 1} (α := A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A)
        { re := x.re + 0 + 0 + 0, imI := 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0,
          imJ := HAdd.hAdd (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0,
          imK := HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 } :
      A)
    ((F : (a : ℍ[R,c₁,c₂,c₃]) → A) x : A)
have H₃ : HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 = x.imK
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (hypothesis)
Goal:
R : Type u_1
inst : Mul R
a : R
ca : ∀ (b : R), Commute a b
h : IsRightRegular a
⊢ IsLeftRegular a
have ca₁ : ∀ (b : R), Commute b a
Tactic: simp only [@Commute.symm_iff R _ a] at ca
Cleared hypotheses: ca
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := R) ((fun (x : R) ↦ a * x) ∘ fun (x : R) ↦ b * x)
have rwa : Function.Injective (β := R) fun (x : R) ↦ a * b * x
Tactic: rwa [comp_mul_left a b]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b
have refine : ∀ (x y : R) (xy : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * b) x) ((fun (x : R) ↦ x * b) y)), x * (b * a) = y * (b * a)
Tactic: refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * b) x) ((fun (x : R) ↦ x * b) y)
⊢ x * (b * a) = y * (b * a)
have rw : x * b * a = y * b * a
Tactic: rw [← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
have refine_1 : IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Semigroup R
a b : R
refine_1 : IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
have refine_2 : IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
have refine : IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
Tactic: refine Iff.trans ?_ isRegular_mul_and_mul_iff
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (b * a)
have rw : IsLeftRegular.{u_1} (R := R) 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular (a * b)
have rw : IsRightRegular.{u_1} (R := R) 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a : R
ua : IsUnit a
⊢ IsRegular a
have rcases : ∀ (a : Rˣ), IsRegular (↑a : R)
Tactic: rcases ua with ⟨a, rfl⟩
Cleared hypotheses: a, ua
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)
have rw : Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (fun (x : R) ↦ x * a)^[n]
Tactic: rw [IsRightRegular, ← mul_right_iterate]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a
have rw : IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
Tactic: rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a
have rw : IsRightRegular (a * a ^ n.pred) → IsRightRegular a
Tactic: rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ b = 1
have rwa : a * b = a * 1
Tactic: rwa [← ha.eq_iff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
⊢ a * b = a
have rw : a * 1 = a
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
rw : a * 1 = a
⊢ a * b = a
have rw₁ : a = a
Tactic: rw [h, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b = 1
have rwa : b * a = 1 * a
Tactic: rwa [← ha.eq_iff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ b * a = a
have rw : 1 * a = a
Tactic: rw [h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
rw : 1 * a = a
⊢ b * a = a
have rw₁ : a = a
Tactic: rw [h, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
| ∀ ⦃a₁ a₂ : M⦄, n • a₁ = n • a₂ → a₁ = a₂
have rw : ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
Tactic: rw [← n.sign_mul_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔ ∀ ⦃a₁ a₂ : M⦄, n • a₁ = n • a₂ → a₁ = a₂
have conv_rhs : (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
  ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
Tactic: conv_rhs => rw [← n.sign_mul_natAbs]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
have inl : ∀ (h : n.sign = 1),
  (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
Tactic: obtain h | h | h := n.sign_trichotomy
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
inl :
  ∀ (h : n.sign = 1),
    (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
      ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
have inr : ∀ (h : n.sign = 0),
  (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
Tactic: obtain h | h | h := n.sign_trichotomy
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
inl :
  ∀ (h : n.sign = 1),
    (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
      ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
inr :
  ∀ (h : n.sign = 0),
    (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
      ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
have inr₁ : ∀ (h : n.sign = -1),
  (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
Tactic: obtain h | h | h := n.sign_trichotomy
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (hypothesis)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst : SMul R M
inst_1 : SMul R S
inst_2 : SMul S M
inst_3 : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : a • s • c = a • s • d
⊢ c = d
have cd₁ : (a • s) • c = (a • s) • d
Tactic: rw [← smul_assoc, ← smul_assoc] at cd
Cleared hypotheses: cd
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (hypothesis)
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : SMul R M
inst_1 : Mul R
inst_2 : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b
have ab₁ : IsSMulRegular M (a • b)
Tactic: rw [← smul_eq_mul] at ab
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : SMul R M
inst_1 : Mul R
inst_2 : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
have refine_1 : IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : SMul R M
inst_1 : Mul R
inst_2 : IsScalarTower R R M
refine_1 : IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
have refine_2 : IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : Monoid R
inst_1 : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (a * b)
have rw : IsSMulRegular.{u_1, u_3} (R := R) M 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (HPow.hPow (β := ℕ) a 0)
have zero : IsSMulRegular.{u_1, u_3} (R := R) M 1
Tactic: rw [pow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a ^ (n + 1))
have succ : IsSMulRegular M (a * a ^ n)
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)
have zero : IsSMulRegular M (HPow.hPow (β := ℕ) a 0)
Tactic: induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
ra : IsSMulRegular M a
zero : IsSMulRegular M (HPow.hPow (β := ℕ) a 0)
⊢ IsSMulRegular M (a ^ n)
have succ : ∀ (n : ℕ) (hn : IsSMulRegular M (a ^ n)), IsSMulRegular M (a ^ (n + 1))
Tactic: induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
have refine : IsSMulRegular M (a ^ n) → IsSMulRegular M a
Tactic: refine ⟨?_, pow n⟩
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a
have rw : IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
Tactic: rw [← Nat.succ_pred_eq_of_pos n0, pow_succ, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst : Monoid S
inst_1 : SMul R M
inst_2 : SMul R S
inst_3 : MulAction S M
inst_4 : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M (a • s)
have rw : IsSMulRegular.{u_2, u_3} (R := S) M 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
h : IsSMulRegular.{u_1, u_3} (R := R) M 0
a b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
have rw : 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
Tactic: rw [MulActionWithZero.zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
h : IsSMulRegular.{u_1, u_3} (R := R) M 0
a b : M
⊢ 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
have rw : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [MulActionWithZero.zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
h : IsSMulRegular.{u_1, u_3} (R := R) M 0
a b : M
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
have repeat' : 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
Tactic: repeat' rw [MulActionWithZero.zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Regular.SMul (goal)
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
⊢ ¬IsSMulRegular.{u_1, u_3} (R := R) M 0 ↔ Nontrivial M
have rw : (¬∃ (x : M), ∃ (y : M), x ≠ y) ↔ ∀ (x y : M), x = y
Tactic: rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]