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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (1 *ᵥ v) x✝ = v x✝

Tactic:
rw [← diagonal_one, mulVec_diagonal, one_mul]

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower' c) ij = b ij.2 • c ij.1

Tactic:
rw [smulTower', reindex_apply, smulTower_apply]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ b ((Equiv.prodComm ι ι').symm ij).1 • c ((Equiv.prodComm ι ι').symm ij).2 = b ij.2 • c ij.1
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : toFinset 0 = {a}
h : s.card = 0
⊢ False

Tactic:
toFinset_zero

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : ∅ = {a}
h : s.card = 0
⊢ False
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ ((fun s ↦ { support := s.toFinset, toFun := fun a ↦ count a s, mem_support_toFun := ⋯ })
        ((fun f ↦ Finsupp.toMultiset f) f))
      a =
    f a

Tactic:
simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a = 0 → 0 = f a
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
by
  obtain rfl | h := Decidable.eq_or_ne j i
  · rw [DirectSum.of_eq_same, if_pos rfl]
  · rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

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

Goal state before:
pp: ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
by
  rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]
  exact Function.Bijective.surjective h

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
⊢ ⇑(h.collectedBasis v) = fun a ↦ ↑((v a.fst) a.snd)

Tactic:
by
  simp [IsInternal.collectedBasis, coeLinearMap, DFinsupp.mapRange.linearEquiv,
    toModule, DFinsupp.lsum]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j

Tactic:
by
      rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]

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

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✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
m : M
n : N
a✝ : ι
⊢ ((finsuppRight R S M N ι) (m ⊗ₜ[R] Finsupp.single i n)) a✝ = (Finsupp.single i (m ⊗ₜ[R] n)) a✝

