mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ i ∉ Finset.univ → diagonal v i i * w i = 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v i * w i = v i * diagonal w i i

Tactic:
simp

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

Goal state before:
pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ i ∉ Finset.univ → v i * diagonal w i i = 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ v i * w i = v i * diagonal w i i

Tactic:
simp

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

Goal state before:
pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ i ∉ Finset.univ → v i * diagonal w i i = 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ x * v i = Pi.single i x i * v i

Tactic:
simp

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

Goal state before:
pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ i ∉ Finset.univ → Pi.single i x i * v i = 0

Tactic:
simp

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

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v i * x = v i * Pi.single i x i

Tactic:
simp

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

Goal state before:
pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ i ∉ Finset.univ → v i * Pi.single i x i = 0

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
i✝ : m
j✝ : n
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then 0 else 0) i✝ j✝ = 0 i✝ j✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
⊢ ∀ j ∈ t, (f j).IsPrime

Tactic:
intro j

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
i : ι
t : Finset ι
left✝ : i ∉ t
hp : ∀ i_1 ∈ insert i t, i_1 ≠ a → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
j : ι
⊢ j ∈ t → (f j).IsPrime
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_1
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 0 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 0 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 0 else 0) =
    A 0 0 * B 0 0 + A 0 1 * B 1 0

Tactic:
simp

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

Goal state before:
pp: case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 0 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
simp

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

Goal state before:
pp: case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 0 else 0) +
        if h : 0 < 2 then A 1 ⟨0, h⟩ * B ⟨0, h⟩ 0 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 0 else 0) =
    A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
simp

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

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
⊢ single i j r (f (f.symm i)) (g (g.symm j)) = single (f.symm i) (g.symm j) r (f.symm i) (g.symm j)

Tactic:
simp

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

Goal state before:
pp: case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (((∑ x ∈ Finset.range 0, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
        if h : 0 < 2 then A 1 ⟨0, h⟩ * B ⟨0, h⟩ 1 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
simp

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

Goal state before:
pp: case inl
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ (∑ i_1, if i = i ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = ((diagonal fun x ↦ a) * M) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (MulOpposite.op a • M) i✝ j✝ = (M * diagonal fun x ↦ a) i✝ j✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ 0 * x + i ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
M : Matrix m n α
⊢ ((liftLinear S) f) M = ∑ i, ∑ j, (f i j) (M i j)

Tactic:
by
  simp [liftLinear, map_sum, LinearEquiv.congrLeft]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = M.col j x✝

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M.row i x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (b : Submodule R M), 1 • b = b

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
ι : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective ⇑(algebraMap R A)
c : R
x : M
⊢ (RingEquiv.ofBijective (algebraMap R A) h) c • x = c • x

Tactic:
simp

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝¹ : M ∈ Set.range ⇑(scalar n)
i j : n
x✝ : i ≠ j
r : α
hr : (scalar n) r = M
⊢ r • single i j 1 = MulOpposite.op r • single i j 1

Tactic:
simp

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ r • single i j 1 = MulOpposite.op r • single i j 1

Tactic:
simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix m n R
v : n → R
i : m
⊢ f ((M *ᵥ v) i) = (M.map ⇑f *ᵥ ⇑f ∘ v) i

Tactic:
simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = #β ^ Fintype.card α

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ ℵ₀ ≤ lift.{v, u} #α

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h'
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = max #α #β

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ #(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
rw [mk_finsupp_lift_of_fintype]

Goal state after:
case inl
α : Type u
β : Type v
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
val✝ : Fintype α
⊢ lift.{u, v} #β ^ Fintype.card α = max (lift.{v, u} #α) (lift.{u, v} #β)
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α β : Type u
inst✝² : Nonempty α
inst✝¹ : Zero β
inst✝ : Infinite β
⊢ #(α →₀ β) = max #α #β

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℕ) = max #α ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : IsEmpty α
⊢ #(α →₀ ℕ) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Multiset α) = #α

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x y : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: case pos
n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i : n
⊢ 0 ≤ 1 i i

Tactic:
simp

Goal state after:
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 β
x✝ : α
⊢ x✝ ∈ (fun a ↦ ⟨a, ⋯⟩) ⁻¹' inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' f i ⁻¹' t ↔ x✝ ∈ ⋃ i, Subtype.val '' f i ⁻¹' t

Tactic:
simp

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

Goal state before:
pp: n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal ((algebraMap R (n → α)) r)).map f = diagonal ((algebraMap R (n → β)) r)

Tactic:
diagonal_map hf

Goal state after:
n : Type u_3
R : Type u_7
α : Type u_11
β : Type u_12
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
f : α → β
hf : f 0 = 0
hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r
⊢ (diagonal fun m ↦ f ((algebraMap R (n → α)) r m)) = diagonal ((algebraMap R (n → β)) r)
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:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∪ t)) a✝ = (toFinsupp s ⊔ toFinsupp t) a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∩ t)) a✝ = (toFinsupp s ⊓ toFinsupp t) a✝

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

Tactic:
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.rank R M = 0
⊢ Subsingleton M

Tactic:
by
  rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
  exact (Module.Free.chooseBasis R M).repr.subsingleton

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

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y → I.ringCon (x - y) 0

pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y

Tactic:
· intro h; convert! I.ringCon.sub h (I.ringCon.refl y); abel

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ ↑I ⊆ ↑J ∧ I ≠ J ↔ ↑I ⊆ ↑J ∧ ↑I ≠ ↑J

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i ↦ I i) ↔ x✝ ∈ Set.range fun i ↦ (I i).ringCon

Tactic:
simp

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ Submodule.restrictScalars R 1 ↔ x✝ ∈ toSubmodule S

Tactic:
simp

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ z ∈ Subsemiring.closure (Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ⇑(algebraMap S A) ∪ t)

Tactic:
simp

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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
simp

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
φ : A →ₐ[R] B
⊢ φ.range.val.comp φ.rangeRestrict = φ

Tactic:
simp

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
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑y

Tactic:
convert! Subtype.ext_iff.mp (h 1) using 1 <;> exact (mul_one _).symm

Goal state after:
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:
simp

Goal state after: