R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
have h₁ : ∀ x y : A, IsUnit (1 - x * y) → IsUnit (1 - y * x) := by
  refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
  calc
    (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
        1 - y * x + y * ((1 - x * y) * h.unit.inv) * x :=
      by noncomm_ring
    _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
  calc
    (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
        1 - y * x + y * (h.unit.inv * (1 - x * y)) * x :=
      by noncomm_ring
    _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
have := Iff.intro (h₁ (r⁻¹ • a) b) (h₁ b (r⁻¹ • a))
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
rw [mul_smul_comm r⁻¹ b a] at this
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
simpa only [mem_iff, not_iff_not, Algebra.algebraMap_eq_smul_one, ← Units.smul_def,
  IsUnit.smul_sub_iff_sub_inv_smul, smul_mul_assoc]
case refine'_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1

case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
refine' fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, _, _⟩, rfl⟩
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
case refine'_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1

case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
calc
  (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
      1 - y * x + y * ((1 - x * y) * h.unit.inv) * x :=
    by noncomm_ring
  _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
no goals
case refine'_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1
calc
  (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
      1 - y * x + y * (h.unit.inv * (1 - x * y)) * x :=
    by noncomm_ring
  _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) = 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x
noncomm_ring
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * (IsUnit.unit h).inv) * x = 1
simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) = 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x
noncomm_ring
no goals
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((IsUnit.unit h).inv * (1 - x * y)) * x = 1
simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]