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

Goal state before:
pp: l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n✝
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ((diagonal fun x ↦ ↑n) + diagonal fun x ↦ 1) = (diagonal fun x ↦ ↑n) + 1

Tactic:
diagonal_one

Goal state after:
l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n✝
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ (diagonal fun x ↦ ↑n) + 1 = (diagonal fun x ↦ ↑n) + 1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔ ¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀

Tactic:
by
    push Not
    refine ⟨fun ⟨n, f, inj⟩ ↦ ⟨n, ?_⟩, fun ⟨n, le⟩ ↦
      ⟨n, le_rank_iff_exists_linearMap.mp (natCast_le_aleph0.trans le)⟩⟩
    have ⟨g, hg⟩ := f.exists_finsupp_nat_of_fin_fun_injective inj
    convert! (Finsupp.basisSingleOne.linearIndependent.map_injOn _ hg.injOn).cardinal_lift_le_rank
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ span R (⇑(Algebra.linearMap R A) '' {1}) = 1

Tactic:
Set.image_singleton,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ R ∙ (Algebra.linearMap R A) 1 = 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u : l → α
v w : m → α
x : n → α
⊢ vecMulVec u (v ᵥ* vecMulVec w x) = vecMulVec u ((v ⬝ᵥ w) • x)

Tactic:
vecMul_vecMulVec

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u : l → α
v w : m → α
x : n → α
⊢ vecMulVec u ((v ⬝ᵥ w) • x) = vecMulVec u ((v ⬝ᵥ w) • x)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
exact mul_right_injective_iff_mulVec_injective

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x

Tactic:
simp [sub_eq_add_neg, add_mulVec, neg_mulVec]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ Multiset.count a (toMultiset f) = f.sum fun x n ↦ Multiset.count a (n • {x})

Tactic:
by
      rw [toMultiset_apply]; exact map_sum (Multiset.countAddMonoidHom a) _ f.support

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
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup (insert (A i) (A '' {j})) = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
Set.image_singleton,

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup {A i, A j} = ⊤ ↔ IsCompl (A i) (A j)
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 : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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 : NonUnitalSubalgebra R A
hT : T = iSup K
⊢ ↥T →ₙₐ[R] B

Tactic:
by
  subst hT
  exact
      { toFun :=
          Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
            (fun i j x hxi hxj => by
              let ⟨k, hik, hjk⟩ := dir i j
              rw [hf i k hik, hf j k hjk]
              rfl)
            _ (by rw [coe_iSup_of_directed dir])
        map_zero' := by
          dsimp
          exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)
        map_mul' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· * ·))
          all_goals simp
        map_add' := by
          dsimp
          apply Set.iUnionLift_binary (coe_iSup_of_directed dir) dir _ (fun _ => (· + ·))
          all_goals simp
        map_smul' := fun r => by
          dsimp
          apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
            (fun _ _ => rfl)
          all_goals simp }

Goal state after:
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'
⊢ 0 = single (i, k) (j, l) r (i, k) (j, l')

Tactic:
single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd 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 = 0
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
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ (fromBlocks A B C D).submatrix Sum.swap f i j = (fromBlocks C D A B).submatrix id f i j

Tactic:
cases i <;> dsimp <;> cases f j <;> rfl

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

Goal state before:
pp: case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = diagonal (Function.update v i x) j k

Tactic:
diagonal_apply_ne _ hjk

Goal state after:
case inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ diagonal v j k = 0

Tactic:
diagonal_apply_ne _ hjk

Goal state after:
case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq m
inst✝ : Mul α
u : m → α
v : n → α
i : m
a : α
i' : m
j : n
hi : i' ≠ i
⊢ vecMulVec (Function.update u i a) v i' j = (vecMulVec u v).updateRow i (a • v) i' j

Tactic:
· simp [vecMulVec_apply, hi]

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

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
j : n
a : α
i : m
j' : n
hi : j' ≠ j
⊢ vecMulVec u (Function.update v j a) i j' = (vecMulVec u v).updateCol j (MulOpposite.op a • u) i j'

Tactic:
· simp [vecMulVec_apply, hi]

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

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i j = of (fun i ↦ vecCons (v i) (Aᵀ i)) i j

Tactic:
refine Fin.cases ?_ ?_ j

Goal state after:
case refine_1
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ (of (vecCons v A))ᵀ i 0 = of (fun i ↦ vecCons (v i) (Aᵀ i)) i 0

case refine_2
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin m.succ
⊢ ∀ (i_1 : Fin m), (of (vecCons v A))ᵀ i i_1.succ = of (fun i ↦ vecCons (v i) (Aᵀ i)) i i_1.succ
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x✝¹ : A ⊗[R] ↥p
x✝ : x✝¹ ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}
a : A
m : ↥p
h : a ⊗ₜ[R] m = x✝¹
⊢ x✝¹ ∈ ↑(comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p)))

