mathlib-initiative/mathlib-tactics huggingface dataset:
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

pp: case inr
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' : n
h : i ≠ i'
⊢ (∑ i_1, if i = i' ∧ j = i_1 then c * x i_1 else 0) = Function.update 0 i (c * x j) i'

Tactic:
·

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

Goal state before:
pp: n : Type u_3
α : Type u_10
inst✝² : NonUnitalNonAssocCommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ Commute (diagonal d₁) (diagonal d₂)

Tactic:
simp_rw [commute_iff_eq, diagonal_mul_diagonal, mul_comm]

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
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x

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
⊢ z * i * x + i * i ^ n + y * x = 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
⊢ (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x
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
⊢ z * i * x + i * i ^ n + y * x = 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
⊢ z * i * x + i * i ^ n + y * x = 1
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
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (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
⊢ ∀ x ∈ Finset.univ ×ˢ Finset.univ, P (single x.1 x.2 (M x.1 x.2))
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✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ i, (v ᵥ* A) i * w i = ∑ j, ∑ i, v i * A i j * w j

Tactic:
vecMul_eq_sum,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x, (∑ i, v i • A i) x * w x = ∑ j, ∑ i, v i * A i j * w j
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✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
b : n
M : Matrix m n α
⊢ (single i j c * M) i b = c * M j b

Tactic:
simp [mul_apply, single]

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 m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
M : Matrix l m α
⊢ (M * single i j c) a j = M a i * c

Tactic:
simp [mul_apply, single]

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
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
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 : ι), ↑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 : ι), ↑0 • v a = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Subsingleton R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Subsingleton R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
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
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

pp: case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec

Tactic:
·

Goal state after:
case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsLeftRegular A ↔ Function.Injective A.mulVec
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

pp: case inr
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : Nonempty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
·

Goal state after:
case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case inl
m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
h✝ : IsEmpty m
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
simp [IsRightRegular, Function.injective_of_subsingleton]

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

Goal state before:
pp: case pos
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
h₁ : i = a
⊢ (∑ 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

pp: case neg
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
h₁ : ¬i = a
⊢ (∑ 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

Tactic:
·

Goal state after:
case pos
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
h₁ : i = a
⊢ (∑ 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.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ A *ᵥ 1 = ∑ j, Aᵀ j

Tactic:
by
  ext; simp [mulVec, dotProduct]

Goal state after:
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
⊢ Finite (ChooseBasisIndex R M)

pp: case inr
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✝ : Nontrivial R
⊢ Finite (ChooseBasisIndex R M)

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
⊢ Finite (ChooseBasisIndex R M)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case inr
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✝ : Nontrivial R
⊢ Finite (ChooseBasisIndex R M)

Tactic:
·

Goal state after:
case inr
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✝ : Nontrivial R
⊢ Finite (ChooseBasisIndex R M)
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case neg
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
h₁ : ¬i = a
⊢ (∑ 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

Tactic:
·

Goal state after:
case neg
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
h₁ : ¬i = a
⊢ (∑ 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.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 : α
⊢ single i j c * single k l d = 0

Tactic:
by
  ext a b
  simp only [mul_apply, single, of_apply]
  by_cases h₁ : i = a
  · simp [h₁, h, Finset.sum_eq_zero]
  · simp [h₁]

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

Goal state before:
pp: case inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : IsEmpty n
⊢ M ∈ Set.range ⇑(scalar n)

pp: case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
·

Goal state after:
case inl
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : IsEmpty n
⊢ M ∈ Set.range ⇑(scalar n)
Module: Mathlib.Data.Matrix.Basis

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

pp: case inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
⊢ diagonal (fun x ↦ M i i) j k = M j k

Tactic:
·

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

Goal state before:
pp: case pos
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ (b.repr (b i • 1)) i' = (single (i, j) 1) (i', j')

pp: case neg
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')

Tactic:
·

Goal state after:
case pos
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ (b.repr (b i • 1)) i' = (single (i, j) 1) (i', j')
Module: Mathlib.Data.Matrix.Basis

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

pp: case inr.inl.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
·

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

Goal state before:
pp: case neg
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')

Tactic:
·

Goal state after:
case neg
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
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')
Module: Mathlib.Data.Matrix.Basis

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

Tactic:
·

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

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

Tactic:
·

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

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

pp: case inr.inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
⊢ 0 = M j k

Tactic:
·

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

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

Tactic:
·

Goal state after:
case inr.inr.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
hkl : j ≠ k
hij : i ≠ j
⊢ 0 = M j k
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
h : s.card = 0
⊢ False
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.card ≠ 0 ∧ s = s.card • {a}
⊢ s.toFinset = {a}

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
⊢ count x s = count x (s.card • {a})
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
⊢ count x s = s.card * if x = a then 1 else 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : x = a
⊢ count x s = s.card * if x = a then 1 else 0
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun i ↦ f i + a

pp: case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ f i + a) ≤ s.sup' hs f + a

Tactic:
·

Goal state after:
case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f + a ≤ s.sup' hs fun i ↦ f i + a
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case a.h
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i ↦ f i + a

pp: case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a

Tactic:
·

Goal state after:
case a.h
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i ↦ f i + a
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a

Tactic:
·

Goal state after:
case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ f i + a) ≤ s.sup' hs f + a

Tactic:
·

Goal state after:
case a
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ f i + a) ≤ s.sup' hs f + a