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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
⊢ Fintype.card m = Fintype.card n

Tactic:
by
  obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)
  have : LinearIndependent R fun i => b i • a := by
    have hb := b.linearIndependent
    rw [Fintype.linearIndependent_iff] at hb ⊢
    intro g hg
    apply hb g
    simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
    exact hg.resolve_right ha
  exact le_antisymm
    (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
      ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
    (c.card_le_card_of_linearIndependent this)

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
⊢ single i j a ∈ S.matrix ↔ a ∈ S

Tactic:
by
  simp only [Set.mem_matrix, single, of_apply]
  conv_lhs => intro _ _; rw [ite_mem]
  simp [hS]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = ∑ i, ↑(f i) • v i

Tactic:
finsuppTotal_apply,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ (f.sum fun i x ↦ ↑x • v i) = ∑ i, ↑(f i) • v i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (finsuppTotal ι M I v) (Finsupp.mapRange (fun r ↦ if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a) = a.sum fun i c ↦ c • v i

Tactic:
finsuppTotal_apply,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ((Finsupp.mapRange (fun r ↦ if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a).sum fun i x ↦ ↑x • v i) = a.sum fun i c ↦ c • v i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
by_cases h₂ : k = b

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
by_cases h₂ : k = b

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
⊢ (finsuppTotal ι M I v).range = I • Submodule.span R (Set.range v)

Tactic:
by
  ext
  rw [Submodule.mem_ideal_smul_span_iff_exists_sum]
  refine ⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩
  rintro ⟨a, ha, rfl⟩
  classical
    refine ⟨a.mapRange (fun r => if h : r ∈ I then ⟨r, h⟩ else 0)
      (by simp only [Submodule.zero_mem, ↓reduceDIte]; rfl), ?_⟩
    rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]
    · apply Finsupp.sum_congr
      intro i _
      rw [dif_pos (ha i)]
    · exact fun _ => zero_smul _ _

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
I : Ideal R
M : Submodule R A
r : R
left✝ : r ∈ ↑I
a : A
a✝ : a ∈ M
⊢ Commute ((Algebra.linearMap R A) r) a

Tactic:
apply Algebra.commutes

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
e : m ≃ n
M : Matrix m n α
⊢ M.submatrix id ⇑e * Mᵀ.submatrix (⇑e) id = M * Mᵀ

Tactic:
rw [submatrix_mul_equiv, submatrix_id_id]

Goal state after:
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
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M

Tactic:
exact .inr h

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | t₁ x 0}
⊢ t₂ a b

Tactic:
rw [h] at H'

Goal state after:
case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ t₂ a b
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
⊢ Injective ⇑(map f) ↔ ∀ (i : ι), Injective ⇑(f i)

Tactic:
exact DFinsupp.mapRange_injective (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
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

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.Injective ⇑(lmap f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)

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

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

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).rangeS = S.toSubsemiring

Tactic:
algebraMap_eq,

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ((algebraMap A A).comp ↑S.val).rangeS = S.toSubsemiring
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ (algebraMap (↥S) A).range = S.toSubring

Tactic:
algebraMap_eq,

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ((algebraMap A A).comp ↑S.val).range = S.toSubring
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
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

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

Goal state before:
pp: 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✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι
j : κ
⊢ (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j

Tactic:
by
  simp [tensorProduct]

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

Goal state before:
pp: 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✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
i : ι × κ
⊢ (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2

Tactic:
by
  simp [tensorProduct]

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

Goal state before:
pp: 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✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
m : M
n : N
i : ι
j : κ
⊢ ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i

Tactic:
by
  simp [tensorProduct]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Mul R
inst✝ : Star R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x

Tactic:
simp only [Commute, SemiconjBy, hx.star_eq]

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
hrx : IsSelfAdjoint (r • x)
⊢ IsSelfAdjoint x

Tactic:
lift r to Rˣ using hu

Goal state after:
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
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint x
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
⊢ ⅟2 • (x + star x) ∈ selfAdjoint A

Tactic:
rw [selfAdjoint.mem_iff, star_smul, star_trivial, star_add, star_star, add_comm]

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

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ (diagonal d).blockDiag k i i = diagonal (fun i ↦ d (i, k)) i i

pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j

Tactic:
· rw [blockDiag_apply, diagonal_apply_eq, diagonal_apply_eq]

Goal state after:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ (diagonal d).blockDiag k i j = diagonal (fun i ↦ d (i, k)) i j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
⊢ vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ

Tactic:
ext i j
  rfl

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ⊆ ↑t ↔ s ≤ t
⊢ IsGLB ((fun {x} ↦ ↑x) '' S) ↑(sInf S)

Tactic:
convert! isGLB_biInf (s := S) (f := SetLike.coe)

Goal state after:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, ↑s ⊆ ↑t ↔ s ≤ t
⊢ ↑(sInf S) = ⨅ x ∈ S, ↑x
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case pos
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
this : DecidableEq M
val✝ : Fintype ι
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
ih : ∀ N' ≤ ⊥, ∀ x ∈ ⊥, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥⊥)

Tactic:
exact ⟨0, ⟨Basis.empty _⟩⟩

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
r : R
i✝ j✝ : m
⊢ (toMatrix b b) ((lmul R S) ((algebraMap R S) r)) i✝ j✝ = (algebraMap R (Matrix m m R)) r i✝ j✝

Tactic:
rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq m
A : Type u_4
M : Type u_5
n : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommSemiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A M
bA : Basis m R A
bM : Basis n A M
f : M →ₗ[A] M
⊢ (toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) =
    (Matrix.comp n n m m R) (((toMatrix bM bM) f).map ⇑(leftMulMatrix bA))

Tactic:
by
  ext; simp [toMatrix, Algebra.leftMulMatrix_apply,
    Basis.smulTower'_repr, Basis.smulTower'_apply, mul_comm]

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

Goal state before:
pp: case surj
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ y * (algebraMap R S) (h.symm.toRingHom (h ↑s)) = (algebraMap R S) (h.symm.toRingHom (h x))

Tactic:
convert! e

Goal state after:
case e'_2
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ h.symm.toRingHom (h ↑s) = ↑s

case e'_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
y : S
x : R
s : ↥M
e : y * (algebraMap R S) ↑s = (algebraMap R S) x
⊢ h.symm.toRingHom (h x) = x
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
x : ↥I ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (rTensor M (inclusion hle)) y

Tactic:
by
  obtain ⟨J, fg, y, rfl⟩ := exists_fg_le_eq_rTensor_subtype x
  refine ⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) y, ?_⟩
  rw [← LinearMap.rTensor_comp_apply]; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
⊢ Algebra.IsEpi R A

Tactic:
refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_
  obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective R x
  set f := algebraMap R A with hf
  replace hb : f b ≠ 0 := by aesop
  calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ hb]

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
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← mul_smul_comm,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring 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
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f a₁ * f a₂ * (g b₁ * g b₂) = f a₁ * g b₁ * (f a₂ * g b₂)

Tactic:
(hfg a₂ b₁).mul_mul_mul_comm

Goal state after:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring 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
inst✝³ : Semiring D
inst✝² : Algebra R D
inst✝¹ : Algebra R C
inst✝ : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute (f x) (g y)
a₁ a₂ : A
b₁ b₂ : B
⊢ f a₁ * g b₁ * (f a₂ * g b₂) = f a₁ * g b₁ * (f a₂ * g b₂)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a ⊆ quasispectrum S a

Tactic:
simpa only [quasispectrum.preimage_algebraMap] using
      (quasispectrum S a).image_preimage_subset (algebraMap R S)

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

Goal state before:
pp: case inr
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 : A
f : S → R
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)
s : S
hs : s ∈ spectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
obtain ⟨r, rfl⟩ := h hs
      rw [hf r]

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

Goal state before:
pp: case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) x_r * (algebraMap R C) r✝ + (x_r • φ a✝ + r✝ • φ x_a + φ x_a * φ a✝) =
    (algebraMap R C) x_r * (algebraMap R C) r✝ + (algebraMap R C) x_r * φ a✝ + φ x_a * ((algebraMap R C) r✝ + φ a✝)

Tactic:
mul_add

Goal state after:
case inl_add_inr.inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
r✝ : R
a✝ : A
⊢ (algebraMap R C) x_r * (algebraMap R C) r✝ + (x_r • φ a✝ + r✝ • φ x_a + φ x_a * φ a✝) =
    (algebraMap R C) x_r * (algebraMap R C) r✝ + (algebraMap R C) x_r * φ a✝ +
      (φ x_a * (algebraMap R C) r✝ + φ x_a * φ a✝)
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

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

Tactic:
intro i j x hxi hxj
    rcases dir i j with ⟨k, hik, hjk⟩
    simp [hf i k hik, hf j k hjk]

Goal state after: