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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0

Tactic:
· simp only [dif_pos]
    split_ifs <;> simp

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case succ
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
h : LinearEquiv.baseChange R A M M (f ^ ↑n) = LinearEquiv.baseChange R A M M f ^ ↑n
⊢ LinearEquiv.baseChange R A M M (f ^ (↑n + 1)) = LinearEquiv.baseChange R A M M f ^ (↑n + 1)

Tactic:
simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)

Tactic:
OreLocalization.expand' r₁ s₁ sa

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ (r₃ /ₒ s₃) • ((sa • r₁ + ra • r₂) /ₒ (sa * s₁)) = (r₃ /ₒ s₃) • (sa • r₁ /ₒ (sa * s₁)) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i : Fin (n' + 1)
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i) =
    Fin.cons a as i • ↑((Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ⋯) (Fin.castLE ⋯ i))

Tactic:
Basis.coe_mkFinConsOfLE

Goal state after:
case neg.intro.refine_2.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i : Fin (n' + 1)
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i) =
    Fin.cons a as i • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i))
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * r₂ = ↑u * r₁
h₂ : ↑u = v
⊢ r₁ = r₂

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : ↑u * r₂ - ↑u * r₁ = 0
h₂ : ↑u = v
⊢ r₁ = r₂
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
classical rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]

Goal state after:
ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (Matrix ι ι A)
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
m : ↥M
⊢ Bijective fun s ↦ m • s

Tactic:
simpa only [Submonoid.smul_def, Algebra.smul_def] using! (map_units S m).smul_bijective

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

Goal state before:
pp: case e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r

Tactic:
RingHom.algebraMap_toAlgebra

Goal state after:
case e'_6
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
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r
Module: Mathlib.RingTheory.Localization.Defs

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
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) x) = f ((algebraMap R S) y)
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
x y : R
hz : f ((algebraMap R S) x) - f ((algebraMap R S) y) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y
Module: Mathlib.RingTheory.Localization.Basic

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 : R
y : ↥M
⊢ (algEquiv M S).symm (mk' S x y) = mk x y

Tactic:
rw [mk_eq_mk', algEquiv_symm_mk']

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

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
Rₘ : Type u_4
Sₘ : Type u_5
inst✝⁸ : CommSemiring Rₘ
inst✝⁷ : CommSemiring Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : ↥M
⊢ (algebraMap Rₘ Sₘ) (mk' Rₘ x y) = mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
    IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
    IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← map_mul, mul_comm,
    IsLocalization.mul_mk'_eq_mk'_of_mul]
  exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)

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

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

Tactic:
← image2_mul,

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ star '' image2 (fun x1 x2 ↦ x1 * x2) s t = image2 (fun x1 x2 ↦ x1 * x2) (star '' t) (star '' s)
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
⊢ NonAssocSemiring α

Tactic:
apply e.injective.nonAssocSemiring _ <;> intros

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 0 = 0

case one
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := ⋯
add_monoid_with_one : AddMonoidWithOne α := ⋯
⊢ e 1 = 1

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
x✝ y✝ : α
⊢ e (x✝ + y✝) = e x✝ + e y✝

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
n✝ : ℕ
x✝ : α
⊢ e (n✝ • x✝) = n✝ • e x✝

case natCast
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonAssocSemiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
n✝ : ℕ
⊢ e ↑n✝ = ↑n✝
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • (↑⋯.unit)⁻¹ʳ = (↑h'.subInvSMul)⁻¹ʳ

Tactic:
Ring.inverse_unit,

Goal state after:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = (↑h'.subInvSMul)⁻¹ʳ
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = (↑h'.subInvSMul)⁻¹ʳ

Tactic:
Ring.inverse_unit,

Goal state after:
case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = ↑h'.subInvSMul⁻¹
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
suffices h : adjoin A ((⊤ : Subalgebra R B).map (includeRight (A := A)) : Set (A ⊗[R] B)) = ⊤ by
    simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤
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✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
have := Set.singleton_subset_iff.mpr (zero_mem_spectrum_inr R S a)

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
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✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
rw [← Set.union_eq_self_of_subset_right this, ← quasispectrum_eq_spectrum_union_zero]

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
this : {0} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ quasispectrum R ↑a
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
⊢ 0 ≤ x

Tactic:
have := by simpa [← mul_assoc] using star_right_conjugate_nonneg h v

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 ≤ v * u * x * star u * star v
⊢ 0 ≤ x
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0

Tactic:
contrapose!

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∃ x, ∀ (a : R), a ≠ 0 → a • x ≠ 0) → Module.rank R M ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a✝ : Nontrivial R
⊢ (∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0

Tactic:
· intro h
    rw [← nonpos_iff_eq_zero, Module.rank_def]
    apply ciSup_le'
    intro ⟨s, hs⟩
    rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]
    rintro ⟨i : s⟩
    obtain ⟨a, ha, ha'⟩ := h i
    apply ha
    simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ 0 < Module.rank R M ↔ ∃ x, x ≠ 0

Tactic:
contrapose!

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ s.toFinset.card = n

Tactic:
by simpa using hs'

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B✝ : Type w
C✝ : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B✝
inst✝¹² : StarRing B✝
inst✝¹¹ : Module R B✝
inst✝¹⁰ : FunLike F A B✝
inst✝⁹ : NonUnitalAlgHomClass F R A B✝
inst✝⁸ : StarHomClass F A B✝
S : NonUnitalStarSubalgebra R A
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B✝ B✝
inst✝² : SMulCommClass R B✝ B✝
inst✝¹ : StarModule R B✝
inst✝ : Subsingleton A
B C : NonUnitalStarSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ 1 ≤ finrank R ↥S ↔ S ≠ ⊥

Tactic:
contrapose!

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsTorsionFree R M
inst✝¹ : StrongRankCondition R
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S < 1 ↔ S = ⊥
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c₁ c₂ : R
h : c₁ • x = c₂ • x
⊢ σ c₁ • y = σ c₂ • y

Tactic:
← sub_eq_zero,

Goal state after:
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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c₁ c₂ : R
h : c₁ • x - c₂ • x = 0
⊢ σ c₁ • y - σ c₂ • y = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ σ (Classical.choose ⋯) • y = σ c • y

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ σ (Classical.choose ⋯) • y - σ c • y = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
fst✝ : Type v
b : Basis fst✝ K V
⊢ Subsingleton V

Tactic:
have := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
fst✝ : Type v
b : Basis fst✝ K V
this : IsEmpty fst✝
⊢ Subsingleton V
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
f : V →ₗ[K] V
hinj : Injective ⇑f
h : Module.rank K ↥f.range = Module.rank K V
⊢ Surjective ⇑f

Tactic:
rw [← finrank_eq_rank, ← finrank_eq_rank, Nat.cast_inj] at h

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : V →ₗ[K] V
hinj : Injective ⇑f
h : finrank K ↥f.range = finrank K V
⊢ Surjective ⇑f
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal

Tactic:
have := Module.Free.of_equiv (topEquiv (R := K) (M := V)).symm
  rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝¹ : Nontrivial K
s : Type v
hs : Basis s K V
this✝ : Finite s
this : lift.{max u v, v} #V = lift.{v, max u v} #(s → K)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
mk_arrow,

Goal state after:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝¹ : Nontrivial K
s : Type v
hs : Basis s K V
this✝ : Finite s
this : lift.{max u v, v} #V = lift.{v, max u v} (lift.{v, u} #K ^ lift.{u, v} #s)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
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
S : Submodule K V
w : V
hS : finrank K ↥S = 1
hw : w ∈ S
hw0 : w ≠ 0
⊢ S = K ∙ w

Tactic:
by
  have : FiniteDimensional K S := Module.finite_of_finrank_pos (by lia)
  exact Eq.symm <| eq_of_le_of_finrank_le (by simpa)
    (by rw [hS, finrank_span_singleton hw0])

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p.comp q * q + ↑n * p.comp q = p.comp q * (q + ↑n)

Tactic:
Nat.cast_comm,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p.comp q * q + p.comp q * ↑n = p.comp q * (q + ↑n)