awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
simp_rw :
  ∀ (x : R),
    (∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I) →
      ∀ (i j : n) (y : Matrix n n R),
        ∃ (z : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * y * single i j x + z - 1)
⊢ ∀ x ∈ I.jacobson, ∀ (i j : n), Membership.mem (γ := Ideal (Matrix n n R)) (jacobson (matrix n I)) (single i j x)

Tactic:
simp_rw [Ideal.mem_jacobson_iff]

Premises used: Ideal.mem_jacobson_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
have :
  ∀ (z : R) (zMx : z * M q p * x + z - 1 ∈ I),
    ∃ (z : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * M * single p q x + z - 1)
⊢ ∃ (z : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * M * single p q x + z - 1)

Tactic:
have ⟨z, zMx⟩ := xIJ (M q p)
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
h : Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (N * M * single p q x + N - 1)
⊢ ∃ (z : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * M * single p q x + z - 1)

Tactic:
use N
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i j : n
h : HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
h₁ : ∀ (qj : q ≠ j), HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i j ∈ (↑I.toAddSubmonoid : Set R)
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i j ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
obtain rfl | qj := eq_or_ne q j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
pos : ∀ (iq : i = q), HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
neg : ∀ (iq : ¬i = q), HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
by_cases iq : i = q
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
iq : i = q
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
simp [iq, N, zMx, single, mul_apply, sum_apply, ite_and, sub_mul]

Premises used: Matrix.sum_apply, Matrix.mul_apply, sub_mul, ite_and, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
iq : ¬i = q
⊢ -M i p * x * (z * M q p * x + z - 1) ∈ I

Tactic:
I.mul_mem_left (-M i p * x) zMx

Premises used: HMul.hMul, Ideal.mul_mem_left, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
iq : ¬i = q
h : HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q = -M i p * x * (z * M q p * x + z - 1)
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
convert! I.mul_mem_left (-M i p * x) zMx

Premises used: HMul.hMul, Ideal.mul_mem_left, Neg.neg
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
iq : ¬i = q
h : M i p * x - M i p * x * z * M q p * x + -(M i p * x * z) = -(M i p * x * (z * M q p * x + z - 1))
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q = -M i p * x * (z * M q p * x + z - 1)

Tactic:
simp [iq, N, single, mul_apply, sum_apply, ite_and, sub_mul]

Premises used: Matrix.sum_apply, Matrix.mul_apply, sub_mul, ite_and, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i : n
iq : ¬i = q
⊢ M i p * x - M i p * x * z * M q p * x + -(M i p * x * z) = -(M i p * x * (z * M q p * x + z - 1))

Tactic:
simp [sub_add, mul_add, mul_sub, mul_assoc]

Premises used: sub_add, mul_sub, mul_assoc, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := HSub.hSub (α := Matrix n n R) 1 (∑ i : n, single i q (if i = q then 1 - z else M i p * x * z))
i j : n
qj : q ≠ j
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i j ∈ (↑I.toAddSubmonoid : Set R)

Tactic:
simp [N, qj, sum_apply, mul_apply]

Premises used: Matrix.sum_apply, Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
rw :
  Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
    (∑ i : n, ∑ j : n, single i j (M i j))
⊢ Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R)) M

Tactic:
rw [matrix_eq_sum_single M]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
h :
  ∀ (c : n),
    Membership.mem (γ := Finset n) Finset.univ c →
      Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
        (∑ j : n, single c j (M c j))
⊢ Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
    (∑ i : n, ∑ j : n, single i j (M i j))

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
i : n
h :
  Membership.mem (γ := Finset n) Finset.univ i →
    Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
      (∑ j : n, single i j (M i j))
⊢ Membership.mem (γ := Finset n) Finset.univ i →
    Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
      (∑ j : n, single i j (M i j))

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
h :
  ∀ (c : n),
    Membership.mem (γ := Finset n) Finset.univ c →
      Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
        (single i c (M i c))
⊢ Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
    (∑ j : n, single i j (M i j))

Tactic:
apply sum_mem

Premises used: sum_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
i : n
h_1 : Membership.mem (γ := Finset n) Finset.univ i
j : n
h :
  Membership.mem (γ := Finset n) Finset.univ j →
    Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
      (single i j (M i j))
⊢ Membership.mem (γ := Finset n) Finset.univ j →
    Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
      (single i j (M i j))

Tactic:
_
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (matrix n I.jacobson) M
i : n
h : Membership.mem (γ := Finset n) Finset.univ i
j : n
h_1 : Membership.mem (γ := Finset n) Finset.univ j
⊢ Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R))
    (single i j (M i j))

Tactic:
apply single_mem_jacobson_matrix I _ (MI i j)

Premises used: Ideal.single_mem_jacobson_matrix
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
c : RingCon R
M N : Matrix n n R
⊢ (matrix n c : (a : Matrix n n R) → Matrix n n R → Prop) M N ↔ ∀ (i j : n), (c : (a : R) → R → Prop) (M i j) (N i j)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (matrix n c : (a : Matrix n n R) → Matrix n n R → Prop) (Matrix.single i j x) (Matrix.single i j y)
⊢ (c : (a : R) → R → Prop) x y

Tactic:
simpa using h i j
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
refine :
  ∀ (h : (c : (a : R) → R → Prop) x y) (i' j' : n),
    (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')
⊢ (matrix n c : (a : Matrix n n R) → Matrix n n R → Prop) (Matrix.single i j x) (Matrix.single i j y) ↔
    (c : (a : R) → R → Prop) x y

Tactic:
refine ⟨fun h ↦ by simpa using h i j, fun h i' j' ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (c : (a : R) → R → Prop) x y
i' j' : n
inl : ∀ (hi : i ≠ i'), (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')
inr : (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')

Tactic:
obtain hi | rfl := ne_or_eq i i'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (c : (a : R) → R → Prop) x y
i' j' : n
hi : i ≠ i'
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')

Tactic:
simpa [hi] using c.refl 0

Premises used: RingCon.refl, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (c : (a : R) → R → Prop) x y
j' : n
inr : ∀ (hj : j ≠ j'), (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')
inr₁ : (c : (a : R) → R → Prop) (Matrix.single i j x i j) (Matrix.single i j y i j)
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
obtain hj | rfl := ne_or_eq j j'

Premises used: ne_or_eq, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (c : (a : R) → R → Prop) x y
j' : n
hj : j ≠ j'
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
simpa [hj] using c.refl _

Premises used: RingCon.refl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon R
i j : n
x y : R
h : (c : (a : R) → R → Prop) x y
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i j) (Matrix.single i j y i j)

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
⊢ Monotone (α := RingCon R) (β := RingCon (Matrix n n R)) (matrix n)

Tactic:
fun _ _ hc _ _ h _ _ ↦ hc (h _ _)

Premises used: Monotone
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : Nonempty n
I J : RingCon R
eq : Eq (α := RingCon (Matrix n n R)) (matrix n I) (matrix n J)
r s : R
⊢ Eq (α := Prop)
    ((matrix n I : (a : Matrix n n R) → Matrix n n R → Prop)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ r)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ s) :
      Prop)
    ((matrix n J : (a : Matrix n n R) → Matrix n n R → Prop)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ r)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ s) :
      Prop)

Tactic:
have := congr_fun (DFunLike.congr_fun eq (Matrix.of fun _ _ ↦ r)) (Matrix.of fun _ _ ↦ s)
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : Nonempty n
I J : RingCon R
eq : Eq (α := RingCon (Matrix n n R)) (matrix n I) (matrix n J)
r s : R
this :
  Eq (α := Prop)
    ((matrix n I : (a : Matrix n n R) → Matrix n n R → Prop)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ r)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ s) :
      Prop)
    ((matrix n J : (a : Matrix n n R) → Matrix n n R → Prop)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ r)
        ((Matrix.of : (a : n → n → R) → Matrix n n R) fun (x x_1 : n) ↦ s) :
      Prop)
⊢ (I : (a : R) → R → Prop) r s ↔ (J : (a : R) → R → Prop) r s

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : Nonempty n
⊢ StrictMono (α := RingCon R) (β := RingCon (Matrix n n R)) (matrix n)

Tactic:
matrix_monotone n |>.strictMono_of_injective <| matrix_injective _

Premises used: RingCon.matrix_injective, Monotone.strictMono_of_injective, RingCon.matrix_monotone
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
⊢ Eq (α := RingCon (Matrix n n R)) (matrix n ⊥) ⊥

Tactic:
eq_bot_iff.2 fun _ _ h ↦ Matrix.ext h

Premises used: Iff.mpr, eq_bot_iff, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
x x_1 : Matrix n n R
h : (⊤ : (a : Matrix n n R) → Matrix n n R → Prop) x x_1
x_2 x_3 : n
⊢ (⊤ : (a : R) → R → Prop) (x x_2 x_3) (x_1 x_2 x_3)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
w x y z : R
h₁ : ∀ (i j : n), (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j w) (single i j x)
h₂ : ∀ (i j : n), (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j y) (single i j z)
i j : n
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j (w * y)) (single i j (x * z))

Tactic:
simpa using c.mul (h₁ i i) (h₂ i j)

Premises used: RingCon.mul
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
w x y z : R
h₁ : ∀ (i j : n), (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j w) (single i j x)
h₂ : ∀ (i j : n), (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j y) (single i j z)
x_1 x_2 : n
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single x_1 x_2 (w + y)) (single x_1 x_2 (x + z))

Tactic:
simpa [single_add] using c.add (h₁ _ _) (h₂ _ _)

Premises used: Matrix.single_add, RingCon.add
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
x y : R
⊢ (c.ofMatrix : (a : R) → R → Prop) x y ↔
    ∀ (i j : n), (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
H : ∀ (x y : R), (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
⊢ ofMatrix (matrix n c) = c

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
x y : R
H : (ofMatrix (matrix n c) : (a : R) → R → Prop) x y → (c : (a : R) → R → Prop) x y
H₁ : (c : (a : R) → R → Prop) x y → (ofMatrix (matrix n c) : (a : R) → R → Prop) x y
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
x y : R
h : (ofMatrix (matrix n c) : (a : R) → R → Prop) x y
H : ∀ (inhabited_h : Inhabited n), (c : (a : R) → R → Prop) x y
⊢ (c : (a : R) → R → Prop) x y

Tactic:
inhabit n
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
x y : R
h : (ofMatrix (matrix n c) : (a : R) → R → Prop) x y
inhabited_h : Inhabited n
⊢ (c : (a : R) → R → Prop) x y

Tactic:
simpa using h default default default default

Premises used: Inhabited.default
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
x y : R
h : (c : (a : R) → R → Prop) x y
i j : n
H H₁ H₂ H₃ : (c : (a : R) → R → Prop) x y
⊢ (matrix n c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)

Tactic:
rwa [matrix_apply_single]

Premises used: RingCon.matrix_apply_single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
c : RingCon R
x y : R
H : (ofMatrix (matrix n c) : (a : R) → R → Prop) x y → (c : (a : R) → R → Prop) x y
H₁ H₂ : (c : (a : R) → R → Prop) x y → (ofMatrix (matrix n c) : (a : R) → R → Prop) x y
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y

Tactic:
classical
  constructor
  · intro h
    inhabit n
    simpa using h default default default default
  · intro h i j
    rwa [matrix_apply_single]

Premises used: RingCon.matrix_apply_single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
H :
  ∀ (x y : Matrix n n R),
    (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y ↔
      (c : (a : Matrix n n R) → Matrix n n R → Prop) x y
⊢ matrix n c.ofMatrix = c

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
H :
  (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y →
    (c : (a : Matrix n n R) → Matrix n n R → Prop) x y
H₁ :
  (c : (a : Matrix n n R) → Matrix n n R → Prop) x y →
    (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y
⊢ (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y ↔
    (c : (a : Matrix n n R) → Matrix n n R → Prop) x y

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y
H :
  (c : (a : Matrix n n R) → Matrix n n R → Prop) (∑ i : n, ∑ j : n, single i j (x i j))
    (∑ i : n, ∑ j : n, single i j (y i j))
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) x y

Tactic:
rw [matrix_eq_sum_single x, matrix_eq_sum_single y]

Premises used: Matrix.matrix_eq_sum_single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (∑ i : n, ∑ j : n, single i j (x i j))
    (∑ i : n, ∑ j : n, single i j (y i j))

Tactic:
c.finsetSum _ fun i _ ↦ c.finsetSum _ fun j _ ↦ h i j i j

Premises used: RingCon.toAddCon, AddCon.finsetSum, Finset.univ
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocSemiring R
inst_1 : Fintype n
inst_2 : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : (matrix n c.ofMatrix : (a : Matrix n n R) → Matrix n n R → Prop) x y
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (∑ i : n, ∑ j : n, single i j (x i j))
    (∑ i : n, ∑ j : n, single i j (y i j))

Tactic:
refine c.finsetSum _ fun i _ ↦ c.finsetSum _ fun j _ ↦ h i j i j

Premises used: RingCon.toAddCon, AddCon.finsetSum