Tactic:
simp +contextual [Finsupp.single_apply, apply_ite]

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
⊢ ((directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i

Tactic:
suffices (DirectSum.component S ι₂ _ i).restrictScalars R ∘ₗ
      (directSumRight R S M₁' M₂).toLinearMap.restrictScalars R ∘ₗ
        (TensorProduct.mk R M₁' (⨁ i, M₂ i) m) =
          (TensorProduct.mk R M₁' (M₂ i) m) ∘ₗ (DirectSum.component R ι₂ M₂ i) by
    simpa using! LinearMap.congr_fun this n
  ext j n
  by_cases hj : j = i
  · subst hj; simp
  · simp [DirectSum.component.of, hj]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddMonoid (R i)
inst✝ : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
⊢ star (single i r) = single i (star r)

Tactic:
ext; exact apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Monoid R
inst✝³ : StarMul R
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x

Tactic:
refine ⟨fun hrx ↦ ?_, .smul hr⟩
  lift r to Rˣ using hu
  rw [← inv_smul_smul r x]
  replace hr : IsSelfAdjoint r := Units.ext hr.star_eq
  exact hr.inv.smul hrx

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
inst✝ : TrivialStar R
x : R
⊢ Commute (star x) x

Tactic:
by rw [star_trivial]

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:
← Matrix.toLin_symm,

Goal state after:
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₂) ((toLin v₁ v₂).symm f) = f
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₂
M : Matrix m n R
⊢ (toMatrix v₁ v₂) ((toLin v₁ v₂) M) = M

Tactic:
← Matrix.toLin_symm,

Goal state after:
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₂
M : Matrix m n R
⊢ (toLin v₁ v₂).symm ((toLin v₁ v₂) M) = M
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
x : OreLocalization S R
⊢ x • 0 = 0

Tactic:
induction x with | _ r s
  rw [OreLocalization.zero_def, smul_div_one, smul_zero, zero_oreDiv, zero_oreDiv]

Goal state after:
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
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ ra * ↑s₂ ∈ S

Tactic:
← ha

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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ ↑(sa * s₁) ∈ S
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✝ : IsCancelMulZero M
⊢ ∀ {a : N}, a ≠ 0 → IsLeftRegular a

Tactic:
← Commute.isRightRegular_iff (Commute.all _)

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
⊢ ∀ {a : N}, a ≠ 0 → IsRightRegular a
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (ra * ↑s₃) ∈ S

Tactic:
← ha

Goal state after:
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
⊢ ↑sb * (↑sa * ↑s₂) ∈ S
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case inl
ι : Type u_5
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
R : Type u_8
M : Type u_9
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis ι R M
a : ι → R
s : End R M
hs : ∀ (k : ι), s (b k) = a k • b k
i j : ι
⊢ s (if j = j then b i else 0) - (b.end (i, j)) (s (b j)) =
    (if j = j then a i • b i else 0) - if j = j then a j • b i else 0

Tactic:
simp [hs, Basis.end_apply_apply]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm⟩ = ↑(c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩)

Tactic:
change _ = N.subtype _

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm⟩ = N.subtype (c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)

Tactic:
refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j
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
x y : ℤ
⊢ (algebraMap ℤ ℚ) x = (algebraMap ℤ ℚ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
eq_intCast,

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
x y : ℤ
⊢ ↑x = (algebraMap ℤ ℚ) y → ∃ c, ↑c * x = ↑c * y
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
x y : ℤ
⊢ ↑x = (algebraMap ℤ ℚ) y → ∃ c, ↑c * x = ↑c * y

Tactic:
eq_intCast,

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
x y : ℤ
⊢ ↑x = ↑y → ∃ c, ↑c * x = ↑c * 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 R s) ⊆ ↑(adjoin S s)

Tactic:
rw [← Subalgebra.coe_restrictScalars R (S := S), SetLike.coe_subset_coe]
    exact adjoin_le subset_adjoin

Goal state after:
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) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
← map_sub,

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 - (algebraMap R S) y) = 0
⊢ (algebraMap R S) x = (algebraMap R S) y
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul.tmul
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ r • (a' ⊗ₜ[R] b' * a ⊗ₜ[R] b) = a' ⊗ₜ[R] b' * r • a ⊗ₜ[R] b

Tactic:
dsimp
        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ {r | True} = univ

Tactic:
Set.ofPred_true

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ -σ a = σ (-a)

Tactic:
rw [spectrum, Set.compl_neg, spectrum, resolventSet_neg]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = f (a₁ ⊗ₜ[R] b₁) * f (a₂ ⊗ₜ[R] b₂)
x y : A ⊗[R] B
⊢ (LinearMap.mul S (A ⊗[R] B)).compr₂ f = (LinearMap.mul S C ∘ₗ f).compl₂ f

Tactic:
by
    -- these instances are needed by the statement of `ext`, but not by the current definition.
    let : Algebra R C := .restrictScalars R S C
    let : IsScalarTower R S C := .restrictScalars R S C
    ext
    dsimp
    exact hf _ _ _ _

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 ≤ v * u * x * star u * star v
⊢ 0 ≤ x

Tactic:
rwa [hv, one_mul, mul_assoc, ← star_mul, hv, star_one, mul_one] at this

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p

Tactic:
rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists,
      ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.comap opAddEquiv (AddSubmonoid.map opAddEquiv (AddSubmonoid.closure (range fun s ↦ star s * s))),
      unop y = unop x + p) ↔
    ∃ x_1, op x_1 ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + op x_1
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : StrongRankCondition R
inst✝³ : Free R M
inst✝² : Free R M'
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
⊢ finrank R (M × M') = finrank R M + finrank R M'

Tactic:
simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M']

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

Goal state before:
pp: case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
rw [← (b.matrix m n).mk_eq_rank'']

Goal state after:
case intro.intro
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
val✝¹ : Fintype m
val✝ : Fintype n
I : Type v
b : Basis I R M
⊢ #(m × n × I) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)

Tactic:
let B i := chooseBasis R (φ i)

Goal state after:
case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i ↦ chooseBasis R (φ i)
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)
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✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ #ι ≤ ↑(finrank R M)

Tactic:
← lift_le.{max v w}

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ lift.{max v w, w} #ι ≤ lift.{max v w, w} ↑(finrank R M)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
j : n
⊢ (⇑W.mkQ ∘ b ∘ Sum.inr) j = bQ j

Tactic:
apply Function.rightInverse_surjInv W.mkQ_surjective

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

Goal state before:
pp: case refine_2
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₀)
⊢ ∑ e ∈ t, f e = 0

Tactic:
simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1

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

Goal state before:
pp: case refine_2.inr
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ f ((Basis.mk H₁ ⋯) ⟨f.ker.subtype x, ⋯⟩) = (Finsupp.single ⟨f.ker.subtype x, ⋯⟩ 1) ⟨w, ⋯⟩

Tactic:
suffices x ≠ w by simp [this]
      apply_fun f
      simp [hw]

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
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c : R
h : c • x ∈ (mkSpanSingleton' x y H).domain
⊢ ↑(mkSpanSingleton' x y H) ⟨c • x, h⟩ = σ c • y

Tactic:
by
  dsimp [mkSpanSingleton']
  rw [← sub_eq_zero, ← sub_smul, ← RingHom.map_sub]
  apply H
  simp only [sub_smul, sub_eq_zero]
  apply Classical.choose_spec (mem_span_singleton.1 h)

Goal state after: