mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ a ∈ s.toFinset ↔ count a s ≠ 0

Tactic:
by simp

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NonAssocSemiring α
inst✝¹ : NonAssocSemiring β
inst✝ : NonAssocSemiring γ
f : α →+* β
⊢ map 1 ⇑f = 1

Tactic:
by simp

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n✝ : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
α : Type u_14
inst✝² : MulOne α
inst✝¹ : AddCommMonoid α
inst✝ : IsStablyFiniteRing α
n : ℕ
⊢ RingEquiv.mopMatrix 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : DecidableEq α
n : ℕ
⊢ ∀ (a : Multiset α), a.card = n ↔ ((Multiset.toFinsupp.toEquiv a).sum fun x ↦ id) = n

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : { P // ∑ i, P i = n }
⊢ ↑((equivNatSumOfFintype α n).symm P) = ∑ a, ↑P a • {a}

Tactic:
obtain ⟨P, hP⟩ := P
  change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _
  ext a
  rw [Multiset.count_sum]
  simp [Multiset.count_singleton]

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
⊢ finrank F K * finrank K A = finrank F A

Tactic:
simp_rw [finrank]
  rw [← toNat_lift.{w} (Module.rank F K), ← toNat_lift.{v} (Module.rank K A), ← toNat_mul,
    lift_rank_mul_lift_rank, toNat_lift]

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
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ lift.{u, v} ℵ₀ ≤ lift.{v, u} #R

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsSimpleRing R
⊢ Nontrivial R

Tactic:
obtain ⟨x, _, hx⟩ := SetLike.exists_of_lt (bot_lt_top : (⊥ : TwoSidedIdeal R) < ⊤)
  use x, 0, hx

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

Goal state before:
pp: ι₁ ι₂ : Type v
inst✝² : DecidableEq ι₂
f : ι₁ → ι₂
β : ι₁ → Type w
inst✝¹ : (i : ι₁) → AddCommMonoid (β i)
inst✝ : DecidableEq ι₁
i : ι₁
x : β i
h : (y : ι₂) × { x // f x = y } ≃ ι₁ := Equiv.sigmaFiberEquiv f
k : (j : ι₂) × { i₁ // f i₁ = j } := ⟨f i, ⟨i, ⋯⟩⟩
⊢ sigmaCurry ((of (fun k ↦ β ↑k.snd) k) x) =
    (of (fun i ↦ ⨁ (j : { i_1 // f i_1 = i }), β ↑j) k.fst) ((of (fun i ↦ β ↑i) k.snd) x)

Tactic:
by simp

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
S : Set (Subalgebra R A)
⊢ ↑(Subalgebra.toSubmodule (sInf S)) = ↑(sInf (⇑Subalgebra.toSubmodule '' S))

Tactic:
by simp

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
S : Set (Subalgebra R A)
⊢ ↑(sInf S).toSubsemiring = ↑(sInf (Subalgebra.toSubsemiring '' S))

Tactic:
by simp

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
⊢ ↑(toSubmodule (⨅ i, S i)) = ↑(⨅ i, toSubmodule (S i))

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
r : R
⊢ 1 * (algebraMap R S) r ∈ s

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ ↑⟨(algebraMap R A) 1, ⋯⟩ = ↑1

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x✝¹ x✝ : R
⊢ ↑⟨(algebraMap R A) (x✝¹ * x✝), ⋯⟩ = ↑(⟨(algebraMap R A) x✝¹, ⋯⟩ * ⟨(algebraMap R A) x✝, ⋯⟩)

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
⊢ ↑⟨(algebraMap R A) 0, ⋯⟩ = ↑0

Tactic:
by simp

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

Goal state before:
pp: S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : SetLike S A
inst✝ : SubsemiringClass S A
hSR : SMulMemClass S R A
s : S
x✝¹ x✝ : R
⊢ ↑⟨(algebraMap R A) (x✝¹ + x✝), ⋯⟩ = ↑(⟨(algebraMap R A) x✝¹, ⋯⟩ + ⟨(algebraMap R A) x✝, ⋯⟩)

Tactic:
by simp

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

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

Tactic:
← Set.image_univ,

Goal state after:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ sSup (A '' Set.univ) = sSup {A i, A j}
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
φ : A →ₐ[R] B
⊢ φ.range.val.comp φ.rangeRestrict = φ

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup (Set.range A) = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
← Set.image_univ,

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ iSupIndep A ∧ sSup (A '' Set.univ) = ⊤ ↔ IsCompl (A i) (A j)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i : ℤ
⊢ (algebraMap ℤ R) 0 ∈ S.carrier

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ y ∈ span R ↑(Subsemigroup.closure s), 0 * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ x ∈ span R ↑(Subsemigroup.closure s), x * 0 ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
⊢ S.toSubmodule = ⊤ ↔ S = ⊤

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toSubmodule = ↑(sInf (NonUnitalSubalgebra.toSubmodule '' S))

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
⊢ ↑(sInf S).toNonUnitalSubsemiring = ↑(sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S))

Tactic:
by simp

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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i).toSubmodule = ↑(⨅ i, (S i).toSubmodule)

Tactic:
by simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
let ⟨k, hik, hjk⟩ := dir i j

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩
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
x✝ : M
⊢ (lift (LinearMap.lsmul R M) ∘ₗ (mk R R M) 1) x✝ = LinearMap.id x✝

Tactic:
by simp

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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)
⊢ ∀ (i : ι), (f i) 0 = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S A
s t : Set A
α : Type u_1
x : A
⊢ ∀ x_1 ∈ {x}, ∀ y ∈ {x}, x_1 * y = y * x_1

Tactic:
by simp

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
x : A
⊢ ∀ x_1 ∈ {x}, ∀ y ∈ {x}, x_1 * y = y * x_1

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (i, PUnit.unit) = (Equiv.prodUnique ι₁ Unit).symm i

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ p i = 0 → (Finsupp.single i (0 ⊗ₜ[R] n)) i = 0

Tactic:
by simp

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
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
x : P
⊢ (linearCombination R id) (Finsupp.single x 1) = x

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ p i = 0 → (Finsupp.single i (m ⊗ₜ[R] 0)) i = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ p i = 0 → (Finsupp.single i (0 • n)) i = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : Algebra R S
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ p i = 0 → (Finsupp.single i (0 • m)) i = 0

Tactic:
by simp

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
x : M₁'
i : ι₂
y : M₂ i
⊢ (PUnit.unit, i) = (Equiv.uniqueProd ι₂ Unit).symm i

Tactic:
by simp

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

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)
H : Projective R (⨁ (i : ι), M i)
i : ι
⊢ component R ι M i ∘ₗ lof R ι M i = LinearMap.id

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : ↥(selfAdjoint R)
⊢ IsSelfAdjoint ↑x

Tactic:
by simp [isSelfAdjoint_iff]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : StarAddMonoid A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : StarAddMonoid B
⊢ ∀ (a : A), (NonUnitalRingHom.toMulHom 0).toFun (star a) = star ((NonUnitalRingHom.toMulHom 0).toFun a)

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : InvolutiveStar α
M : Matrix m n α
⊢ ∀ (i : m) (j : n), Mᴴᴴ i j = M i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
⊢ ∀ (i : n) (j : m), 0ᴴ i j = 0 i j

Tactic:
by simp

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
⊢ M = map 1 star ↔ M = 1

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M + N)ᴴ i j = (Mᴴ + Nᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M - N)ᴴ i j = (Mᴴ - Nᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module ℚ α
c : ℚ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (c • M)ᴴ i j = (c • Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (-M)ᴴ i j = (-Mᴴ) i j

Tactic:
by simp

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

Goal state before:
pp: l : Type u_14
m : Type u_15
n : Type u_16
o : Type u_17
α : Type u_18
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D).submatrix Sum.swap Sum.swap = fromBlocks D C B A

Tactic:
by simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ (M.map star)ᵀ.updateCol i (star b) = ((M.updateRow i b).map star)ᵀ

Tactic:
updateCol_transpose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.updateRow i b).map star)ᵀ
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
⊢ (blockDiagonal' M).map f = blockDiagonal' fun k ↦ (M k).map f

Tactic:
ext
  simp only [map_apply, blockDiagonal'_apply]
  rw [apply_dite f, hf]

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

Goal state before:
pp: α : Type u
n : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w

Tactic:
by simp

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

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : StarAddMonoid A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : StarAddMonoid B
⊢ ∀ (a : A),
    (NonUnitalAlgHom.toDistribMulActionHom 0).toFun (star a) = star ((NonUnitalAlgHom.toDistribMulActionHom 0).toFun a)

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
⊢ LinearEquiv.baseChange R A M M (f ^ n) = LinearEquiv.baseChange R A M M f ^ n

Tactic:
induction n with
  | zero => simp
  | succ n h =>
    simp [pow_succ, LinearEquiv.baseChange_mul, h]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
x : M
hx : x ∈ {p | p ∈ Submonoid.closure S ∧ Irreducible p}
⊢ Irreducible 1 → 1 ∈ S

Tactic:
by simp

Goal state after: