mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case neg.inr
ι : 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 ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f i ∨ ∃ x ∈ t, I ≤ f x

Tactic:
]

Goal state after:
case neg.inr
ι : 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 ≤ f i ∨ ∃ i ∈ t, I ≤ f i
has : a ∉ insert i t
hbs : b ∉ insert i t
his : i ∈ insert i t
hp' : ∀ j ∈ t, (f j).IsPrime
⊢ I ≤ f i ∨ ∃ x ∈ t, I ≤ f x
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:
]

Goal state after:
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
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
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 : α
j' : m
hj : g.symm j ≠ j'
⊢ 0 = 0

pp: case inr.inl.hj
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 : α
j' : m
hj : g.symm j ≠ j'
⊢ j ≠ g j'

Tactic:
]

Goal state after:
case inr.inl.hj
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 : α
j' : m
hj : g.symm j ≠ j'
⊢ j ≠ g j'
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:
]

Goal state after:
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
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
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d : n → α
M : Matrix m n α
i : m
j : n
⊢ (M * (diagonal d)ᵀ) i j = M i j * d j
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)
hmem_union : ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ↑I ⊆ ⋃ i ∈ ↑t, ↑(f i)
⊢ (∃ i ∈ t, I ≤ f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
]

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 ∈ t, I ≤ 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✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M i✝ j✝ = M i✝ j✝

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M i✝ j✝ = M i✝ j✝

Tactic:
]

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ M ∈ S

Tactic:
‹M.IsMaximal›.eq_of_le _ le

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ∈ S

R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ≠ ⊤
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ single j j (f j) j k = if j = k then f j else 0

pp: case h₀
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ ∀ b ∈ Finset.univ, b ≠ j → single b b (f b) j k = 0

pp: case h₁
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ j ∉ Finset.univ → single j j (f j) j k = 0

Tactic:
]

Goal state after:
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ single j j (f j) j k = if j = k then f j else 0

case h₀
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ ∀ b ∈ Finset.univ, b ≠ j → single b b (f b) j k = 0

case h₁
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ j ∉ Finset.univ → single j j (f j) j k = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ∈ S

pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ≠ ⊤

Tactic:
]

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ∈ S

R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
hp : ∀ I ∈ S, I ≠ a → I ≠ b → I.IsPrime
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
⊢ I ≠ ⊤
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✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
i : m
j : n
⊢ (∑ x_1, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j = of x i j

Tactic:
]

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
i : m
j : n
⊢ (∑ x_1, single x_1.1 x_1.2 (x x_1.1 x_1.2)) i j = of x i j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M M' : Matrix m n α
N : Matrix n o α
⊢ M * N + -(M' * N) = M * N + -(M' * N)

Tactic:
]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * N + -(M * N') = M * N + -(M * N')

Tactic:
]

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

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ ∑ j_1, (A ^ m) i j_1 * A j_1 j

Tactic:
]

Goal state after:
case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ ∑ j_1, (A ^ m) i j_1 * A j_1 j
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, single x.1 x.2 (M x.1 x.2))

Tactic:
]

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, single x.1 x.2 (M x.1 x.2))
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
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ y * x + i * 1 = 1

Tactic:
]

Goal state after:
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
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ y * x + i * 1 = 1
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f (∑ i, ∑ j, single i j (x i j)) = g (∑ i, ∑ j, single i j (x i j))

Tactic:
]

Goal state after:
case intro.intro
m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
val✝¹ : Fintype m
val✝ : Fintype n
x : Matrix m n α
⊢ f (∑ i, ∑ j, single i j (x i j)) = g (∑ i, ∑ j, single i j (x i j))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∉ I → b ∈ I ^ n

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∉ I → b ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ b ∈ I ^ n

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ b ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case pos
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single j j c).diag j = Pi.single j c j

Tactic:
]

Goal state after:
case pos
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
hij : i = j
⊢ (single j j c).diag j = Pi.single j c j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
]

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n

Tactic:
]

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ⊤ = ⊤

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (f.sum fun a b ↦ ↑b • v a) = f.sum fun i x ↦ ↑x • v i

pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∑ i, ↑(f i) • v i = ∑ i, ↑(f i) • v i

pp: case h
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0

Tactic:
]

Goal state after:
case h
ι : Type u_1
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
v : ι → M
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ (finsuppTotal ι M I v).range ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • v i) = x✝

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
x✝ : M
⊢ x✝ ∈ (finsuppTotal ι M I v).range ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c ↦ c • v i) = x✝
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0

Tactic:
]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i

Tactic:
]

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ v i * Pi.single j x i = Pi.single j (v j * x) i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i : ι
a✝ : i ∈ a.support
⊢ ↑⟨a i, ⋯⟩ • v i = a i • v i

Tactic:
]

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i

Tactic:
]

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ Pi.single j x i * v i = Pi.single j (x * v j) i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ ¬r = 0 ↔ r ≠ 0

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ ¬r = 0 ↔ r ≠ 0

Tactic:
]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j

Tactic:
]

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
A B C : Matrix n n α
i j : n
⊢ (A * (B * C)) i j = A i ⬝ᵥ B *ᵥ Cᵀ j
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
s : Set R
N : Submodule R M
⊢ s • N = s • N

Tactic:
]

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
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ R ∙ 1 = R ∙ 1

Tactic:
]

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✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ (algebraMap R A) r * a ∈
    { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ (algebraMap R A) r * a ∈
    { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M
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✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ r • a ∈ I • M

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ r • a ∈ I • M
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
I : Ideal R
f : M →ₗ[R] N
h : Function.Surjective ⇑f
⊢ comap f (I • ⊤) = comap f (I • ⊤)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
⊢ ∀ (y : ↑s), a y ∈ ↑I

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Set R
I J : Ideal R
m : ↑s → ℕ
a b : ↑s → R
ha : ∀ (z : ↑s), a z ∈ I
hb : ∀ (z : ↑s), b z ∈ J
heq : ∀ (z : ↑s), a z + b z = ↑z ^ m z
⊢ ∀ (y : ↑s), a y ∈ ↑I
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ Finite ↑⋯.choose

Tactic:
]

Goal state after:
case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ Finite ↑⋯.choose
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective
    ⇑(↑R (linearCombination S c) ∘ₗ mapRange.linearMap (linearCombination R b) ∘ₗ ↑(curryLinearEquiv R))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
b : ι → S
ι' : Type u_6
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ Function.Injective
    ⇑(↑R (linearCombination S c) ∘ₗ mapRange.linearMap (linearCombination R b) ∘ₗ ↑(curryLinearEquiv R))