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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : CommSemiring K
inst✝³ : CommSemiring L
inst✝² : Algebra K L
E1 E2 : Subalgebra K L
inst✝¹ : Module.Finite K ↥E1
inst✝ : Module.Finite K ↥E2
⊢ Module.Finite K ↥(E1 ⊔ E2)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
⊢ Subsingleton ((A ⧸ R') ⊗[R] (A ⧸ R'))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
⊢ Algebra.IsEpi R A ↔ Surjective ⇑(algebraMap R A)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a ⊗ₜ[R] b = a • 1 ⊗ₜ[R] b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • 1 ⊗ₜ[R] b = a • b ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a✝ b✝ a b : A
⊢ a • b ⊗ₜ[R] 1 = a • b • 1 ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : Algebra.IsEpi R A
a b : A
⊢ a ⊗ₜ[R] b = b ⊗ₜ[R] a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
f : M →ₗ[R] A ⊗[R] M := { toFun := fun m ↦ 1 ⊗ₜ[R] m, map_add' := ⋯, map_smul' := ⋯ }
⊢ f ∘ₗ lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)) = LinearMap.id

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
⊢ (Algebra.TensorProduct.map f (AlgHom.id R T)).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
this : ∀ (a : A) (m : M), 1 ⊗ₜ[R] (a • m) = a ⊗ₜ[R] m
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x : A
⊢ ∀ (x_1 y : A), x ⊗ₜ[R] ((x_1 + y) • m) = x ⊗ₜ[R] (x_1 • m) + x ⊗ₜ[R] (y • m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
x : A
⊢ ∀ (m_1 : R) (x_1 : A), x ⊗ₜ[R] ((m_1 • x_1) • m) = (RingHom.id R) m_1 • x ⊗ₜ[R] (x_1 • m)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
T' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : CommRing S'
inst✝⁴ : CommRing T'
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R S'
inst✝ : Algebra R T'
f : S →ₐ[R] S'
Hf : f.Finite
g : T →ₐ[R] T'
Hg : g.Finite
⊢ (Algebra.TensorProduct.map f g).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ ∀ (x y : A),
    { toFun := fun y_1 ↦ (x + y) ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ } =
      { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } +
        { toFun := fun y_1 ↦ y ⊗ₜ[R] (y_1 • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionSemiring R
inst✝⁴ : CharZero R
inst✝³ : DivisionSemiring S
inst✝² : CharZero S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
q : ℚ≥0
a : R
⊢ f (q • a) = (RingHom.id ℚ≥0) q • f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionSemiring R
inst✝⁴ : CharZero R
inst✝³ : DivisionSemiring S
inst✝² : CharZero S
inst✝¹ : SMul R S
inst✝ : SMulCommClass R S S
q : ℚ≥0
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
q : ℚ
a : R
⊢ f (q • a) = (RingHom.id ℚ) q • f a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : EquivLike F R S
inst✝ : RingEquivClass F R S
f : F
c : ℚ
x : R
⊢ f (c • x) = (RingHom.id ℚ) c • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Rat

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : DivisionRing R
inst✝⁴ : CharZero R
inst✝³ : DivisionRing S
inst✝² : CharZero S
inst✝¹ : SMul R S
inst✝ : SMulCommClass R S S
q : ℚ
a : R
b : S
⊢ q • a • b = a • q • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
a : A
m : M
⊢ ∀ (m_1 : R) (x : A),
    { toFun := fun y ↦ (m_1 • x) ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ } =
      (RingHom.id R) m_1 • { toFun := fun y ↦ x ⊗ₜ[R] (y • m), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
⊢ Injective ⇑(lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (AlgebraTensorModule.lift (LinearMap.restrictScalarsₗ R A M M A ∘ₗ LinearMap.lsmul A M)) (1 ⊗ₜ[R] m) = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra.IsEpi R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (lid' R A M) ((lid' R A M).symm m) = (lid' R A M) (1 ⊗ₜ[R] m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
⊢ Sort ?u.17

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
semiring✝ : Semiring α := e.semiring
algebra✝ : Algebra R α := Equiv.algebra R e
r : R
⊢ e.ringEquiv.toFun ((algebraMap R α) r) = (algebraMap R β) r

Tactic:
apply e.symm.injective
        simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def]

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
semiring✝ : Semiring α := e.semiring
algebra✝ : Algebra R α := Equiv.algebra R e
r : R
⊢ e.ringEquiv.toFun ((algebraMap R α) r) = (algebraMap R β) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
⊢ let semiring := e.semiring;
  let algebra := Equiv.algebra R e;
  α ≃ₐ[R] β

Tactic:
intros
  exact
    { Equiv.ringEquiv e with
      commutes' := fun r => by
        apply e.symm.injective
        simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def] }

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
⊢ let semiring := e.semiring;
  let algebra := Equiv.algebra R e;
  α ≃ₐ[R] β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
b : β
⊢ Sort ?u.18

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
⊢ Sort ?u.13

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x + y) = e.toFun x + e.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
⊢ let add := e.add;
  let mul := e.mul;
  α ≃+* β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
b : β
⊢ Sort ?u.14

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
⊢ NonUnitalNonAssocSemiring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = s⋆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝ : InvolutiveStar α
s : Set α
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝ : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: β : Type u_2
inst✝ : InvolutiveStar β
x : β
⊢ {x}⋆ = {x⋆}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
s✝ t : Set α
a : α
inst✝¹ : Star α
inst✝ : TrivialStar α
s : Set α
⊢ s⋆ = s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
⊢ star ↑s = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalSemiring β
⊢ NonUnitalSemiring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddMonoidWithOne β
⊢ e (e.invFun ↑0) = e 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ e (e.invFun ↑(n + 1)) = e (e.invFun ↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
⊢ NonAssocSemiring α

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NoncommRing

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n * r = OfNat.ofNat n • r

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NoncommRing

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
r : R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ r * OfNat.ofNat n = OfNat.ofNat n • r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
⊢ Semiring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommSemiring β
⊢ NonUnitalCommSemiring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommSemiring β
⊢ CommSemiring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
⊢ NonUnitalNonAssocRing α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalRing β
⊢ NonUnitalRing α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocRing β
⊢ NonAssocRing α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Ring β
⊢ Ring α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
⊢ NonUnitalCommRing α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
⊢ CommRing α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = 0
⊢ p * q + q * p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = p
⊢ q * p = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hqp : q * p = p
⊢ p * q = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsStarProjection (q - p) ↔ p * q = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsStarProjection (q - p) ↔ q * p = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
⊢ ∀ (a_1 : R), Commute (star a) a_1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ star a * (b * c) = star a * b * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
ha : a ∈ center R
b c : R
⊢ b * c * star a = b * (c * star a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
s : Set R
h : ∀ a ∈ s, star a ∈ s
ha : a ∈ s.centralizer
y : R
hy : y ∈ s
⊢ y * star a = star a * y

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
y : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] y) = l y

Tactic:
by

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
A : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module A N
inst✝⁴ : IsScalarTower R A N
P : Type u_1
inst✝³ : AddCommMonoid P
inst✝² : Module A P
inst✝¹ : Module R P
inst✝ : IsScalarTower R A P
l : M →ₗ[R] N
l' : N →ₗ[A] P
⊢ l' ∘ₗ liftBaseChange A l = liftBaseChange A (↑R l' ∘ₗ l)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x : M
⊢ (liftBaseChange A l) (1 ⊗ₜ[R] x) = l x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
⊢ (liftBaseChange A l).range = Submodule.span A ↑l.range

Tactic:
by

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

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✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
⊢ ↑0 ⊗ₜ[R] 1 = 0

Tactic:
by

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

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✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑(n + 1) ⊗ₜ[R] 1 = ↑n ⊗ₜ[R] 1 + 1

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑n = 1 ⊗ₜ[R] ↑n

Tactic:
by

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

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✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
a b c : A ⊗[R] B
⊢ a * (b + c) = a * b + a * c

Tactic:
by

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

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✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
a b c : A ⊗[R] B
⊢ (a + b) * c = a * c + b * c

Tactic:
by

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

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✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
a : A ⊗[R] B
⊢ 0 * a = 0

Tactic:
by

Goal state after: