mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = lift.{v, max u v} #(ChooseBasisIndex R M →₀ R)
⊢ Module.rank R M = #M

Tactic:
simp only [mk_finsupp_lift_of_infinite', ← rank_eq_card_chooseBasisIndex, lift_max,
    lift_lift] at h

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
h : lift.{max u v, v} #M = max (lift.{max u v, v} (Module.rank R M)) (lift.{v, u} #R)
⊢ Module.rank R M = #M
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case neg
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ finrank S M ≤ finrank R M

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ finrank R S ≤ finrank R T

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon

Tactic:
exact le_sup_right

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

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
⊢ Surjective ⇑(map f) ↔ ∀ (i : ι), Surjective ⇑(f i)

Tactic:
exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
⊢ motive x

Tactic:
by
  let T : Subalgebra R A :=
  { carrier := {x | motive x}
    mul_mem' {a b} := mul a b
    add_mem' {a b} := add a b
    algebraMap_mem' := algebraMap }
  suffices iSup S ≤ T from this mem
  rwa [iSup_le_iff]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (N i)
inst✝ : (i : ι) → Module R (N i)
f : (i : ι) → M i →ₗ[R] N i
⊢ Function.Surjective ⇑(lmap f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)

Tactic:
exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
i : ι
k : κ
hik : i = e.symm k
x : M i
y : M (e.symm k)
hxy : cast ⋯ x = y
⊢ (lequivCongrLeft R e) ((lof R ι M i) x) = (lof R κ (fun i ↦ M (e.symm i)) k) y

Tactic:
subst hik hxy
  ext j
  simp [lof_eq_of, of_apply]
  lia

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
f₁ f₂ : ι →₀ M
hf₁ : ((finsuppTensorFinsupp R S M N ι κ) (f₁ ⊗ₜ[R] g)) (i, k) = f₁ i ⊗ₜ[R] g k
hf₂ : ((finsuppTensorFinsupp R S M N ι κ) (f₂ ⊗ₜ[R] g)) (i, k) = f₂ i ⊗ₜ[R] g k
⊢ ((finsuppTensorFinsupp R S M N ι κ) ((f₁ + f₂) ⊗ₜ[R] g)) (i, k) = (f₁ + f₂) i ⊗ₜ[R] g k

Tactic:
simp [add_tmul, hf₁, hf₂]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
⊢ IsSelfAdjoint (x * y)

case refine_2
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : IsSelfAdjoint (x * y)
⊢ Commute x y
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))

Tactic:
Submodule.mem_span

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p
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:
rw [apply_ite f, hf]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁸ : CommSemiring R
inst✝²⁷ : Semiring A
inst✝²⁶ : Semiring B
inst✝²⁵ : Algebra R A
inst✝²⁴ : Algebra R B
inst✝²³ : AddCommMonoid M
inst✝²² : Module R M
inst✝²¹ : Module A M
inst✝²⁰ : IsScalarTower R A M
inst✝¹⁹ : AddCommMonoid N
inst✝¹⁸ : Module R N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : Module R P
inst✝¹⁵ : Module A P
inst✝¹⁴ : IsScalarTower R A P
inst✝¹³ : AddCommMonoid Q
inst✝¹² : Module R Q
inst✝¹¹ : AddCommMonoid P'
inst✝¹⁰ : Module R P'
inst✝⁹ : Module A P'
inst✝⁸ : Module B P'
inst✝⁷ : IsScalarTower R A P'
inst✝⁶ : IsScalarTower R B P'
inst✝⁵ : SMulCommClass A B P'
inst✝⁴ : AddCommMonoid Q'
inst✝³ : Module R Q'
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
x✝¹ : B
x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ (lift (x✝¹ • x✝)) (x ⊗ₜ[R] y) = ((RingHom.id B) x✝¹ • lift x✝) (x ⊗ₜ[R] y)

Tactic:
simp only [lift_tmul, smul_apply, RingHom.id_apply]

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₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ ψ'.submoduleImage N = R ∙ generator (ϕ.submoduleImage N)

Tactic:
span_singleton_generator

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₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ ψ'.submoduleImage N = ϕ.submoduleImage N
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ 0⁻¹ = 0

Tactic:
by
  rw [OreLocalization.zero_def, OreLocalization.inv_def]
  simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x + (lmul R S) y) = (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y)

Tactic:
map_add

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y) =
    (toMatrix b b) ((lmul R S) x) + (toMatrix b b) ((lmul R S) y)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a.add
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✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) (x✝ + y✝) ∈ Submodule.span A ↑l.range

Tactic:
map_add

Goal state after:
case a.add
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✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) x✝ + (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B) (x_1 y_1 : A ⊗[R] B),
    (x_1 * x ⊗ₜ[R] y) • m = x_1 • x ⊗ₜ[R] y • m →
      (y_1 * x ⊗ₜ[R] y) • m = y_1 • x ⊗ₜ[R] y • m → ((x_1 + y_1) * x ⊗ₜ[R] y) • m = (x_1 + y_1) • x ⊗ₜ[R] y • m

Tactic:
intro a b z w hz hw

Goal state after:
case refine_3.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • a ⊗ₜ[R] b • m
hw : (w * a ⊗ₜ[R] b) • m = w • a ⊗ₜ[R] b • m
⊢ ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • a ⊗ₜ[R] b • m
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)
⊢ Function.Surjective ⇑((mk R S M) 1)

Tactic:
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
  rintro _ ⟨x, y, rfl⟩
  obtain ⟨x, rfl⟩ := h x
  rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
  exact ⟨x • y, rfl⟩

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:
← sub_add_cancel (↑hx.unit⁻¹ : R) 1,

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 = 1 - 1
⊢ 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:
← sub_add_cancel (↑hx.unit⁻¹ : R) 1,

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 = 1 - 1
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ IsQuasiregular ↑a ↔ IsQuasiregular a

Tactic:
by
  refine ⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩
  rw [isQuasiregular_iff] at ha ⊢
  obtain ⟨y, hy₁, hy₂⟩ := ha
  lift y to A using by simpa using congr(fstHom R A $(hy₁))
  refine ⟨y, ?_, ?_⟩ <;> exact inr_injective (R := R) <| by simpa

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

Goal state before:
pp: 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 : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a

Tactic:
have : { r | ¬ IsUnit r} ⊆ spectrum R _ := mem_spectrum_inr_of_not_isUnit a

Goal state after:
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 : A
r : R
this : {r | ¬IsUnit r} ⊆ spectrum R ↑a
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R ↑a
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
a : R
ha : IsSelfAdjoint a
⊢ 0 ≤ a * a

Tactic:
simpa [ha.star_eq] using star_mul_self_nonneg a

Goal state after:
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
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c < star c * b * c

Tactic:
rw [(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a b : R
hab : a < b
c : R
hc : IsRegular c
⊢ a ≠ b
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x ∈ t.erase x₀, (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x +
      -((∑ z ∈ t.erase x₀, g (z - x₀)) • x₀) =
    0

Tactic:
sum_smul,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : ∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀) = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∑ x ∈ t.erase x₀, (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x +
      -∑ i ∈ t.erase x₀, g (i - x₀) • x₀ =
    0
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S T : NonUnitalStarSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Goal state after:
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
inst✝ : Nontrivial R
⊢ Set.finrank R ∅ = 0

Tactic:
Set.finrank,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
⊢ finrank R ↥(span R ∅) = 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
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = 1 • y

Tactic:
rw [← RingHom.map_one, ← mkSpanSingleton'_apply x y H 1 ?_]

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
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨x, h⟩ = ↑(mkSpanSingleton' x y H) ⟨1 • x, ?m.71⟩

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
h : x ∈ (mkSpanSingleton' x y H).domain
⊢ 1 • x ∈ (mkSpanSingleton' x y H).domain
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
⊢ ∀ (a b c : E →ₛₗ.[σ] F), a ≤ b → a ≤ c → a ≤ { domain := b.eqLocus c, toFun := b.toFun ∘ₛₗ inclusion ⋯ }

Tactic:
intro f g h ⟨fg_le, fg_eq⟩ ⟨fh_le, fh_eq⟩

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
f g h : E →ₛₗ.[σ] F
fg_le : f.domain ≤ g.domain
fg_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
fh_le : f.domain ≤ h.domain
fh_eq : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥h.domain⦄, ↑x = ↑y → ↑f x = ↑h y
⊢ f ≤ { domain := g.eqLocus h, toFun := g.toFun ∘ₛₗ inclusion ⋯ }
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
s : Submodule K V
inst✝ : Free K ↥s
x✝¹ : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ r, r • v₀ = v
x✝ : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • ⟨v₀, hv₀⟩ = ⟨v, hv⟩

Tactic:
by rwa [Subtype.ext_iff, coe_smul]

Goal state after:
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
⊢ ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y

Tactic:
intro p

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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
p : ↑c
⊢ ∀ (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₛₗ.[σ] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
x' : ↥p.domain := (inclusion ⋯) ⟨↑x, ⋯⟩
y' : ↥p.domain := (inclusion ⋯) ⟨↑y, ⋯⟩
⊢ ↑↑⟨p, hpc⟩ (x' + y') = ↑↑⟨p, hpc⟩ x' + ↑↑⟨p, hpc⟩ y'

Tactic:
map_add

Goal state after:
case w.refine_1
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
x y : ↥(sSup (domain '' c))
p : E →ₛₗ.[σ] F
hpc : p ∈ c
hpx : ↑↑(P x) ≤ p
hpy : ↑↑(P y) ≤ p
x' : ↥p.domain := (inclusion ⋯) ⟨↑x, ⋯⟩
y' : ↥p.domain := (inclusion ⋯) ⟨↑y, ⋯⟩
⊢ ↑↑⟨p, hpc⟩ x' + ↑↑⟨p, hpc⟩ y' = ↑↑⟨p, hpc⟩ x' + ↑↑⟨p, hpc⟩ y'