mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x + 1

Tactic:
suffices p'.length ≤ height p'.last by
      simpa [p', hlast'] using! this

Goal state after:
α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithBot α)
hlast : RelSeries.last p = ↑x
hlenpos : p.length ≠ 0
p' : LTSeries α :=
  { length := p.length - 1,
    toFun := fun x ↦
      match x with
      | ⟨i, hi⟩ => (p.toFun ⟨i + 1, ⋯⟩).unbot ⋯,
    step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p'.length ≤ height (RelSeries.last p')
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M ⊗[R] N
x : M
y : N
⊢ -x ⊗ₜ[R] y + x ⊗ₜ[R] y = 0

Tactic:
convert! (add_tmul (R := R) (-x) x y).symm

Goal state after:
case e'_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M ⊗[R] N
x : M
y : N
⊢ 0 = (-x + x) ⊗ₜ[R] y
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t : M ⊗[R] N
⊢ ∀ (x y : M ⊗[R] N),
    x ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → x + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
intro t₁

Goal state after:
case refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
t t₁ : M ⊗[R] N
⊢ ∀ (y : M ⊗[R] N),
    t₁ ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} →
      y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} → t₁ + y ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: case base
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
⊢ ↑1 = 1

Tactic:
| base =>

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 * t ∈ ⨆ i, S i * T

Tactic:
simp_rw [zero_mul]

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_4
S : ι → AddSubmonoid R
T : AddSubmonoid R
s : R
hs : s ∈ ⨆ i, S i
t : R
ht : t ∈ T
⊢ 0 ∈ ⨆ i, S i * T
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : ℤ
h : IsCoprime a b
⊢ IsCoprime ↑a ↑b

Tactic:
rcases h with ⟨u, v, H⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ IsCoprime ↑a ↑b
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
rw [mul_comm] at h
  exact h.of_add_mul_left_left

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

Goal state before:
pp: case cons
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)
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := fun x hx ↦ by
      rw [mem_sdiff, mem_singleton]
      exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩

Goal state after:
case cons
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}
⊢ (∃ μ, ∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j = 1) ↔
    Pairwise (IsCoprime on fun a ↦ s ↑a) ∧ ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥ by
    obtain ⟨n, w⟩ := t
    use n + 1
    rintro (_ | m) p
    · cases p
    · apply w
      exact Nat.succ_le_succ_iff.mp p
  obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)
  refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
  simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0

Tactic:
by
    simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
m x : M
hx : x ∈ I • (R ∙ m)
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ (y1 + y2) • m = m1 + m2

Tactic:
rw [add_smul, hy1, hy2]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
r : R
hr : r ∈ Ideal.span S
m : M
hm : m ∈ span R T
⊢ r • m ∈ span R (S • T)

Tactic:
revert r

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
S : Set R
T : Set M
inst✝ : (Ideal.span S).IsTwoSided
m : M
hm : m ∈ span R T
⊢ ∀ r ∈ Ideal.span S, r • m ∈ span R (S • T)
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
f : F
r : R
⊢ r ∈ ker f ↔ f r = 0

Tactic:
rw [ker, Ideal.mem_comap, Submodule.mem_bot]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ ∀ (m : M), (r - s) • m = 0

