awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ha : IsLeftRegular a
hb : IsLeftRegular b
⊢ IsLeftRegular (a, b)

Tactic:
Prod.isLeftRegular_mk.2 ⟨ha, hb⟩

Premises used: Iff.mpr, Prod.isLeftRegular_mk, And.intro
-- 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
ha : IsRightRegular a
hb : IsRightRegular b
⊢ IsRightRegular (a, b)

Tactic:
Prod.isRightRegular_mk.2 ⟨ha, hb⟩

Premises used: Iff.mpr, Prod.isRightRegular_mk, And.intro
-- 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
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a, b)

Tactic:
Prod.isRegular_mk.2 ⟨ha, hb⟩

Premises used: Iff.mpr, Prod.isRegular_mk, And.intro
-- Module: Mathlib.Algebra.Regular.Prod
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : SMul α R
inst_1 : SMul α S
r : α
inst_2 : Nonempty R
inst_3 : Nonempty S
⊢ IsSMulRegular (R × S) r ↔ IsSMulRegular R r ∧ IsSMulRegular S r

Tactic:
Prod.map_injective

Premises used: Prod.map, Prod.map_injective, IsSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
c : R
h : IsLeftRegular c
⊢ IsSMulRegular R c

Tactic:
h

Premises used: IsSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
a : R
⊢ IsLeftRegular a ↔ IsSMulRegular R a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
c : R
h : IsRightRegular c
⊢ IsSMulRegular R (MulOpposite.op c)

Tactic:
h

Premises used: IsSMulRegular, MulOpposite.unop
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
a : R
⊢ IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsSMulRegular, MulOpposite.unop
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
inst : SMul R M
inst_1 : SMul S M
f : R → S
smul : ∀ (m : M), f a • m = a • m
⊢ IsSMulRegular M (f a) ↔ IsSMulRegular M a

Tactic:
simp [IsSMulRegular, smul]

Premises used: IsSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
rw : ∀ ⦃a₁ a₂ : M⦄, (n.sign * (↑n.natAbs : ℤ)) • a₁ = (n.sign * (↑n.natAbs : ℤ)) • a₂ → a₁ = a₂
| ∀ ⦃a₁ a₂ : M⦄, n • a₁ = n • a₂ → a₁ = a₂

Tactic:
rw [← n.sign_mul_natAbs]

Premises used: Int.sign_mul_natAbs
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
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₂
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔ ∀ ⦃a₁ a₂ : M⦄, n • a₁ = n • a₂ → a₁ = a₂

Tactic:
conv_rhs => rw [← n.sign_mul_natAbs]

Premises used: Int.sign_mul_natAbs
-- Module: Mathlib.Algebra.Regular.SMul
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₂
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₂
⊢ (∀ ⦃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

Premises used: Int.sign_trichotomy
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
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:
simp [h]
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
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:
simp [Int.sign_eq_zero_iff_zero.mp h]

Premises used: Iff.mp, Int.sign_eq_zero_iff_zero
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
M : Type u_3
inst : SubtractionMonoid M
n : ℤ
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:
simp [h, neg_zsmul]

Premises used: neg_zsmul
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst : SMul R M
inst_1 : SMul R S
inst_2 : SMul S M
inst_3 : IsScalarTower R S M
ra : IsSMulRegular M a
rs : IsSMulRegular M s
⊢ IsSMulRegular M (a • s)

Tactic:
fun _ _ ab => rs (ra ((smul_assoc _ _ _).symm.trans (ab.trans (smul_assoc _ _ _))))

Premises used: smul_assoc, IsSMulRegular, Function.Injective, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Regular.SMul
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
⊢ (a • s) • c = (a • s) • d

Tactic:
rw [← smul_assoc, ← smul_assoc] at cd

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

Tactic:
ab cd
-- Module: Mathlib.Algebra.Regular.SMul
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

Tactic:
exact ab cd
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
inst : SMul R M
inst_1 : SMul R S
inst_2 : SMul S M
inst_3 : IsScalarTower R S M
b : S
ha : IsSMulRegular M a
⊢ IsSMulRegular M (a • b) ↔ IsSMulRegular M b

Tactic:
⟨of_smul _, ha.smul⟩

Premises used: IsSMulRegular.of_smul, IsSMulRegular.smul, Iff.intro
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
a : R
h : IsSMulRegular R a
⊢ IsLeftRegular a

Tactic:
h
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
inst : Mul R
a : R
h : IsSMulRegular R (MulOpposite.op a)
⊢ IsRightRegular a

Tactic:
h

Premises used: MulOpposite.unop
-- Module: Mathlib.Algebra.Regular.SMul
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
ra : IsSMulRegular M a
rb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b)

