[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective (?m.3122 ab ∘ fun x => b * x)
[PROOFSTEP]
rwa [comp_mul_left a b]
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
⊢ IsRightRegular b
[PROOFSTEP]
refine' fun x y xy => ab (_ : x * (b * a) = y * (b * a))
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * (b * a) = y * (b * a)
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRightRegular (b * a)
x y : R
xy : (fun x => x * b) x = (fun x => x * b) y
⊢ x * b * a = y * b * a
[PROOFSTEP]
exact congr_fun (congr_arg (· * ·) xy) a
[GOAL]
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
[PROOFSTEP]
rintro ⟨ab, ba⟩
[GOAL]
case refine'_1.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b
[PROOFSTEP]
exact
  ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
    ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case refine'_2.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
exact
  ⟨⟨(mul_isLeftRegular_iff _ ha.left).mpr hb.left, (mul_isRightRegular_iff _ hb.right).mpr ha.right⟩,
    ⟨(mul_isLeftRegular_iff _ hb.left).mpr ha.left, (mul_isRightRegular_iff _ ha.right).mpr hb.right⟩⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ ¬IsRightRegular 0 ↔ Nontrivial R
[PROOFSTEP]
rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
push_neg
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
⊢ (∀ (x y : R), x = y) ↔ ∀ (x y : R), x = y
[PROOFSTEP]
exact Iff.rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
a b : R
inst✝ : Nontrivial R
la : IsLeftRegular a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne R with ⟨x, y, xy⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ False
[PROOFSTEP]
refine'
  xy
    (la (_ : 0 * x = 0 * y))
      -- Porting note: lean4 seems to need the type signature
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ 0 * x = 0 * y
[PROOFSTEP]
rw [zero_mul, zero_mul]
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
a b : R
inst✝ : Nontrivial R
ra : IsRightRegular a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne R with ⟨x, y, xy⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ False
[PROOFSTEP]
refine' xy (ra (_ : x * 0 = y * 0))
[GOAL]
case intro.intro
R : Type u_1
inst✝¹ : MulZeroClass R
b : R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ x * 0 = y * 0
[PROOFSTEP]
rw [mul_zero, mul_zero]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = 0 ↔ a = 0
[PROOFSTEP]
nth_rw 1 [← mul_zero b]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0
[PROOFSTEP]
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, mul_zero]⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0
[PROOFSTEP]
rw [ha, mul_zero]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 ↔ a = 0
[PROOFSTEP]
nth_rw 1 [← zero_mul b]
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0
[PROOFSTEP]
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha, zero_mul]⟩
[GOAL]
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b
[PROOFSTEP]
rw [ha, zero_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b
[PROOFSTEP]
refine' Iff.trans _ isRegular_mul_and_mul_iff
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)
[PROOFSTEP]
refine' ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩
[GOAL]
R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (b * a)
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (?m.12942 h * a)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
[PROOFSTEP]
exact isRegular_one.left
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular (a * ?m.13480 h)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
h : a * b = 1
⊢ IsRightRegular 1
[PROOFSTEP]
exact isRegular_one.right
[GOAL]
R : Type u_1
inst✝ : Monoid R
a b : R
ua : IsUnit a
⊢ IsRegular a
[PROOFSTEP]
rcases ua with ⟨a, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Monoid R
b : R
a : Rˣ
⊢ IsRegular ↑a
[PROOFSTEP]
exact Units.isRegular a
