mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
single_apply_of_col_ne _ _ hj,

Goal state after:
case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ 0 k' l' = single (i, k) (j, l) r (i, k') (j', l')
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
hj : l ≠ l'
⊢ single k l r k l' = single (i, k) (j, l) r (i, k) (j, l')

Tactic:
single_apply_of_col_ne _ _ hj,

Goal state after:
case inr.inr.inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
l' : L
hj : l ≠ l'
⊢ 0 = single (i, k) (j, l) r (i, k) (j, l')
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ star x * star z = star y * star x ↔ x * y = z * x

Tactic:
← star_mul,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ star (z * x) = star (x * y) ↔ x * y = z * x
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star ⅟r * star r = 1

Tactic:
← star_mul,

Goal state after:
R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star (r * ⅟r) = 1
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star r * star ⅟r = 1

Tactic:
← star_mul,

Goal state after:
R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star (⅟r * r) = 1
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)

Tactic:
by
  simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Star R
inst✝² : Star A
inst✝¹ : SMul R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)

Tactic:
by
  simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')

Tactic:
by
  ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case succ
m : Type u_2
n✝ : Type u_3
α : Type u_12
inst✝⁴ : Semiring α
inst✝³ : Fintype n✝
inst✝² : Fintype m
inst✝¹ : DecidableEq n✝
inst✝ : DecidableEq m
A : Matrix n✝ n✝ α
D : Matrix m m α
n : ℕ
ih : fromBlocks A 0 0 D ^ n = fromBlocks (A ^ n) 0 0 (D ^ n)
⊢ fromBlocks A 0 0 D ^ (n + 1) = fromBlocks (A ^ (n + 1)) 0 0 (D ^ (n + 1))

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ f (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0

Tactic:
apply_ite f,

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : o → Matrix m n α
f : α → β
hf : f 0 = 0
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else f 0) = if i✝.2 = j✝.2 then f (M i✝.2 i✝.1 j✝.1) else 0
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col i j = vecCons (fun j ↦ A i✝ (col j)) (A.submatrix row col) i j

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [submatrix]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ {d} ⊆ ↑(ψ'.submoduleImage N)

Tactic:
singleton_subset_iff,

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ d ∈ ↑(ψ'.submoduleImage N)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝² : CommSemiring R
n✝ : Type u_5
inst✝¹ : DecidableEq n✝
inst✝ : Fintype n✝
M : Matrix n✝ n✝ R
n : ℕ
ih : toLin' (M ^ n) = toLin' M ^ n
⊢ toLin' (M ^ (n + 1)) = toLin' M ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ (toLin v₁ v₂) ((toMatrix v₁ v₂) f) = f

Tactic:
rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : NoZeroDivisors M
n : N
hn : n ≠ 0
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
hs : ms.1 ≠ 0
⊢ n ∈ nonZeroDivisors N

Tactic:
exact And.left <| mul_mem_nonZeroDivisors.mp
    (eq ▸ f.map_nonZeroDivisors_le ⟨_, mem_nonZeroDivisors_of_ne_zero hs, rfl⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case succ
R : Type u_1
inst✝⁴ : CommSemiring R
n✝ : Type u_4
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n✝ R M₁
A : Matrix n✝ n✝ R
n : ℕ
ih : (toLin v₁ v₁) (A ^ n) = (toLin v₁ v₁) A ^ n
⊢ (toLin v₁ v₁) (A ^ (n + 1)) = (toLin v₁ v₁) A ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) m

Tactic:
by
  nth_rw 2 [← one_mul m]
  rw [mk'_mul, mk'_one, Algebra.smul_def]

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

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ (algebraMap R P) x = (algebraMap R P) y → ∃ c, ↑c * x = ↑c * y

Tactic:
← h.symm.toEquiv.injective.eq_iff,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
⊢ mk' K x y = 1 ↔ x = ↑y

Tactic:
refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩

Goal state after:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
⊢ mk' K x y = 1 → x = ↑y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsFractionRing B L
C : Type u_12
M : Type u_13
inst✝³ : CommRing C
inst✝² : CommRing M
inst✝¹ : Algebra C M
inst✝ : IsFractionRing C M
f : A ≃+* B
g : B ≃+* C
a : K
⊢ (ringEquivOfRingEquiv (f.trans g)) a = ((ringEquivOfRingEquiv f).trans (ringEquivOfRingEquiv g)) a

Tactic:
simp [IsLocalization.map_map]

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R✝ : Type u_1
inst✝²⁸ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝²⁷ : CommRing S✝
inst✝²⁶ : Algebra R✝ S✝
P : Type u_3
inst✝²⁵ : CommRing P
A✝ : Type u_4
inst✝²⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝²³ : CommRing B✝
inst✝²² : IsDomain B✝
inst✝²¹ : Field K✝
L✝ : Type u_7
inst✝²⁰ : Field L✝
inst✝¹⁹ : Algebra A✝ K✝
inst✝¹⁸ : IsFractionRing A✝ K✝
g✝ : A✝ →+* L✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • b • x = (g • b) • g • x

Tactic:
Algebra.smul_def',

Goal state after:
R✝ : Type u_1
inst✝²⁸ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝²⁷ : CommRing S✝
inst✝²⁶ : Algebra R✝ S✝
P : Type u_3
inst✝²⁵ : CommRing P
A✝ : Type u_4
inst✝²⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝²³ : CommRing B✝
inst✝²² : IsDomain B✝
inst✝²¹ : Field K✝
L✝ : Type u_7
inst✝²⁰ : Field L✝
inst✝¹⁹ : Algebra A✝ K✝
inst✝¹⁸ : IsFractionRing A✝ K✝
g✝ : A✝ →+* L✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • ((algebraMap B L) b * x) = (g • b) • g • x
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R✝ : Type u_1
inst✝²⁸ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝²⁷ : CommRing S✝
inst✝²⁶ : Algebra R✝ S✝
P : Type u_3
inst✝²⁵ : CommRing P
A✝ : Type u_4
inst✝²⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝²³ : CommRing B✝
inst✝²² : IsDomain B✝
inst✝²¹ : Field K✝
L✝ : Type u_7
inst✝²⁰ : Field L✝
inst✝¹⁹ : Algebra A✝ K✝
inst✝¹⁸ : IsFractionRing A✝ K✝
g✝ : A✝ →+* L✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • ((algebraMap B L) b * x) = (g • b) • g • x

Tactic:
Algebra.smul_def',

Goal state after:
R✝ : Type u_1
inst✝²⁸ : CommRing R✝
M : Submonoid R✝
S✝ : Type u_2
inst✝²⁷ : CommRing S✝
inst✝²⁶ : Algebra R✝ S✝
P : Type u_3
inst✝²⁵ : CommRing P
A✝ : Type u_4
inst✝²⁴ : CommRing A✝
K✝ : Type u_5
B✝ : Type u_6
inst✝²³ : CommRing B✝
inst✝²² : IsDomain B✝
inst✝²¹ : Field K✝
L✝ : Type u_7
inst✝²⁰ : Field L✝
inst✝¹⁹ : Algebra A✝ K✝
inst✝¹⁸ : IsFractionRing A✝ K✝
g✝ : A✝ →+* L✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • ((algebraMap B L) b * x) = (algebraMap B L) (g • b) * g • x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)

Tactic:
Finset.coe_image,

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A (⇑((TensorProduct.mk R A M) 1) '' ↑s)
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
⊢ p * q = p ∧ star q * star p = p ↔ p * q = p

Tactic:
← star_mul,

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ star (p * q) = p ↔ p * q = p
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_2.refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ ∀ (x : A) (y : B), a₁ ⊗ₜ[R] b₁ * x ⊗ₜ[R] y = x ⊗ₜ[R] y * a₁ ⊗ₜ[R] b₁

Tactic:
intro a₂

Goal state after:
case refine_2.refine_2
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
a₂ : A
⊢ ∀ (y : B), a₁ ⊗ₜ[R] b₁ * a₂ ⊗ₜ[R] y = a₂ ⊗ₜ[R] y * a₁ ⊗ₜ[R] b₁
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_2.refine_3
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
⊢ ∀ (x y : A ⊗[R] B),
    a₁ ⊗ₜ[R] b₁ * x = x * a₁ ⊗ₜ[R] b₁ →
      a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁ → a₁ ⊗ₜ[R] b₁ * (x + y) = (x + y) * a₁ ⊗ₜ[R] b₁

Tactic:
intro a₂

Goal state after:
case refine_2.refine_3
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 A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y : A ⊗[R] B
a₁ : A
b₁ : B
a₂ : A ⊗[R] B
⊢ ∀ (y : A ⊗[R] B),
    a₁ ⊗ₜ[R] b₁ * a₂ = a₂ * a₁ ⊗ₜ[R] b₁ →
      a₁ ⊗ₜ[R] b₁ * y = y * a₁ ⊗ₜ[R] b₁ → a₁ ⊗ₜ[R] b₁ * (a₂ + y) = (a₂ + y) * a₁ ⊗ₜ[R] b₁
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0

Tactic:
by
  simpa [-Units.mul_inv] using congr($(u.mul_inv).val)

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

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

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this

Goal state after:
case h.right
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1 = 0
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

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

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this

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

Goal state before:
pp: case e'_3
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} = quasispectrum R (b * a) ∩ {r | IsUnit r}

pp: case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
· simpa [Set.inter_comm _ {r | IsUnit r}, Unitization.quasispectrum_eq_spectrum_inr,
      Unitization.inr_mul] using spectrum.setOfPred_isUnit_inter_mul_comm _ _

Goal state after:
case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
x✝² x✝¹ x✝ : Unitization R A
⊢ ((x✝² + x✝¹) * x✝).toProd.2 = (x✝² * x✝ + x✝¹ * x✝).toProd.2

Tactic:
simp [smul_add, add_smul, add_mul]
      abel

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: case mem
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r✝ : R
a : A
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
r : R
hr : r ∈ range fun s ↦ star s * s
⊢ r • a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)

Tactic:
induction ha using AddSubmonoid.closure_induction with
  | zero => simp
  | add a₁ a₂ _ _ ha₁ ha₂ => simpa [smul_add] using add_mem ha₁ ha₂
  | mem a ha =>
  obtain ⟨r, rfl⟩ := hr
  obtain ⟨a, rfl⟩ := ha
  exact AddSubmonoid.subset_closure ⟨r • a, by simp [star_smul, smul_mul_smul_comm]⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
rcases dir i j with ⟨k, hik, hjk⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T ≤ iSup K
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : K i ≤ K k
hjk : K j ≤ K k
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x ≤ y
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint y

Tactic:
rw [StarOrderedRing.le_iff] at h
  obtain ⟨d, hd, rfl⟩ := h
  rw [IsSelfAdjoint, star_add, hx.star_eq]
  congr
  refine AddMonoidHom.eqOn_closureM (f := starAddEquiv (R := R)) (g := .id R) ?_ hd
  rintro - ⟨s, rfl⟩
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * (star u * star v)
⊢ 0 ≤ x

Tactic:
← star_mul,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
u x : R
hu : IsUnit u
h : 0 ≤ u * x * star u
v : R
hv : v * u = 1
this : 0 ≤ x * star (v * u)
⊢ 0 ≤ x
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
⊢ lift.{v, w} #{ i // V i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
by
  set I := { i : ι // V i ≠ ⊥ }
  have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
    intro i
    rw [← Submodule.ne_bot_iff]
    exact i.prop
  choose v hvV hv using hI
  have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
  exact this.cardinal_lift_le_rank

Goal state after: