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

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f) =
    (LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)

Tactic:
ext

Goal state after:
R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
x✝¹ x✝ : A
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry ((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f))) 1) x✝¹))
        1)
      x✝ =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                ((LinearMap.mul S B).compl₁₂ (LinearMap.liftBaseChange S ↑f) (LinearMap.liftBaseChange S ↑f)))
              1)
            x✝¹))
        1)
      x✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
      ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f) =
    f

Tactic:
ext

Goal state after:
R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x✝ : A
⊢ ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight)
        ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯) f))
      x✝ =
    f x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
⊢ (LinearMap.mul S (A ⊗[R] B)).compr₂ f = (LinearMap.mul S C ∘ₗ f).compl₂ f

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
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
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
this✝ : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := IsScalarTower.restrictScalars R S C
x✝³ : A
x✝² : B
x✝¹ : A
x✝ : B
⊢ ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ((LinearMap.mul S (A ⊗[R] B)).compr₂ f)) x✝³) x✝²)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f)) x✝³) x✝²)) x✝¹) x✝
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
⊢ (restrictScalars R
          ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯)
            ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight) f))).comp
      Algebra.TensorProduct.includeRight =
    (restrictScalars R f).comp Algebra.TensorProduct.includeRight

Tactic:
ext

Goal state after:
R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
x✝ : A
⊢ ((restrictScalars R
            ((fun f ↦ ofLinearMap (LinearMap.liftBaseChange S ↑f) ⋯ ⋯)
              ((fun f ↦ (restrictScalars R f).comp Algebra.TensorProduct.includeRight) f))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((restrictScalars R f).comp Algebra.TensorProduct.includeRight) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)
h_one : f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1
⊢ (LinearMap.mul R (A ⊗[R] B ⊗[R] C)).compr₂ ↑f = (LinearMap.mul R D ∘ₗ ↑f).compl₂ ↑f

Tactic:
ext

Goal state after:
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
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂)
h_one : f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1
x✝⁵ : A
x✝⁴ : B
x✝³ : C
x✝² : A
x✝¹ : B
x✝ : C
⊢ (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry (AlgebraTensorModule.curry ((LinearMap.mul R (A ⊗[R] B ⊗[R] C)).compr₂ ↑f)))
                    x✝⁵)
                  x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((((AlgebraTensorModule.curry (AlgebraTensorModule.curry ((LinearMap.mul R D ∘ₗ ↑f).compl₂ ↑f))) x✝⁵) x✝⁴)
                x✝³)))
          x✝²)
        x✝¹)
      x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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
⊢ lift includeLeft includeRight ⋯ = AlgHom.id S (A ⊗[R] B)

Tactic:
ext

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.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x → ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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) }
⊢ (fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩)
      ((fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯) fg) =
    fg

Tactic:
ext

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: 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
⊢ (fun fg ↦ lift (↑fg).1 (↑fg).2 ⋯)
      ((fun f' ↦ ⟨(f'.comp includeLeft, (AlgHom.restrictScalars R f').comp includeRight), ⋯⟩) f') =
    f'

Tactic:
ext

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.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝ : B →ₐ[R] C
⊢ (fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) ((fun f ↦ lift (ofId S C) f ⋯) x✝) = x✝

Tactic:
ext

Goal state after:
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✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : B →ₐ[R] C
x✝ : B
⊢ ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) ((fun f ↦ lift (ofId S C) f ⋯) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝ : S ⊗[R] B →ₐ[S] C
⊢ (fun f ↦ lift (ofId S C) f ⋯) ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) x✝) = x✝

Tactic:
ext

Goal state after:
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✝
C : Type u_3
inst✝³ : CommRing C
inst✝² : Algebra R C
inst✝¹ : Algebra S C
inst✝ : IsScalarTower R S C
x✝¹ : S ⊗[R] B →ₐ[S] C
x✝ : B
⊢ ((AlgHom.restrictScalars R
            ((fun f ↦ lift (ofId S C) f ⋯) ((fun f ↦ (AlgHom.restrictScalars R f).comp includeRight) x✝¹))).comp
        includeRight)
      x✝ =
    ((AlgHom.restrictScalars R x✝¹).comp includeRight) x✝
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case h
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0 ∧ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0

Tactic:
constructor

Goal state after:
case h.left
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0

case h.right
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap =
    LinearMap.lTensor S (Algebra.linearMap R B)

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : S
⊢ ((AlgebraTensorModule.curry (↑R (Algebra.linearMap S (S ⊗[R] B)) ∘ₗ (TensorProduct.rid R R S).toLinearMap)) x✝) 1 =
    ((AlgebraTensorModule.curry (LinearMap.lTensor S (Algebra.linearMap R B))) x✝) 1
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
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
⊢ (↑(TensorProduct.rid R S A)).comp includeLeftRingHom = RingHom.id A

Tactic:
ext

Goal state after:
R : Type uR
S : Type uS
A : Type uA
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
x✝ : A
⊢ ((↑(TensorProduct.rid R S A)).comp includeLeftRingHom) x✝ = (RingHom.id A) x✝
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: 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 R✝¹ C
inst✝³³ : Algebra S✝ C
inst✝³² : IsScalarTower R✝¹ S✝ C
inst✝³¹ : Semiring D
inst✝³⁰ : Algebra R✝¹ D
inst✝²⁹ : Semiring E
inst✝²⁸ : Algebra R✝¹ E
inst✝²⁷ : Algebra S✝ E
inst✝²⁶ : IsScalarTower R✝¹ S✝ E
inst✝²⁵ : Semiring F
inst✝²⁴ : Algebra R✝¹ F
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this✝ : IsAddTorsionFree (M ⊗[R] N)
this : q.den • (q • m) ⊗ₜ[R] n = q.den • m ⊗ₜ[R] (q • n)
⊢ (fun x ↦ q.den • x) ((q • m) ⊗ₜ[R] n) = (fun x ↦ q.den • x) (m ⊗ₜ[R] (q • n))

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a

Tactic:
by
  refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩
  · simpa only [quasispectrum.preimage_algebraMap] using
      (quasispectrum S a).image_preimage_subset (algebraMap R S)
  exact ⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Tactic:
ext

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝ : B ⊗[R] A
⊢ (TensorProduct.comm R A B).symm a✝ = (TensorProduct.comm R B A) a✝