Tactic:
ra.smul rb

Premises used: IsSMulRegular.smul
-- Module: Mathlib.Algebra.Regular.SMul
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 (a • b)

Tactic:
rw [← smul_eq_mul] at ab

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

Tactic:
ab.of_smul _

Premises used: IsSMulRegular.of_smul
-- Module: Mathlib.Algebra.Regular.SMul
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

Tactic:
exact ab.of_smul _

Premises used: IsSMulRegular.of_smul
-- Module: Mathlib.Algebra.Regular.SMul
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
ha : IsSMulRegular M a
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M b

Tactic:
⟨of_mul, ha.mul⟩

Premises used: IsSMulRegular.of_mul, IsSMulRegular.mul, Iff.intro
-- Module: Mathlib.Algebra.Regular.SMul
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

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Regular.SMul
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
refine_2 : IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Algebra.Regular.SMul
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)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
⟨ba.of_mul, ab.of_mul⟩

Premises used: IsSMulRegular.of_mul, And.intro
-- Module: Mathlib.Algebra.Regular.SMul
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)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
exact ⟨ba.of_mul, ab.of_mul⟩
-- Module: Mathlib.Algebra.Regular.SMul
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
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

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

Premises used: IsSMulRegular.mul, And.intro
-- Module: Mathlib.Algebra.Regular.SMul
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
ha : IsSMulRegular M a
hb : IsSMulRegular M b
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Monoid R
inst_1 : MulAction R M
a b : M
ab : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 a = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 b
⊢ a = b

Tactic:
rw [one_smul, one_smul] at ab

Premises used: one_smul
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Monoid R
inst_1 : MulAction R M
a b : M
ab : a = b
⊢ a = b

Tactic:
assumption
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : Monoid R
inst_1 : MulAction R M
h : a * b = 1
rw : IsSMulRegular.{u_1, u_3} (R := R) M 1
⊢ IsSMulRegular M (a * b)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Regular.SMul
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.{u_1, u_3} (R := R) M 1

Tactic:
one M

Premises used: IsSMulRegular.one
-- Module: Mathlib.Algebra.Regular.SMul
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.{u_1, u_3} (R := R) M 1

Tactic:
exact one M

Premises used: IsSMulRegular.one
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ra : IsSMulRegular M a
zero : IsSMulRegular.{u_1, u_3} (R := R) M 1
⊢ IsSMulRegular M (HPow.hPow (β := ℕ) a 0)

Tactic:
rw [pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular.{u_1, u_3} (R := R) M 1

Tactic:
simp only [one]

Premises used: IsSMulRegular.one
-- Module: Mathlib.Algebra.Regular.SMul
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)
succ : IsSMulRegular M (a * a ^ n)
⊢ IsSMulRegular M (a ^ (n + 1))

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Regular.SMul
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 * a ^ n)

Tactic:
(ra.smul_iff (a ^ n)).mpr hn

Premises used: Iff.mpr, HPow.hPow, IsSMulRegular.smul_iff
-- Module: Mathlib.Algebra.Regular.SMul
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 * a ^ n)

Tactic:
exact (ra.smul_iff (a ^ n)).mpr hn

Premises used: Iff.mpr, HPow.hPow, IsSMulRegular.smul_iff
-- Module: Mathlib.Algebra.Regular.SMul
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)
succ : ∀ (n : ℕ) (hn : IsSMulRegular M (a ^ n)), IsSMulRegular M (a ^ (n + 1))
⊢ IsSMulRegular M (a ^ n)

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

Premises used: pow_zero, IsSMulRegular.one, pow_succ'
-- Module: Mathlib.Algebra.Regular.SMul
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

Tactic:
⟨?_, pow n⟩

Premises used: Iff.intro, IsSMulRegular.pow
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
n0 : 0 < n
refine : IsSMulRegular M (a ^ n) → IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