Tactic:
by simp only [sub_smul, H', sub_self, implies_true]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ n * I ^ (m + 1) ≤ I ^ (m + 1)

Tactic:
exact mul_le_right

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

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f (c - a * b) = 0
⊢ a * b ∈ I

Tactic:
convert! I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f (c - a * b) = 0
⊢ a * b = c - (c - a * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
⊢ (d₁ * d₂) ^ k = d₁ ^ k * d₂ ^ k

Tactic:
exact mul_pow d₁ d₂ k

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
have h3 : d₁ ^ k ∣ a := by
    apply (dvd_gcd_mul_of_dvd_mul h2).trans
    rw [h1.mul_left_dvd]

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
h3 : d₁ ^ k ∣ a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ a ∣ normalize (Classical.choose ⋯)

Tactic:
rw [dvd_normalize_iff, ← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b c : α
ac : a ∣ c
ab : a ∣ b
h : ¬c = 0
h_1 : ¬b = 0
h0 : lcm c b ≠ 0
⊢ lcm c b * a ∣ c * b
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✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
⊢ #κ ≤ #ι

Tactic:
by_contra h
  rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
  let Φ := fun k : κ => (b.repr (v k)).support
  obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber' Φ h
  let v' := fun k : Φ ⁻¹' {s} => v k
  have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
  have w' : Finite (Φ ⁻¹' {s}) := by
    apply i'.finite_of_le_span_finite v' (s.image b)
    rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
    simp only [SetLike.mem_coe, Finset.coe_image]
    apply Basis.mem_span_repr_support
  exact w.false

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

Goal state before:
pp: case neg.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
hp : ∀ i ∈ ∅, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ∅
has : a ∉ ∅
hbs : b ∉ ∅
⊢ ∃ i ∈ ∅, I ≤ f i

Tactic:
exact (h I.zero_mem).elim

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
classical
    by_cases has : a ∈ s
    · obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
    · by_cases hbs : b ∈ s
      · obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
      rcases s.eq_empty_or_nonempty with rfl | hsne
      · rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim
      · obtain ⟨i, his⟩ := hsne
        obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

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

Goal state before:
pp: 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 k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (single i j c * single k l d) a b = 0 a b

Tactic:
simp only [mul_apply, single, of_apply]

Goal state after:
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 k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
⊢ (∑ j_1, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = 0 a b
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
cases nonempty_fintype ι₁

Goal state after:
case intro
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
val✝ : Fintype ι₁
⊢ Module.Finite R (Matrix ι₁ ι₂ M)
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    (Multiset.map (fun b ↦ Multiset.count a (↑⟨P, hP⟩ b • {b})) univ.val).sum

Tactic:
simp [Multiset.count_singleton]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : OrzechProperty R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
h : finrank R M ≤ finrank R M'
h✝ : Subsingleton R
⊢ Bijective ⇑f

Tactic:
have := Module.subsingleton R M
    exact ⟨Function.injective_of_subsingleton f, hf⟩

Goal state after:
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
s : NonUnitalSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
by
  simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

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 : Subalgebra R A
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (mk R M R).compr₂ₛₗ ↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) =
    (mk R M R).compr₂ₛₗ ↑(TensorProduct.rid R M)

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (mk R R M).compr₂ₛₗ ↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) =
    (mk R R M).compr₂ₛₗ ↑(TensorProduct.lid R M)

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
      lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) =
    LinearMap.id

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
      lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) =
    LinearMap.id

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
⊢ lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) =
    LinearMap.id

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
⊢ lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) =
    LinearMap.id

Tactic:
by ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
⊢ x * r • a = r • a * x

Tactic:
rw [mul_smul_comm, smul_mul_assoc, ha x hx]

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = (↑q.den)⁻¹ * ↑q.num

Tactic:
Int.commute_cast,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
q : ℚ
⊢ ↑q.num / ↑q.den = ↑q.num * (↑q.den)⁻¹
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (star ↑u)⁻¹ʳ = star ↑u⁻¹

Tactic:
← Units.coe_star,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (↑(star u))⁻¹ʳ = star ↑u⁻¹
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
hx : IsSelfAdjoint x
⊢ ↑((skewAdjointPart R) x) = ↑0

Tactic:
by
  rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]

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

Goal state before:
pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (blockDiagonal fun x ↦ diagonal fun x ↦ 1) = diagonal fun x ↦ 1

Tactic:
rw [blockDiagonal_diagonal]

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
      lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) =
    LinearMap.id

Tactic:
by ext; rfl

Goal state after: