mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, iInf_eq_bot.2, bot_eq_zero]
    exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x.toList

Tactic:
simp_rw [List.isChain_iff_getElem, length_toList, add_lt_add_iff_right]

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ ∀ (i : ℕ) (_hi : i < x.length), (x.toList[i], x.toList[i + 1]) ∈ r
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ (s.toFun 0, s.toFun 0) ∈ r

Tactic:
nth_rw 2 [rid]

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ (s.toFun 0, s.toFun 1) ∈ r
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
use p.drop ⟨m-n, by lia⟩

Goal state after:
case h
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).last = a ∧ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ ¬Subsingleton α

Tactic:
← Order.krullDim_eq_zero_iff_of_orderTop,

Goal state after:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ ¬krullDim α = 0
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
⊢ a + b + c = b + c

Tactic:
hab

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
⊢ b + c = b + c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ = a∗

Tactic:
have h : 1 + a * a∗ ≤ a∗ := by
    rw [add_le_iff]
    exact ⟨one_le_kstar, mul_kstar_le_kstar⟩

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
⊢ 1 + a * a∗ = a∗
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: case refine_2.inr
m : ℕ
⊢ IsCoprime m 1

Tactic:
· exact isCoprime_one_right

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
h : ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ t, s i) x

Tactic:
by
  induction t using Finset.cons_induction with
  | empty => apply isCoprime_one_left
  | cons b t hbt ih =>
    rw [Finset.prod_cons]
    rw [Finset.forall_mem_cons] at h
    exact h.1.mul_left (ih h.2)

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

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : op m ∈ map (↑(opLinearEquiv R)) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R)) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R)) (M * N)

Tactic:
rw [Submodule.mem_map_equiv] at hm hn ⊢

Goal state after:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
m : A
hm : (opLinearEquiv R).symm (op m) ∈ N
n : A
hn : (opLinearEquiv R).symm (op n) ∈ M
⊢ (opLinearEquiv R).symm (op m * op n) ∈ M * N
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (fun i ↦ if i = a then u else v * μ i) a * ∏ j ∈ t, s j +
      ∑ x ∈ t, (fun i ↦ if i = a then u else v * μ i) x * ∏ j ∈ insert a t \ {x}, s j =
    1

Tactic:
simp only [↓reduceIte, ite_mul]

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝ : Field K
a b : K
⊢ b * (a / b) + (a - a * b / b) = a

Tactic:
by_cases h : b = 0

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
a b : K
h : b = 0
⊢ b * (a / b) + (a - a * b / b) = a

case neg
K : Type u_1
inst✝ : Field K
a b : K
h : ¬b = 0
⊢ b * (a / b) + (a - a * b / b) = a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x = f 0
⊢ x ∈ ⊥

Tactic:
exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
I✝ J : Ideal R
K✝ L : Ideal S
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective ⇑f
I : Ideal R
K x✝¹ x✝ : Ideal S
h :
  { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
    { toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝
this :
  map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝¹) ≤
    map f ({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } x✝)
⊢ x✝¹ ≤ x✝

Tactic:
simpa only [Equiv.coe_fn_mk, map_comap_of_surjective f hf.2] using this

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ 1 ∉ ker f

Tactic:
rw [mem_ker, map_one]

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
rcf : RingHomClass F R S
inst✝ : Nontrivial S
f : F
⊢ ¬1 = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
M' : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
⊢ map f (r • N) = r • map f N

Tactic:
by
  simp_rw [← ideal_span_singleton_smul, map_smul'']

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ (I ^ x✝¹.succ).IsTwoSided

Tactic:
by rw [Submodule.pow_succ]; infer_instance

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case neg
z : ℤ
hz : normalize z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
rw [normalize_of_nonpos h.le] at hz

Goal state after:
case neg
z : ℤ
hz : -z = z
h : z < 0
⊢ 0 ≤ z
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : j.IsPrime
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

Tactic:
have : j.IsPrime := hj'

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : j.IsPrime
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case neg.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * if hb : b ∈ s then g' hb else 0

Tactic:
dif_pos hb,

Goal state after:
case neg.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * g' hb
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this : Nontrivial R
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
have := basis_finite_of_finite_spans w.toFinite s b

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : RankCondition R
ι : Type u_2
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
this✝ : Nontrivial R
this : Finite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
j : n
⊢ (diagonal d).row j = Pi.single j (d j)

Tactic:
ext
  simp +contextual [diagonal, eq_comm, Pi.single_apply]

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

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) :=
    (congrArg _ heq).to_iff

Goal state after:
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)
hmem_union : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ↑I ⊆ ⋃ i ∈ ↑t, ↑(f i)
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext i
  simp [vecMul, dotProduct, vecMulVec, Finset.sum_mul, mul_assoc]

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

Goal state before:
pp: case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
⊢ (scalar n) (M i i) j k = M j k

Tactic:
simp only [scalar_apply]

Goal state after:
case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
⊢ diagonal (fun x ↦ M i i) j k = M j k
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = submatrix 1 ⇑e.symm ⇑e.symm ↔ B * A = 1

Tactic:
submatrix_one_equiv,

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = 1 ↔ B * A = 1
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
⊢ ∃! c, u = c • LinearMap.id

Tactic:
let e := (nonempty_linearEquiv_of_finrank_eq_one d1).some
  set c := e.symm (u (e 1)) with hc
  suffices u = c • LinearMap.id by
    use c
    simp only [this, true_and]
    intro d hcd
    rw [LinearMap.ext_iff] at hcd
    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm
  ext x
  have (x : M) : x = (e.symm x) • (e 1) := by simp [← LinearEquiv.map_smul]
  rw [this x]
  simp only [hc, map_smul, LinearMap.smul_apply, LinearMap.id_coe, id_eq]
  rw [← this]

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

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
f : A →ₐ[R] B
⊢ Subalgebra.toSubmodule (Subalgebra.map f ⊥) = Subalgebra.toSubmodule ⊥

Tactic:
simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
← mem_toSubsemiring,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S.toSubsemiring ↔ x ∈ T
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S.toSubsemiring ↔ x ∈ T

Tactic:
← mem_toSubsemiring,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
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:
by
    rw [← one_smul R s, ← smul_assoc, one_smul, ← one_smul R (s • t), ← smul_assoc,
      Algebra.smul_def, Algebra.smul_def]
    apply mul_assoc

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
⊢ Commute (r • a) b

Tactic:
rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Projective R P

Tactic:
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
  intro m
  simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
    map_finsuppSum]
  exact b.linearCombination_repr m

Goal state after:
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:
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]

Goal state after:
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
⊢ (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0) = (if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
obtain rfl | hj := eq_or_ne j' j

Goal state after:
case inl
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
r : m → α
j' : n
⊢ (v ᵥ* B.updateCol j' r) j' = Function.update (v ᵥ* B) j' (v ⬝ᵥ r) j'

case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'

Tactic:
obtain rfl | hj := eq_or_ne j' j

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
c : m → α
i' : l
j' : n
⊢ (A * B.updateCol j' c) i' j' = (A * B).updateCol j' (A *ᵥ c) i' j'

case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
B : Matrix m n α
j : n
c : m → α
i' : l
j' : n
hj : j' ≠ j
⊢ (A * B.updateCol j c) i' j' = (A * B).updateCol j (A *ᵥ c) i' j'
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✝⁵ : 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₂
inst✝ : Finite m
f : M₁ →ₗ[R] R
x : M₂
i : m
j : n
⊢ (toMatrix v₁ v₂) (f.smulRight x) i j = vecMulVec (⇑(v₂.repr x)) (⇑f ∘ ⇑v₁) i j

Tactic:
simpa [toMatrix_apply, vecMulVec_apply] using mul_comm _ _

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✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
t : R
s : ↥S
ht : t * ↑s ∈ S
⊢ -r /ₒ s = t • -r /ₒ ⟨t * ↑s, ht⟩

Tactic:
← OreLocalization.expand

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
t : R
s : ↥S
ht : t * ↑s ∈ S
⊢ -r /ₒ s = -r /ₒ s
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₁
M : Matrix n n R
v : M₁
⊢ v₁.equivFun.symm ((toLinAlgEquiv' M) ⇑(v₁.repr v)) = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j

Tactic:
Matrix.toLinAlgEquiv'_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₁
M : Matrix n n R
v : M₁
⊢ v₁.equivFun.symm (M *ᵥ ⇑(v₁.repr v)) = ∑ j, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j
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
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) = blockDiagonal fun x_1 ↦ (leftMulMatrix b) x

Tactic:
by
  ext ⟨i, k⟩ ⟨j, k'⟩
  rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
  split_ifs with h <;> simp only at h <;> simp

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
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = snf.a i • c i

Tactic:
snf.snf,

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
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr (snf.a a • snf.bM (snf.f a))) (snf.f i) = snf.a i • c i
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 y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) m

Tactic:
← one_mul m

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 y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case mpr
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
hM : M ≤ nonZeroDivisors R
h : x = 0
⊢ (algebraMap R S) x = 0

Tactic:
· rw [h, map_zero]

Goal state after: