mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

Tactic:
intros

Goal state after:
case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
x✝ y✝ : α
⊢ e (x✝ - y✝) = e x✝ - e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
n✝ : ℤ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0

Tactic:
intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 0 = 0
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
intros

Goal state after:
case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ e 1 = 1
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

Tactic:
intros

Goal state after:
case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α), e (-x) = -e x

Tactic:
intros

Goal state after:
case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
⊢ e (-x✝) = -e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

Tactic:
intros

Goal state after:
case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ - y✝) = e x✝ - e y✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x

Tactic:
intros

Goal state after:
case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℤ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
case npow
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℕ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := ⋯
add_group_with_one : AddGroupWithOne α := ⋯
npow : Pow α ℕ := ⋯
⊢ ∀ (n : ℤ), e ↑n = ↑n

Tactic:
intros

Goal state after:
case intCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
mul : Mul α := e.mul
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
n✝ : ℤ
⊢ e ↑n✝ = ↑n✝
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:
simpa using congr_arg star (ha _ (h _ hy)).symm

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✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (r • 1)

Tactic:
smul_tmul

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
r : R
⊢ 1 ⊗ₜ[R] (r • 1) = 1 ⊗ₜ[R] (r • 1)
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 : 𝕜
⊢ σ (↑ₐ k) = {k}

Tactic:
by
  rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]

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

Goal state before:
pp: 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

Tactic:
simpa [ha, zero_smul_set] using (show {(0 : 𝕜)} = (0 : Set 𝕜) from rfl)

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_mem : k ∈ σ (x✝ * y✝)
k_ne : k ∉ {0}
⊢ k ∈ σ (y✝ * x✝) \ {0}

Tactic:
change ((Units.mk0 k k_ne) : 𝕜) ∈ _ at k_mem

Goal state after:
𝕜 : Type u
A : Type v
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
a b x✝ y✝ : A
k : 𝕜
k_ne : k ∉ {0}
k_mem : ↑(Units.mk0 k k_ne) ∈ σ (x✝ * y✝)
⊢ k ∈ σ (y✝ * x✝) \ {0}
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (x • 1) ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range

Tactic:
smul_tmul

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈ ↑((mk R S M) 1).range
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)
⊢ (q.num • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q.num • n)

Tactic:
smul_tmul

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 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)
⊢ m ⊗ₜ[R] (q.num • n) = m ⊗ₜ[R] (q.num • n)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case a
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
⊢ (map f g).range ≤ (includeLeft.comp f).range ⊔ (includeRight.comp g).range

Tactic:
rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]

Goal state after:
case a
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
⊢ ⇑(map f g) '' {t | ∃ a b, a ⊗ₜ[R] b = t} ⊆ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)
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
h : Function.Bijective ⇑(algebraMap R B)
⊢ Function.Bijective ⇑includeLeft

Tactic:
have : (includeLeft : A →ₐ[S] A ⊗[R] B).comp (TensorProduct.rid R S A).toAlgHom =
      map (.id S A) (Algebra.ofId R B) := by ext; simp

Goal state after:
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
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑includeLeft
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
r : R
⊢ (r • 1) ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (r • 1)

Tactic:
smul_tmul

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
r : R
⊢ 1 ⊗ₜ[R] (r • 1) = 1 ⊗ₜ[R] (r • 1)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
⊢ ∃ g, g ∘ₗ p.subtype = f ∧ g v = y

Tactic:
rcases (LinearPMap.supSpanSingleton ⟨p, f⟩ v y hv).toFun.exists_extend with ⟨g, hg⟩
  refine ⟨g, ?_, ?_⟩
  · ext x
    have := LinearPMap.supSpanSingleton_apply_mk_of_mem ⟨p, f⟩ y hv x.2
    simpa using! congr($hg _).trans this
  · have := LinearPMap.supSpanSingleton_apply_self ⟨p, f⟩ y hv
    simpa using! congr($hg _).trans this

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalSemiring A
inst✝³ : StarRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ↑(centralizer R Set.univ) = ↑(center R A)

Tactic:
by rw [coe_centralizer, Set.univ_union, coe_center, Set.centralizer_univ]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ Fintype.card ↑(this.extend ⋯) ≤ Fintype.card ↑(Basis.ofVectorSpaceIndex K ↥S)

Tactic:
← finrank_eq_card_basis bS,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
S : Submodule K V
h : finrank K ↥S = finrank K V
bS : Basis (↑(Basis.ofVectorSpaceIndex K ↥S)) K ↥S := Basis.ofVectorSpace K ↥S
bS_eq : bS = Basis.ofVectorSpace K ↥S
this : LinearIndepOn K id (Subtype.val '' Basis.ofVectorSpaceIndex K ↥S)
b : Basis (↑(this.extend ⋯)) K V := Basis.extend this
b_eq : b = Basis.extend this
i2 : Fintype ↑(Subtype.val '' Basis.ofVectorSpaceIndex K ↥S) := ⋯.fintype
⊢ Fintype.card ↑(this.extend ⋯) ≤ finrank K ↥S
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
ι : Type u_1
f : ι → V →ₗ[K] V
s : Finset ι
comm : (↑s).Pairwise (Commute on f)
h : s.SupIndep fun i ↦ (f i).ker
⊢ (s.noncommProd f comm).ker = ⨆ i ∈ s, (f i).ker

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp [Module.End.one_eq_id]
  | insert i s hi ih =>
    replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
        ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Module.End.mul_eq_comp,
      ker_comp_eq_of_commute_of_disjoint_ker]
    · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
    · exact s.noncommProd_commute _ _ _ fun j hj ↦
        comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by lia)
    · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
      simpa [ih, hi, Finset.sup_eq_iSup] using h

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 1 * a = a

Tactic:
rintro ⟨⟩
    exact Quot.sound Rel.one_mul

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : K ∙ x = ⊤
⊢ ∃ c, c • x = y

Tactic:
have : y ∈ Submodule.span K {x} := by rw [this]; exact mem_top

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this✝ : K ∙ x = ⊤
this : y ∈ K ∙ x
⊢ ∃ c, c • x = y
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case zero_mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (0 * a✝) = liftFun R X f 0

Tactic:
change algebraMap _ _ _ * _ = algebraMap _ _ _

Goal state after:
case zero_mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ (algebraMap R A) 0 * liftFun R X f a✝ = (algebraMap R A) 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ (f + g).domain⦄ ⦃hg : x ∈ domain 0⦄, ↑(f + g) ⟨x, hf⟩ = ↑0 ⟨x, hg⟩
⊢ ↑f ⟨x, hf⟩ + ↑g ⟨x, hg⟩ = 0

Tactic:
simp only [hdom, zero_domain, mem_top, zero_apply, forall_true_left] at h'

Goal state after:
case h'
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
x : E
hf : x ∈ (-f).domain
hg : x ∈ g.domain
hdom : (f + g).domain = ⊤
h' : ∀ ⦃x : E⦄, ↑(f + g) ⟨x, ⋯⟩ = 0
⊢ ↑f ⟨x, hf⟩ + ↑g ⟨x, hg⟩ = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
h : Commute a x
⊢ eval x (p * C a) = eval x p * a

Tactic:
by
  rw [eval, eval₂_mul_C'] <;> simp [h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (a : R), ((C a).comp ψ).comp χ = (C a).comp (ψ.comp χ)

Tactic:
intros

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
a✝ : R
⊢ ((C a✝).comp ψ).comp χ = (C a✝).comp (ψ.comp χ)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)

Tactic:
intros

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ p✝ q✝ : R[X]
a✝¹ : (p✝.comp ψ).comp χ = p✝.comp (ψ.comp χ)
a✝ : (q✝.comp ψ).comp χ = q✝.comp (ψ.comp χ)
⊢ ((p✝ + q✝).comp ψ).comp χ = (p✝ + q✝).comp (ψ.comp χ)