mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul 0) (1 ⊗ₜ[R] 1) = 0

pp: case refine_2
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B), (mul (x ⊗ₜ[R] y)) (1 ⊗ₜ[R] 1) = x ⊗ₜ[R] y

pp: case refine_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B), (mul x) (1 ⊗ₜ[R] 1) = x → (mul y) (1 ⊗ₜ[R] 1) = y → (mul (x + y)) (1 ⊗ₜ[R] 1) = x + y

Tactic:
<;>

Goal state after:
case refine_1
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ (mul 0) (1 ⊗ₜ[R] 1) = 0

case refine_2
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x : A) (y : B), (mul (x ⊗ₜ[R] y)) (1 ⊗ₜ[R] 1) = x ⊗ₜ[R] y

case refine_3
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x : A ⊗[R] B
⊢ ∀ (x y : A ⊗[R] B), (mul x) (1 ⊗ₜ[R] 1) = x → (mul y) (1 ⊗ₜ[R] 1) = y → (mul (x + y)) (1 ⊗ₜ[R] 1) = x + y
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ ¬¬IsUnit a ↔ IsUnit a

Tactic:
Classical.not_not

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ IsUnit a ↔ IsUnit a
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (1 - r • ↑a⁻¹)

Tactic:
IsUnit.sub_iff

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r • ↑a⁻¹ - 1)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case refine_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)

pp: case refine_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a

Tactic:
<;>

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : star r ∈ resolventSet R a
⊢ r ∈ resolventSet R (star a)

case refine_2
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
h : r ∈ resolventSet R (star a)
⊢ star r ∈ resolventSet R a
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
⊢ σ (k • a) = k • σ a

Tactic:
rcases eq_or_ne k 0 with (rfl | h)

Goal state after:
case inl
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
a : A
ha : (σ a).Nonempty
⊢ σ (0 • a) = 0 • σ a

case inr
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
a : A
ha : (σ a).Nonempty
h : k ≠ 0
⊢ σ (k • a) = k • σ a
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (0 * y) • m = 0 • y • m

pp: case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = x ⊗ₜ[R] y_1 • y • m

pp: case refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ (0 * y) • m = 0 • y • m

case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = x ⊗ₜ[R] y_1 • y • m

case refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y_1 : A ⊗[R] B), (x * y) • m = x • y • m → (y_1 * y) • m = y_1 • y • m → ((x + y_1) * y) • m = (x + y_1) • y • m
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A
⊢ ((lift includeLeft includeRight ⋯).comp includeLeft) x✝ = ((AlgHom.id S (A ⊗[R] B)).comp includeLeft) x✝

pp: case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R (lift includeLeft includeRight ⋯)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (A ⊗[R] B))).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A
⊢ ((lift includeLeft includeRight ⋯).comp includeLeft) x✝ = ((AlgHom.id S (A ⊗[R] B)).comp includeLeft) x✝

case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : B
⊢ ((AlgHom.restrictScalars R (lift includeLeft includeRight ⋯)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (AlgHom.id S (A ⊗[R] B))).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case fst
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : A
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).1
      x✝ =
    (↑fg).1 x✝

pp: case snd
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : B
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).2
      x✝ =
    (↑fg).2 x✝

Tactic:
<;>

Goal state after:
case fst
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : A
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).1
      x✝ =
    (↑fg).1 x✝

case snd
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
fg : { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) }
x✝ : B
⊢ (↑((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg))).2
      x✝ =
    (↑fg).2 x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x✝ : A
⊢ (((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
            ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f')).comp
        includeLeft)
      x✝ =
    (f'.comp includeLeft) x✝

pp: case hb
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
              ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f'))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R f').comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x✝ : A
⊢ (((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
            ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f')).comp
        includeLeft)
      x✝ =
    (f'.comp includeLeft) x✝

case hb
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra S C
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f' : A ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
              ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f'))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R f').comp includeRight) x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x ↔ IsUnit (1 + ↑x)

Tactic:
refine ⟨?_, fun hx ↦ ?_⟩
  · rintro ⟨u, rfl⟩
    exact (Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit
  · exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ y + a + a * y = 0

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ a + y + y * a = 0

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ y + a + a * y = 0

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ a + y + y * a = 0
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
x✝ : A
⊢ (((↑(TensorProduct.comm R C D)).comp (map f g)).comp includeLeft) x✝ =
    (((map g f).comp ↑(TensorProduct.comm R A B)).comp includeLeft) x✝

pp: case hb
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
x✝ : B
⊢ ((AlgHom.restrictScalars R ((↑(TensorProduct.comm R C D)).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((map g f).comp ↑(TensorProduct.comm R A B))).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
x✝ : A
⊢ (((↑(TensorProduct.comm R C D)).comp (map f g)).comp includeLeft) x✝ =
    (((map g f).comp ↑(TensorProduct.comm R A B)).comp includeLeft) x✝

case hb
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
x✝ : B
⊢ ((AlgHom.restrictScalars R ((↑(TensorProduct.comm R C D)).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((map g f).comp ↑(TensorProduct.comm R A B))).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : A
⊢ (((lmul' R).comp (map f g)).comp includeLeft) x✝ = ((lift f g ⋯).comp includeLeft) x✝

pp: case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : B
⊢ ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (lift f g ⋯)).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : A
⊢ (((lmul' R).comp (map f g)).comp includeLeft) x✝ = ((lift f g ⋯).comp includeLeft) x✝

case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : B
⊢ ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R (lift f g ⋯)).comp includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : A
⊢ ((productMap f g).comp includeLeft) x✝ = (((lmul' R).comp (map f g)).comp includeLeft) x✝

pp: case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : B
⊢ ((AlgHom.restrictScalars R (productMap f g)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝

Tactic:
<;>

Goal state after:
case ha
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : A
⊢ ((productMap f g).comp includeLeft) x✝ = (((lmul' R).comp (map f g)).comp includeLeft) x✝

case hb
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
x✝ : B
⊢ ((AlgHom.restrictScalars R (productMap f g)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((lmul' R).comp (map f g))).comp includeRight) x✝
Module: Mathlib.Algebra.Algebra.StrictPositivity

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a

Tactic:
by
  simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]
  lift u to Aˣ using hu
  rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case ha
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((lmul' (ULift.{u₁, u_4} R)).comp includeLeft) x✝).down =
    ((((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm).comp
          includeLeft)
        x✝).down

pp: case hb
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((AlgHom.restrictScalars (ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R))).comp includeRight) x✝).down =
    (((AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              ((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp
                ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm)).comp
          includeRight)
        x✝).down

Tactic:
<;>

Goal state after:
case ha
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((lmul' (ULift.{u₁, u_4} R)).comp includeLeft) x✝).down =
    ((((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm).comp
          includeLeft)
        x✝).down

case hb
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : ULift.{u₂, u_5} S
⊢ (((AlgHom.restrictScalars (ULift.{u₁, u_4} R) (lmul' (ULift.{u₁, u_4} R))).comp includeRight) x✝).down =
    (((AlgHom.restrictScalars (ULift.{u₁, u_4} R)
              ((AlgHom.ulift.{u_8, u₁, u₂, u_4, u_5, u_5} (lmul' R)).comp
                ↑(uliftEquiv R (ULift.{u₁, u_4} R) S S).symm)).comp
          includeRight)
        x✝).down