Tactic:
refine ⟨?_, pow n⟩
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
n : ℕ
n0 : 0 < n
rw : IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a

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

Premises used: Nat.succ_pred_eq_of_pos, pow_succ, smul_eq_mul
-- Module: Mathlib.Algebra.Regular.SMul
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.pred • a) → IsSMulRegular M a

Tactic:
of_smul _

Premises used: IsSMulRegular.of_smul
-- Module: Mathlib.Algebra.Regular.SMul
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.pred • a) → IsSMulRegular M a

Tactic:
exact of_smul _

Premises used: IsSMulRegular.of_smul
-- Module: Mathlib.Algebra.Regular.SMul
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
rw : IsSMulRegular.{u_2, u_3} (R := S) M 1
⊢ IsSMulRegular M (a • s)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Regular.SMul
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.{u_2, u_3} (R := S) M 1

Tactic:
one M

Premises used: IsSMulRegular.one
-- Module: Mathlib.Algebra.Regular.SMul
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.{u_2, u_3} (R := S) M 1

Tactic:
exact one M

Premises used: IsSMulRegular.one
-- Module: Mathlib.Algebra.Regular.SMul
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
rw : 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b

Tactic:
rw [MulActionWithZero.zero_smul]

Premises used: MulActionWithZero.zero_smul
-- Module: Mathlib.Algebra.Regular.SMul
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
rw rw₁ : Eq.{u_3 + 1} (α := M) 0 0
⊢ 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b

Tactic:
rw [MulActionWithZero.zero_smul]

Premises used: MulActionWithZero.zero_smul
-- Module: Mathlib.Algebra.Regular.SMul
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
repeat' repeat'₁ repeat'₂ : 0 = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 a = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 b

Tactic:
repeat' rw [MulActionWithZero.zero_smul]

Premises used: MulActionWithZero.zero_smul
-- Module: Mathlib.Algebra.Regular.SMul
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 ↔ Subsingleton M

Tactic:
⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩

Premises used: Iff.intro, Subsingleton.elim, IsSMulRegular.subsingleton
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
rw : (¬∃ (x : M), ∃ (y : M), x ≠ y) ↔ ∀ (x y : M), x = y
⊢ ¬IsSMulRegular.{u_1, u_3} (R := R) M 0 ↔ Nontrivial M

Tactic:
rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff]

Premises used: subsingleton_iff, nontrivial_iff, IsSMulRegular.zero_iff_subsingleton, not_iff_comm
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
push : (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
⊢ (¬∃ (x : M), ∃ (y : M), x ≠ y) ↔ ∀ (x y : M), x = y

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
sM : Subsingleton M
⊢ IsSMulRegular.{u_1, u_3} (R := R) M 0

Tactic:
zero_iff_subsingleton.mpr sM

Premises used: Iff.mpr, IsSMulRegular.zero_iff_subsingleton
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : MonoidWithZero R
inst_1 : Zero M
inst_2 : MulActionWithZero R M
nM : Nontrivial M
⊢ ¬IsSMulRegular.{u_1, u_3} (R := R) M 0

Tactic:
not_zero_iff.mpr nM

Premises used: Iff.mpr, IsSMulRegular.not_zero_iff
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : CommSemigroup R
inst_1 : SMul R M
inst_2 : IsScalarTower R R M
rw : IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rw [← mul_and_mul_iff]

Premises used: IsSMulRegular.mul_and_mul_iff
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : CommSemigroup R
inst_1 : SMul R M
inst_2 : IsScalarTower R R M
ab rwa rwa₁ rwa₂ rwa₃ : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (b * a)

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a b : R
inst : CommSemigroup R
inst_1 : SMul R M
inst_2 : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g⁻¹ • x) ((fun (x : R) ↦ g • x) x))
    ((fun (x : R) ↦ g⁻¹ • x) ((fun (x : R) ↦ g • x) y))

Tactic:
congr_arg (g⁻¹ • ·) h

Premises used: congr_arg, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
h₁ : x = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) x)
h₂ : y = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) y)
⊢ x = y

Tactic:
convert! congr_arg (g⁻¹ • ·) h using 1

Premises used: congr_arg, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
⊢ x = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) x)

Tactic:
simp [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
G : Type u_4
inst : Group G
inst_1 : MulAction G R
g : G
x y : R
h : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ g • x) x) ((fun (x : R) ↦ g • x) y)
⊢ y = HSMul.hSMul (β := R) g⁻¹ ((fun (x : R) ↦ g • x) y)

Tactic:
simp [← smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Monoid R
inst_1 : MulAction R M
a : Rˣ
⊢ IsSMulRegular M (↑a : R)

Tactic:
IsSMulRegular.of_mul_eq_one a.inv_val

Premises used: IsSMulRegular.of_mul_eq_one, Units.inv_val
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
a : R
inst : Monoid R
inst_1 : MulAction R M
ua : IsUnit a
rcases : ∀ (a : Rˣ), IsSMulRegular M (↑a : R)
⊢ IsSMulRegular M a

Tactic:
rcases ua with ⟨a, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Monoid R
inst_1 : MulAction R M
a : Rˣ
⊢ IsSMulRegular M (↑a : R)

Tactic:
a.isSMulRegular M

Premises used: Units.isSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Monoid R
inst_1 : MulAction R M
a : Rˣ
⊢ IsSMulRegular M (↑a : R)

Tactic:
exact a.isSMulRegular M

Premises used: Units.isSMulRegular
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : Zero M
inst_1 : SMulZeroClass R M
r : R
x : M
h1 : IsSMulRegular M r
h2 : r • x = 0
⊢ x = 0

Tactic:
h1 (h2.trans (smul_zero r).symm)

Premises used: smul_zero, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_1
M : Type u_3
inst : AddGroup M
inst_1 : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : Eq.{u_3 + 1} (α := M) ((fun (x : M) ↦ r • x) m₁) ((fun (x : M) ↦ r • x) m₂)
simp_rw : r • m₁ - r • m₂ = 0
simp_rw₁ : r • m₂ - r • m₂ = 0
⊢ r • (m₁ - m₂) = 0

Tactic:
simp_rw [smul_sub, eq, sub_self]

Premises used: sub_self, smul_sub
-- Module: Mathlib.Algebra.Regular.SMul
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
M' : Type u_7
inst : SMul R M
inst_1 : SMul S M'
e : M ≃ M'
r : R
s : S
h : ∀ (x : M), (e : (a : M) → M') (r • x) = HSMul.hSMul (β := M') s ((e : (a : M) → M') x : M')
⊢ IsSMulRegular M r ↔ IsSMulRegular M' s

Tactic:
(e.comp_injective _).symm.trans <|
    (iff_of_eq <| congrArg _ <| funext h).trans <| e.injective_comp _

Premises used: congrArg, Equiv.injective_comp, funext, IsSMulRegular, Iff.trans, Equiv.comp_injective, Iff.symm, iff_of_eq
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : R
⊢ IsLeftRegular { down := a : ULift.{u, v} R } ↔ IsLeftRegular a

Tactic:
Equiv.ulift.symm.comp_injective _ |>.trans <| Equiv.ulift.symm.injective_comp _ |>.symm

Premises used: Equiv.ulift, Equiv.injective_comp, Iff.trans, Equiv.comp_injective, Equiv.symm, Iff.symm
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : R
⊢ IsRightRegular { down := a : ULift.{u, v} R } ↔ IsRightRegular a

Tactic:
Equiv.ulift.symm.comp_injective _ |>.trans <| Equiv.ulift.symm.injective_comp _ |>.symm

Premises used: Equiv.ulift, Equiv.injective_comp, Iff.trans, Equiv.comp_injective, Equiv.symm, Iff.symm
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : R
⊢ IsRegular { down := a : ULift.{u, v} R } ↔ IsRegular a

Tactic:
simp [isRegular_iff]

Premises used: isRegular_iff
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : ULift.{u, v} R
⊢ IsLeftRegular a.down ↔ IsLeftRegular a

Tactic:
isLeftRegular_up.symm

Premises used: ULift.isLeftRegular_up, Iff.symm
-- Module: Mathlib.Algebra.Regular.ULift
Goal:
R : Type v
inst : Mul R
a : ULift.{u, v} R
⊢ IsRightRegular a.down ↔ IsRightRegular a

Tactic:
isRightRegular_up.symm

Premises used: ULift.isRightRegular_up, Iff.symm