case refine'_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

case refine'_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b
refine' ⟨_, _⟩
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
case refine'_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b
rintro ⟨ab, ba⟩
no goals
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
exact
  ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
    ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩
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)
case refine'_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)
rintro ⟨ha, hb⟩
no goals
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)
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⟩⟩