mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ liftCover S f hf hS ⁻¹' t = ⋃ i, Subtype.val '' f i ⁻¹' t

Tactic:
change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
  rw [preimage_comp, preimage_iUnionLift]
  ext; simp

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.rank R M

Tactic:
← not_lt,

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
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.rank R M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: 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
⊢ ℵ₀ ≤ Module.rank S M

Tactic:
← not_lt,

Goal state after:
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
⊢ ¬Module.rank S M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: 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
⊢ ℵ₀ ≤ Module.rank R S

Tactic:
← not_lt,

Goal state after:
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
⊢ ¬Module.rank R S < ℵ₀
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

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

Tactic:
by rw [ringCon_le_iff] at h1 h2 ⊢; exact sup_le h1 h2

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

Goal state before:
pp: case inr
ι : 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)
h : j ≠ i
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
· rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

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

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 1 ∈ s

Tactic:
simpa using h.2.2 1

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑((x • s) • t) = ↑(x • s • t)

Tactic:
← one_smul R s,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑((x • 1 • s) • t) = ↑(x • (1 • s) • t)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single.single
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
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k

Tactic:
| single k' n =>

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

Goal state before:
pp: I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
⊢ (comp I I J J R) (diagonal fun i ↦ diagonal fun j ↦ d i j) = diagonal fun ij ↦ d ij.1 ij.2

Tactic:
ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
  dsimp [comp_apply]
  obtain hi | rfl := ne_or_eq i₁ i₂
  · rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]
  rw [diagonal_apply_eq]
  obtain hj | rfl := ne_or_eq j₁ j₂
  · rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]
  rw [diagonal_apply_eq, diagonal_apply_eq]

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

Goal state before:
pp: R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star r * star ⅟r = 1

Tactic:
by rw [← star_mul, invOf_mul_self, star_one]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (M + N) i✝ j✝ = (blockDiagonal M + blockDiagonal N) i✝ j✝

Tactic:
simp only [blockDiagonal_apply, Pi.add_apply, add_apply]

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 else 0) =
    (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) + if i✝.2 = j✝.2 then N i✝.2 i✝.1 j✝.1 else 0
Module: Mathlib.Data.Matrix.Block

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

Tactic:
rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]

Goal state after:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ e₂.toFun (r • e₁.toFun a) = r • e₂.toFun (e₁.toFun a)

Tactic:
e₂.map_smul'

Goal state after:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ r • e₂.toFun (e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
a₀ a₁ a₂ b₀ b₁ b₂ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
h₂ : a₂ = b₂
⊢ ![a₀, a₁, a₂] = ![b₀, b₁, b₂]

Tactic:
simp [h₀, h₁, h₂]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
hr' : r = (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s ∈
    ↑(closure (↑S \ {(∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s}))

Tactic:
refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr']

Goal state after:
case refine_1
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
hr' : r = (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
s : M
hs : s ∈ S \ {r}
⊢ s ∈ ↑S \ {r}

case refine_2
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
hr' : r = (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
s : M
hs : s ∈ S \ {r}
⊢ s ∈ ↑S \ {r}
Module: Mathlib.LinearAlgebra.FreeModule.PID

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

Tactic:
ϕy_eq,

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

Tactic:
by
  ext; simp [vecMul_transpose]

Goal state after:
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₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrixAlgEquiv v₁) f k i

Tactic:
LinearMap.toMatrixAlgEquiv_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₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (v₁.reindexRange.repr (f (v₁.reindexRange ⟨v₁ i, ⋯⟩))) ⟨v₁ k, ⋯⟩ = (v₁.repr (f (v₁ i))) k
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) ((algebraMap S (Matrix n n S)) x (i, k).2 (j, k').2) (i, k).1 (j, k').1 =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')

Tactic:
blockDiagonal_apply,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) ((algebraMap S (Matrix n n S)) x (i, k).2 (j, k').2) (i, k).1 (j, k').1 =
    if (i, k).2 = (j, k').2 then (leftMulMatrix b) x (i, k).1 (j, k').1 else 0
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
⊢ IsLocalization M S ↔
    (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
isLocalization_iff_isLocalizationMap,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ M.IsLocalizationMap ⇑(algebraMap R S) ↔
    (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
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
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
by
    rw [IsLocalization.eq_iff_exists M]
    rintro ⟨c, hc⟩
    exact ⟨⟨c, h₁ c.2⟩, hc⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ ((algebraMap R K).comp e.symm.toRingHom).toAlgebra = inst✝¹

Tactic:
exact Algebra.algebra_ext _ _ (by simp [RingHom.algebraMap_toAlgebra, h])

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
r : R
⊢ σ a - {r} = σ (a - ↑ₐ r)

Tactic:
simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : FunLike F A R
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ φ a ∈ σ a

Tactic:
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
    simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
      Algebra.algebraMap_self, RingHom.id_apply, sub_self]
  simp only [spectrum.mem_iff, ← mem_nonunits_iff,
    coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0

Tactic:
simpa [-Units.inv_mul] using congr($(u.inv_mul).val)

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 : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * star x * x * c = star c * star x * (x * c)

Tactic:
mul_assoc _ _ c

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x : R
⊢ star c * star x * (x * c) = star c * star x * (x * c)
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:
by
    rw [← unop_le_unop, StarOrderedRing.le_iff, op_surjective.exists,
      ← (AddSubmonoid.closure _).comap_map_eq_of_injective opAddEquiv.injective]
    congr! with p
    · simp [AddMonoidHom.map_mclosure, ← range_comp', Function.comp_def,
        ← (star_involutive.surjective.comp op_surjective).range_comp]
    · simp [← op_inj (α := R)]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
ι : Type v
inst✝ : Fintype ι
⊢ toNat (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) = card ι * toNat (Module.rank R M)

Tactic:
← mk_toNat_eq_card,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
ι : Type v
inst✝ : Fintype ι
⊢ toNat (lift.{v, v} #ι * lift.{v, v} (Module.rank R M)) = toNat #ι * toNat (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ toNat (lift.{u, v} #ι) = card ι

Tactic:
← mk_toNat_eq_card,

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ toNat (lift.{u, v} #ι) = toNat #ι
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
M η : Type u
inst✝³ : Fintype η
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M

Tactic:
rank_pi,

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
M η : Type u
inst✝³ : Fintype η
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ (sum fun i ↦ Module.rank R M) = ↑(Fintype.card η) * Module.rank R M
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
η : Type u₁'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Fintype η
⊢ Module.rank R (η → M) = ↑(Fintype.card η) * lift.{u₁', v} (Module.rank R M)

Tactic:
rank_pi,

Goal state after:
R : Type u
M : Type v
η : Type u₁'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Fintype η
⊢ (sum fun i ↦ Module.rank R M) = ↑(Fintype.card η) * lift.{u₁', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : lift.{?u.64, v} (Module.rank R ↥(span R (range b))) = lift.{?u.64, v} #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
mk_range_eq_of_injective hb.injective,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this

Goal state after: