awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuaternionBasis
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 :
  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)
⊢ 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:
simp only [← map_smul, ← map_add, mk_add_mk, smul_mk, smul_zero, algebraMap_eq]

Premises used: QuaternionAlgebra.smul_mk, smul_zero, map_add, QuaternionAlgebra.algebraMap_eq, QuaternionAlgebra.mk_add_mk, map_smul
-- Module: Mathlib.Algebra.QuaternionBasis
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
H₃ : HAdd.hAdd (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 = x.imK
⊢ 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:
congr
-- Module: Mathlib.Algebra.QuaternionBasis
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₃]
⊢ x.re + 0 + 0 + 0 = x.re

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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₃]
⊢ 0 + HSMul.hSMul (β := R) x.imI 1 + 0 + 0 = x.imI

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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 (α := R) 0 0 + HSMul.hSMul (β := R) x.imJ 1 + 0 = x.imJ

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
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 (α := R) 0 0 + 0 + HSMul.hSMul (β := R) x.imK 1 = x.imK

Tactic:
simp
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
c₁ c₂ c₃ : R
f g : ℍ[R,c₁,c₂,c₃] →ₐ[R] A
hi :
  Eq.{u_2 + 1} (α := A) ((f : (a : ℍ[R,c₁,c₂,c₃]) → A) (Basis.i (Basis.self R)) : A)
    ((g : (a : ℍ[R,c₁,c₂,c₃]) → A) (Basis.i (Basis.self R)) : A)
hj :
  Eq.{u_2 + 1} (α := A) ((f : (a : ℍ[R,c₁,c₂,c₃]) → A) (Basis.j (Basis.self R)) : A)
    ((g : (a : ℍ[R,c₁,c₂,c₃]) → A) (Basis.j (Basis.self R)) : A)
⊢ f = g

Tactic:
lift.symm.injective <| Basis.ext hi hj

Premises used: QuaternionAlgebra.lift, Equiv.injective, Equiv.symm, QuaternionAlgebra.Basis.ext
-- Module: Mathlib.Algebra.QuaternionBasis
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
f g : ℍ[R] →ₐ[R] A
hi :
  Eq.{u_2 + 1} (α := A) ((f : (a : ℍ[R]) → A) (Basis.i (Basis.self R)) : A)
    ((g : (a : ℍ[R]) → A) (Basis.i (Basis.self R)) : A)
hj :
  Eq.{u_2 + 1} (α := A) ((f : (a : ℍ[R]) → A) (Basis.j (Basis.self R)) : A)
    ((g : (a : ℍ[R]) → A) (Basis.j (Basis.self R)) : A)
⊢ f = g

Tactic:
QuaternionAlgebra.hom_ext hi hj

Premises used: QuaternionAlgebra.hom_ext, Quaternion
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
ca : ∀ (b : R), Commute a b
h : IsLeftRegular a
⊢ IsRightRegular a

Tactic:
fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm

Premises used: Commute.symm, Function.Injective, Eq.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
ca : ∀ (b : R), Commute a b
h : IsRightRegular a
⊢ ∀ (b : R), Commute b a

Tactic:
simp only [@Commute.symm_iff R _ a] at ca

Premises used: Commute.symm_iff
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
h : IsRightRegular a
ca : ∀ (b : R), Commute b a
⊢ IsLeftRegular a

Tactic:
fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm

Premises used: Commute.symm, Function.Injective, Eq.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
h : IsRightRegular a
ca : ∀ (b : R), Commute b a
⊢ IsLeftRegular a

Tactic:
exact fun x y xy => h <| (ca x).trans <| xy.trans <| (ca y).symm

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
ca : ∀ (b : R), Commute a b
⊢ IsRightRegular a ↔ IsLeftRegular a

Tactic:
⟨IsRightRegular.left_of_commute ca, IsLeftRegular.right_of_commute ca⟩

Premises used: IsRightRegular.left_of_commute, Iff.intro, IsLeftRegular.right_of_commute
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Mul R
a : R
ca : ∀ (b : R), Commute a b
⊢ IsRegular a ↔ IsLeftRegular a

Tactic:
⟨fun h => h.left, fun h => ⟨h, h.right_of_commute ca⟩⟩

Premises used: IsRegular.mk, Iff.intro, IsRegular.left, IsLeftRegular.right_of_commute
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
lra : IsLeftRegular a
lrb : IsLeftRegular b
⊢ IsLeftRegular (a * b)

Tactic:
show Function.Injective (((a * b) * ·)) from comp_mul_left a b ▸ lra.comp lrb

Premises used: Eq.rec, comp_mul_left, Function.Injective.comp
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
rra : IsRightRegular a
rrb : IsRightRegular b
⊢ IsRightRegular (a * b)

Tactic:
show Function.Injective (· * (a * b)) from comp_mul_right b a ▸ rrb.comp rra

Premises used: Eq.rec, comp_mul_right, Function.Injective.comp
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
rra : IsRegular a
rrb : IsRegular b
⊢ IsRegular (a * b)

Tactic:
⟨rra.left.mul rrb.left, rra.right.mul rrb.right⟩

Premises used: IsRightRegular.mul, IsRegular.right, IsLeftRegular.mul, IsRegular.mk, IsRegular.left
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
rwa rwa₁ rwa₂ rwa₃ : Function.Injective (β := R) fun (x : R) ↦ a * b * x
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := R) ((fun (x : R) ↦ a * x) ∘ fun (x : R) ↦ b * x)

Tactic:
rwa [comp_mul_left a b]

Premises used: comp_mul_left
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ha : IsLeftRegular a
⊢ IsLeftRegular (a * b) ↔ IsLeftRegular b

Tactic:
⟨fun ab => IsLeftRegular.of_mul ab, fun ab => IsLeftRegular.mul ha ab⟩

Premises used: IsLeftRegular.of_mul, IsLeftRegular.mul, Iff.intro
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b

Tactic:
fun x y xy => ab (?_ : x * (b * a) = y * (b * a))

Premises used: Function.Injective
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRightRegular (b * a)
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)
⊢ IsRightRegular b

Tactic:
refine fun x y xy => ab (?_ : x * (b * a) = y * (b * a))
-- Module: Mathlib.Algebra.Regular.Basic
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)
rw : x * b * a = y * b * a
⊢ x * (b * a) = y * (b * a)

Tactic:
rw [← mul_assoc, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Regular.Basic
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

Tactic:
congr_arg (· * a) xy

Premises used: HMul.hMul, congr_arg
-- Module: Mathlib.Algebra.Regular.Basic
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

Tactic:
exact congr_arg (· * a) xy

Premises used: HMul.hMul, congr_arg
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ha : IsRightRegular a
⊢ IsRightRegular (b * a) ↔ IsRightRegular b

Tactic:
⟨fun ab => IsRightRegular.of_mul ab, fun ab => IsRightRegular.mul ab ha⟩

Premises used: IsRightRegular.of_mul, IsRightRegular.mul, Iff.intro
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
refine_1 : IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
refine_2 : IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Tactic:
⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩

Premises used: IsRightRegular.of_mul, IsLeftRegular.of_mul, IsRegular.right, IsRegular.mk, And.intro, IsRegular.left
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Tactic:
exact
      ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
        ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
⟨ha.mul hb, hb.mul ha⟩

Premises used: IsRegular.mul, And.intro
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Tactic:
isRegular_mul_and_mul_iff.mp ⟨ab, ba⟩

Premises used: isRegular_mul_and_mul_iff, And.intro, Iff.mp
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : MulOneClass R
⊢ IsRegular.{u_1} (R := R) 1

Tactic:
⟨fun a b ab => (one_mul a).symm.trans (Eq.trans ab (one_mul b)), fun a b ab =>
    (mul_one a).symm.trans (Eq.trans ab (mul_one b))⟩

Premises used: IsRegular.mk, mul_one, Eq.symm, one_mul, Eq.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

Tactic:
Iff.trans ?_ isRegular_mul_and_mul_iff

Premises used: isRegular_mul_and_mul_iff, Iff.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : CommSemigroup R
a b : R
refine : IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine Iff.trans ?_ isRegular_mul_and_mul_iff

Premises used: isRegular_mul_and_mul_iff, Iff.trans
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : CommSemigroup R
a b : R
ab : IsRegular (a * b)
rwa rwa₁ rwa₂ rwa₃ : IsRegular (a * b)
⊢ IsRegular (b * a)

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : b * a = 1
rw : IsLeftRegular.{u_1} (R := R) 1
⊢ IsLeftRegular (b * a)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular.{u_1} (R := R) 1

Tactic:
isRegular_one.left

Premises used: IsRegular.left, isRegular_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular.{u_1} (R := R) 1

Tactic:
exact isRegular_one.left

Premises used: IsRegular.left, isRegular_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : a * b = 1
rw : IsRightRegular.{u_1} (R := R) 1
⊢ IsRightRegular (a * b)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular.{u_1} (R := R) 1

Tactic:
isRegular_one.right

Premises used: IsRegular.right, isRegular_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular.{u_1} (R := R) 1

Tactic:
exact isRegular_one.right

Premises used: IsRegular.right, isRegular_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : Rˣ
⊢ IsRegular (↑a : R)

Tactic:
⟨isLeftRegular_of_mul_eq_one a.inv_mul, isRightRegular_of_mul_eq_one a.mul_inv⟩

Premises used: Units.inv_mul, Units.mul_inv, isLeftRegular_of_mul_eq_one, IsRegular.mk, isRightRegular_of_mul_eq_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
ua : IsUnit a
rcases : ∀ (a : Rˣ), IsRegular (↑a : R)
⊢ IsRegular a

Tactic:
rcases ua with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : Rˣ
⊢ IsRegular (↑a : R)

Tactic:
Units.isRegular a

Premises used: Units.isRegular
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : Rˣ
⊢ IsRegular (↑a : R)

Tactic:
exact Units.isRegular a

Premises used: Units.isRegular
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)

Tactic:
simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]

Premises used: mul_left_iterate, Function.Injective.iterate, IsLeftRegular
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
rw : Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (fun (x : R) ↦ x * a)^[n]
⊢ IsRightRegular (a ^ n)

Tactic:
rw [IsRightRegular, ← mul_right_iterate]

Premises used: IsRightRegular, mul_right_iterate
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (fun (x : R) ↦ x * a)^[n]

Tactic:
rra.iterate n

Premises used: Function.Injective.iterate
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (fun (x : R) ↦ x * a)^[n]

Tactic:
exact rra.iterate n

Premises used: Function.Injective.iterate
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
ra : IsRegular a
⊢ IsRegular (a ^ n)

Tactic:
⟨IsLeftRegular.pow n ra.left, IsRightRegular.pow n ra.right⟩

Premises used: IsRegular.right, IsLeftRegular.pow, IsRegular.mk, IsRegular.left, IsRightRegular.pow
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
rw : IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ]

Premises used: Nat.succ_pred_eq_of_pos, pow_succ
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a

Tactic:
.of_mul

Premises used: IsLeftRegular.of_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred * a) → IsLeftRegular a

Tactic:
exact .of_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
rw : IsRightRegular (a * a ^ n.pred) → IsRightRegular a
⊢ IsRightRegular (a ^ n) → IsRightRegular a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']

Premises used: Nat.succ_pred_eq_of_pos, pow_succ'
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Tactic:
.of_mul

Premises used: IsRightRegular.of_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a * a ^ n.pred) → IsRightRegular a

Tactic:
exact .of_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
rwa : a * b = a * 1
rwa₁ rwa₂ rwa₃ rwa₄ : a * b = a
⊢ b = 1

Tactic:
rwa [← ha.eq_iff, mul_one]

Premises used: Function.Injective.eq_iff, mul_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
rw : a * 1 = a
rw₁ rw₂ : a = a
⊢ a * b = a

Tactic:
rw [h, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
rwa : b * a = 1 * a
rwa₁ rwa₂ rwa₃ rwa₄ : b * a = a
⊢ b = 1

Tactic:
rwa [← ha.eq_iff, one_mul]

Premises used: Function.Injective.eq_iff, one_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
rw : 1 * a = a
rw₁ rw₂ : a = a
⊢ b * a = a

Tactic:
rw [h, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
h : ∀ (x y : R), x * y = 1 → IsLeftRegular x
a b : R
eq : a * b = 1
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a * x) (b * a)) ((fun (x : R) ↦ a * x) 1)

Tactic:
simp [← mul_assoc, eq]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Regular.Basic
Goal:
R : Type u_1
inst : Monoid R
h : ∀ (x y : R), x * y = 1 → IsRightRegular y
a b : R
eq : a * b = 1
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ x * b) (b * a)) ((fun (x : R) ↦ x * b) 1)

Tactic:
simp [mul_assoc, eq]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Regular.Defs
Goal:
R : Type u_1
inst : Mul R
c : R
⊢ IsRegular c ↔ IsLeftRegular c ∧ IsRightRegular c

Tactic:
⟨fun ⟨h1, h2⟩ => ⟨h1, h2⟩, fun ⟨h1, h2⟩ => ⟨h1, h2⟩⟩

Premises used: IsRegular, _private.0.isRegular_iff.match_2, IsLeftRegular, IsRegular.mk, IsRightRegular, And, _private.0.isRegular_iff.match_1, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : R
⊢ IsLeftRegular (op a) ↔ IsRightRegular a

Tactic:
opEquiv.comp_injective _ |>.trans <| opEquiv.injective_comp _ |>.symm

Premises used: MulOpposite.opEquiv, Equiv.injective_comp, Iff.trans, Equiv.comp_injective, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : R
⊢ IsRightRegular (op a) ↔ IsLeftRegular a

Tactic:
opEquiv.comp_injective _ |>.trans <| opEquiv.injective_comp _ |>.symm

Premises used: MulOpposite.opEquiv, Equiv.injective_comp, Iff.trans, Equiv.comp_injective, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : R
⊢ IsRegular (op a) ↔ IsRegular a

Tactic:
simp [isRegular_iff, and_comm]

Premises used: isRegular_iff, and_comm
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : Rᵐᵒᵖ
⊢ IsLeftRegular (unop a) ↔ IsRightRegular a

Tactic:
isRightRegular_op.symm

Premises used: MulOpposite, isRightRegular_op, MulOpposite.unop, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : Rᵐᵒᵖ
⊢ IsRightRegular (unop a) ↔ IsLeftRegular a

Tactic:
isLeftRegular_op.symm

Premises used: MulOpposite, isLeftRegular_op, MulOpposite.unop, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Regular.Opposite
Goal:
R : Type u_1
inst : Mul R
a : Rᵐᵒᵖ
⊢ IsRegular (unop a) ↔ IsRegular a

Tactic:
isRegular_op.symm

Premises used: MulOpposite, isRegular_op, MulOpposite.unop, Iff.symm, MulOpposite.op
-- Module: Mathlib.Algebra.Regular.Pi
Goal:
ι : Type u_1
R : ι → Type u_3
inst : (i : ι) → Mul (R i)
a : (i : ι) → R i
⊢ IsLeftRegular a ↔ ∀ (i : ι), IsLeftRegular (a i)

Tactic:
have (i : _) : Nonempty (R i) := ⟨a i⟩; Pi.map_injective

Premises used: Pi.map_injective, Pi.map, Nonempty.intro
-- Module: Mathlib.Algebra.Regular.Pi
Goal:
ι : Type u_1
R : ι → Type u_3
inst : (i : ι) → Mul (R i)
a : (i : ι) → R i
⊢ IsRightRegular a ↔ ∀ (i : ι), IsRightRegular (a i)

Tactic:
have (i : _) : Nonempty (R i) := ⟨a i⟩; .symm <| Pi.map_injective.symm

Premises used: Pi.map_injective, Nonempty.intro, Iff.symm
-- Module: Mathlib.Algebra.Regular.Pi
Goal:
ι : Type u_1
R : ι → Type u_3
inst : (i : ι) → Mul (R i)
a : (i : ι) → R i
⊢ IsRegular a ↔ ∀ (i : ι), IsRegular (a i)

Tactic:
simp [_root_.isRegular_iff, forall_and]

Premises used: isRegular_iff, forall_and
-- Module: Mathlib.Algebra.Regular.Pi
Goal:
ι : Type u_1
α : Type u_2
R : ι → Type u_3
inst : (i : ι) → SMul.{u_2, u_3} α (R i)
r : α
inst_1 : ∀ (i : ι), Nonempty.{u_3 + 1} (R i)
⊢ IsSMulRegular ((i : ι) → R i) r ↔ ∀ (i : ι), IsSMulRegular.{u_2, u_3} (R i) r

Tactic:
Pi.map_injective

Premises used: Pi.map_injective, Pi.map, IsSMulRegular
-- Module: Mathlib.Algebra.Regular.Pow
Goal:
ι : Type u_2
R : Type u_3
inst : CommMonoid R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, IsLeftRegular (f i)
⊢ IsLeftRegular.{u_3} (R := R) (∏ i ∈ s, f i)

Tactic:
s.prod_induction _ _ (@IsLeftRegular.mul R _) isRegular_one.left h

Premises used: IsLeftRegular.mul, Finset.prod_induction, IsRegular.left, isRegular_one
-- Module: Mathlib.Algebra.Regular.Pow
Goal:
ι : Type u_2
R : Type u_3
inst : CommMonoid R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, IsRightRegular (f i)
⊢ IsRightRegular.{u_3} (R := R) (∏ i ∈ s, f i)

Tactic:
s.prod_induction _ _ (@IsRightRegular.mul R _) isRegular_one.right h

Premises used: IsRightRegular.mul, IsRegular.right, Finset.prod_induction, isRegular_one
-- Module: Mathlib.Algebra.Regular.Pow
Goal:
ι : Type u_2
R : Type u_3
inst : CommMonoid R
s : Finset ι
f : ι → R
h : ∀ i ∈ s, IsRegular (f i)
⊢ IsRegular.{u_3} (R := R) (∏ i ∈ s, f i)

Tactic:
⟨IsLeftRegular.prod fun a ha ↦ (h a ha).left,
   IsRightRegular.prod fun a ha ↦ (h a ha).right⟩

Premises used: IsRightRegular.prod, IsRegular.right, IsRegular.mk, IsLeftRegular.prod, IsRegular.left
-- Module: Mathlib.Algebra.Regular.Prod
Goal:
R : Type u_2
S : Type u_3
inst : Mul R
inst_1 : Mul S
a : R
b : S
⊢ IsLeftRegular (a, b) ↔ IsLeftRegular a ∧ IsLeftRegular b

Tactic:
have : Nonempty R := ⟨a⟩; have : Nonempty S := ⟨b⟩; Prod.map_injective

Premises used: Prod.map, Nonempty.intro, Prod.map_injective
-- Module: Mathlib.Algebra.Regular.Prod
Goal:
R : Type u_2
S : Type u_3
inst : Mul R
inst_1 : Mul S
a : R
b : S
⊢ IsRightRegular (a, b) ↔ IsRightRegular a ∧ IsRightRegular b

Tactic:
have : Nonempty R := ⟨a⟩; have : Nonempty S := ⟨b⟩; Iff.symm <| Prod.map_injective |>.symm

Premises used: Nonempty.intro, Prod.map_injective, Iff.symm
-- Module: Mathlib.Algebra.Regular.Prod
Goal:
R : Type u_2
S : Type u_3
inst : Mul R
inst_1 : Mul S
a : R
b : S
⊢ IsRegular (a, b) ↔ IsRegular a ∧ IsRegular b

Tactic:
simp [isRegular_iff, and_and_and_comm]

Premises used: isRegular_iff, and_and_and_comm