Tactic:
← h,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x✝¹ : A ⊗[R] ↥p
x✝ : x✝¹ ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}
a : A
m : ↥p
h : a ⊗ₜ[R] m = x✝¹
⊢ a ⊗ₜ[R] m ∈ ↑(comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p)))
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: 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
⊢ ∀ (a b : X × ↥S), a ≈ b → add'' a.fst a.snd r₂ s₂ = add'' b.fst b.snd r₂ s₂

Tactic:
rintro ⟨r₁', s₁'⟩ ⟨r₁, s₁⟩ ⟨sb, rb, hb, hb'⟩

Goal state after:
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₁ : X
s₁ sb : ↥S
rb : R
hb : sb • (r₁, s₁).fst = rb • (r₁', s₁').fst
hb' : ↑sb * ↑(r₁, s₁).snd = rb * ↑(r₁', s₁').snd
⊢ add'' (r₁', s₁').fst (r₁', s₁').snd r₂ s₂ = add'' (r₁, s₁).fst (r₁, s₁).snd r₂ s₂
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ (Function.Injective fun x ↦ M *ᵥ x) ↔ LinearIndependent R M.col

Tactic:
← M.vecMul_transpose,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ (Function.Injective fun x ↦ x ᵥ* Mᵀ) ↔ LinearIndependent R M.col
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
⊢ ((toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0

Tactic:
rw [toLin_apply]

Goal state after:
m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
⊢ ∑ j, (A *ᵥ ⇑(v₁.repr x)) j • v₂ j = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: 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₁
x : R
i✝ j✝ : n
⊢ Pi.single j✝ x i✝ = Matrix.diagonal (fun x_1 ↦ x) i✝ j✝

Tactic:
Matrix.diagonal_apply,

Goal state after:
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₁
x : R
i✝ j✝ : n
⊢ Pi.single j✝ x i✝ = if i✝ = j✝ then x else 0
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
m : Matrix ι ι (End A M)
x✝¹ y✝ : ι → M
x✝ : ι
⊢ ∑ j, (m x✝ j) ((x✝¹ + y✝) j) = ((fun i ↦ ∑ j, (m i j) (x✝¹ j)) + fun i ↦ ∑ j, (m i j) (y✝ j)) x✝

Tactic:
simp [Finset.sum_add_distrib]

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 : R
y : ↥M
z : R
h : z * ↑y = x
⊢ (algebraMap R S) z * (algebraMap R S) ↑y = (algebraMap R S) x

Tactic:
← h,

Goal state after:
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
z : R
h : z * ↑y = x
⊢ (algebraMap R S) z * (algebraMap R S) ↑y = (algebraMap R S) (z * ↑y)
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S ↑(adjoin R s) = adjoin S s

Tactic:
apply le_antisymm (adjoin_le _)

Goal state after:
R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ adjoin S s ≤ adjoin S ↑(adjoin R s)

R : Type uR
S : Type uS
A : Type uA
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
s : Set A
⊢ ↑(adjoin R s) ⊆ ↑(adjoin S s)
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
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
⊢ f.fieldRange = Subfield.closure s

Tactic:
ringHom_fieldRange_eq_of_comp_eq h,

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
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
⊢ Subfield.closure ↑g.range = Subfield.closure s
Module: Mathlib.Algebra.Star.Pointwise

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

Tactic:
by
  rw [← star_subset_star, star_star]

Goal state after:
Module: Mathlib.Tactic.NoncommRing

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

Tactic:
simp only [nsmul_eq_mul, Nat.cast_ofNat]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial 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
⊢ ¬IsUnit ↑a

Tactic:
rintro ⟨u, hu⟩

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial 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
u : (Unitization S A)ˣ
hu : ↑u = ↑a
⊢ False
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ Set.RightInvOn e (⇑(algebraMap R₁ R₃)) (quasispectrum R₃ a)

Tactic:
convert! hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem

Goal state after:
R₁ : Type u_6
R₂ : Type u_7
R₃ : Type u_8
A : Type u_9
inst✝¹³ : Semifield R₁
inst✝¹² : Field R₂
inst✝¹¹ : Field R₃
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R₁ A
inst✝⁸ : Module R₂ A
inst✝⁷ : Module R₃ A
inst✝⁶ : Algebra R₁ R₂
inst✝⁵ : Algebra R₂ R₃
inst✝⁴ : Algebra R₁ R₃
inst✝³ : IsScalarTower R₁ R₂ R₃
inst✝² : IsScalarTower R₂ R₃ A
inst✝¹ : IsScalarTower R₃ A A
inst✝ : SMulCommClass R₃ A A
a : A
f : R₃ → R₂
g : R₂ → R₁
e : R₃ → R₁
hfge : g ∘ f = e
hf : QuasispectrumRestricts a f
hg : QuasispectrumRestricts a g
⊢ ⇑(algebraMap R₁ R₃) = ⇑(algebraMap R₂ R₃) ∘ ⇑(algebraMap R₁ R₂)
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✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S b ∪ {0})

Tactic:
← h,

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a b : A
f : S → R
ha : SpectrumRestricts a f
h : spectrum S a = spectrum S b
⊢ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a ∪ {0})
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑hx.unit⁻¹ i = ↑⋯.unit⁻¹

Tactic:
rw [← Units.inv_eq_val_inv, ← MulEquiv.val_inv_piUnits_apply]

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
hx : IsUnit x
i : ι
⊢ ↑(MulEquiv.piUnits hx.unit i)⁻¹ = ↑⋯.unit⁻¹
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T K : Subalgebra R A
⊢ K ≤ centralizer R ↑(S ⊔ T) ↔ K ≤ centralizer R ↑S ⊓ centralizer R ↑T

Tactic:
by
    simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ x ≤ y

Tactic:
rw [← f_inv_f x, ← f_inv_f y]

Goal state after:
R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁹ : NonUnitalSemiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : StarRing R
inst✝⁶ : StarOrderedRing R
inst✝⁵ : NonUnitalSemiring S
inst✝⁴ : PartialOrder S
inst✝³ : StarRing S
inst✝² : StarOrderedRing S
inst✝¹ : EquivLike F R S
inst✝ : StarRingEquivClass F R S
f : F
x y : R
h : f x ≤ f y
f_inv : S →⋆ₙ+* R := ↑(↑f).symm
f_inv_f : ∀ (r : R), f_inv (f r) = r
⊢ f_inv (f x) ≤ f_inv (f y)
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✝¹ : 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 : ∑ e ∈ t', g e • e = 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)

Goal state after:
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 : ∑ e ∈ t', g e • e = 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₀)
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∑ e ∈ t, f e = 0 ∧ ∃ x ∈ t, f 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 : NonUnitalStarSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
this : f (b j) = 0
⊢ f (b j) = (f (b i) • b.coord i) (b j)

Tactic:
simp [Finsupp.single_eq_of_ne h, this]

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

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
⊢ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
obtain ⟨v₀, hv⟩ := rank_le_one_iff.1 h.le

Goal state after:
case refine_1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ r, r • v₀ = v
⊢ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v