awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (c : (a : Matrix n n R) → Matrix n n R → Prop) x y
i' j' i j : n
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j (x i' j')) (single i j (y i' j'))

Tactic:
simpa using c.mul (c.mul (c.refl <| single i i' 1) h) (c.refl <| single j' j 1)

Premises used: RingCon.mul, RingCon.refl, OfNat.ofNat, Matrix.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) x y
H₁ 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:
classical
  constructor
  · intro h
    rw [matrix_eq_sum_single x, matrix_eq_sum_single y]
    refine c.finsetSum _ fun i _ ↦ c.finsetSum _ fun j _ ↦ h i j i j
  · intro h i' j' i j
    simpa using c.mul (c.mul (c.refl <| single i i' 1) h) (c.refl <| single j' j 1)

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 : R
i j : n
⊢ (c.ofMatrix : (a : R) → R → Prop) x y ↔ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)

Tactic:
⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩

Premises used: Iff.intro
-- 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 : R
i j : n
refine :
  ∀ (h : (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)) (i' j' : n),
    (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i' j' x) (single i' j' y)
⊢ (c.ofMatrix : (a : R) → R → Prop) x y ↔ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)

Tactic:
refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩
-- 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 : R
i j : n
h : (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i j x) (single i j y)
i' j' : n
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i' j' x) (single i' j' y)

Tactic:
simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

Premises used: RingCon.mul, RingCon.refl, OfNat.ofNat, Matrix.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)
i j : n
h :
  ∀ (x y : R),
    (c.ofMatrix : (a : R) → R → Prop) x y ↔
      Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
        (fun (x : Matrix n n R) ↦ x i j) x y
⊢ Eq (α := (a : R) → R → Prop) (⇑c.ofMatrix : (a : R) → R → Prop)
    (Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      fun (x : Matrix n n R) ↦ x i j)

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)
i j : n
x y : R
h :
  (c.ofMatrix : (a : R) → R → Prop) x y →
    Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      (fun (x : Matrix n n R) ↦ x i j) x y
h₁ :
  Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      (fun (x : Matrix n n R) ↦ x i j) x y →
    (c.ofMatrix : (a : R) → R → Prop) x y
⊢ (c.ofMatrix : (a : R) → R → Prop) x y ↔
    Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
      (fun (x : Matrix n n R) ↦ x i j) 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)
i j : n
x y : R
h : (c.ofMatrix : (a : R) → R → Prop) x y
⊢ Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
    (fun (x : Matrix n n R) ↦ x i j) x y

Tactic:
⟨_,_, h i j, ?_⟩

Premises used: And.intro, Exists.intro, Relation.Map
-- 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)
i j : n
x y : R
h : (c.ofMatrix : (a : R) → R → Prop) x y
h₁ : (fun (x : Matrix n n R) ↦ x i j) (single i j x) = x ∧ (fun (x : Matrix n n R) ↦ x i j) (single i j y) = y
⊢ Relation.Map (⇑c : (a : Matrix n n R) → Matrix n n R → Prop) (fun (x : Matrix n n R) ↦ x i j)
    (fun (x : Matrix n n R) ↦ x i j) x y

Tactic:
refine ⟨_,_, h i j, ?_⟩
-- 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)
i j : n
x y : R
h : (c.ofMatrix : (a : R) → R → Prop) x y
⊢ (fun (x : Matrix n n R) ↦ x i j) (single i j x) = x ∧ (fun (x : Matrix n n R) ↦ x i j) (single i j y) = y

Tactic:
simp
-- 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)
i j : n
X Y : Matrix n n R
h : (c : (a : Matrix n n R) → Matrix n n R → Prop) X Y
i' j' : n
⊢ (c : (a : Matrix n n R) → Matrix n n R → Prop) (single i' j' ((fun (x : Matrix n n R) ↦ x i j) X))
    (single i' j' ((fun (x : Matrix n n R) ↦ x i j) Y))

Tactic:
simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

Premises used: RingCon.mul, RingCon.refl, OfNat.ofNat, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Fintype n
I : TwoSidedIdeal R
M : Matrix n n R
⊢ Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) M ↔ ∀ (i j : n), M i j ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Fintype n
⊢ Monotone (α := TwoSidedIdeal R) (β := TwoSidedIdeal (Matrix n n R)) (matrix n)

Tactic:
fun _ _ IJ _ MI i j => IJ (MI i j)

Premises used: Set.Mem, Monotone, setOf
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Fintype n
h : Nonempty n
⊢ StrictMono (α := TwoSidedIdeal R) (β := TwoSidedIdeal (Matrix n n R)) (matrix n)

Tactic:
matrix_monotone n |>.strictMono_of_injective <|
    .comp (fun _ _ => mk.inj) <| (RingCon.matrix_injective n).comp ringCon_injective

Premises used: TwoSidedIdeal.ringCon_injective, TwoSidedIdeal.mk.inj, setOf, RingCon.matrix_injective, Function.Injective.comp, Monotone.strictMono_of_injective, TwoSidedIdeal.matrix_monotone
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Fintype n
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (matrix n ⊥) ⊥

Tactic:
ringCon_injective <| RingCon.matrix_bot _

Premises used: TwoSidedIdeal.ringCon_injective, RingCon.matrix_bot
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : Fintype n
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (matrix n ⊤) ⊤

Tactic:
ringCon_injective <| RingCon.matrix_top _

Premises used: TwoSidedIdeal.ringCon_injective, RingCon.matrix_top
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
h :
  ∀ (r : R),
    r ∈
        (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) :
          Set R) ↔
      Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
⊢ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) =
    {x : R | ∃ N ∈ I, N i j = x}

Tactic:
ext r
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h :
  r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) →
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r
h₁ :
  Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r →
    r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
⊢ r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R) ↔
    Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h : r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
⊢ single i j r ∈ I

Tactic:
simpa using h i j
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h : r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
⊢ single i j r i j = r

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h : r ∈ (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n n R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)
⊢ Membership.mem (γ := Set R) {x : R | ∃ N ∈ I, N i j = x} r

Tactic:
exact ⟨single i j r, by simpa using h i j, by simp⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n_1 : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n_1
inst_2 : Nonempty n_1
inst_3 : DecidableEq n_1
I : TwoSidedIdeal (Matrix n_1 n_1 R)
i j : n_1
n : Matrix n_1 n_1 R
hn : n ∈ I
h :
  Relation.Map (δ := R) (⇑I.ringCon : (a : Matrix n_1 n_1 R) → Matrix n_1 n_1 R → Prop)
    (fun (x : Matrix n_1 n_1 R) ↦ x i j) (fun (x : Matrix n_1 n_1 R) ↦ x i j) (n i j) 0
⊢ n i j ∈
    (↑((Equiv.symm equivMatrix : (a : TwoSidedIdeal (Matrix n_1 n_1 R)) → TwoSidedIdeal R) I : TwoSidedIdeal R) : Set R)

Tactic:
rw [SetLike.mem_coe, mem_iff, equivMatrix_symm_apply_ringCon,
      RingCon.coe_ofMatrix_eq_relationMap i j]

Premises used: TwoSidedIdeal.equivMatrix_symm_apply_ringCon, RingCon.coe_ofMatrix_eq_relationMap, TwoSidedIdeal.mem_iff, SetLike.mem_coe
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n_1 : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n_1
inst_2 : Nonempty n_1
inst_3 : DecidableEq n_1
I : TwoSidedIdeal (Matrix n_1 n_1 R)
i j : n_1
n : Matrix n_1 n_1 R
hn : n ∈ I
⊢ Relation.Map (δ := R) (⇑I.ringCon : (a : Matrix n_1 n_1 R) → Matrix n_1 n_1 R → Prop)
    (fun (x : Matrix n_1 n_1 R) ↦ x i j) (fun (x : Matrix n_1 n_1 R) ↦ x i j) (n i j) 0

Tactic:
⟨n, 0, (I.mem_iff n).mp hn, rfl, rfl⟩

Premises used: TwoSidedIdeal.mem_iff, And.intro, Exists.intro, Iff.mp, OfNat.ofNat, rfl, Relation.Map
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n_1 : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n_1
inst_2 : Nonempty n_1
inst_3 : DecidableEq n_1
I : TwoSidedIdeal (Matrix n_1 n_1 R)
i j : n_1
n : Matrix n_1 n_1 R
hn : n ∈ I
⊢ Relation.Map (δ := R) (⇑I.ringCon : (a : Matrix n_1 n_1 R) → Matrix n_1 n_1 R → Prop)
    (fun (x : Matrix n_1 n_1 R) ↦ x i j) (fun (x : Matrix n_1 n_1 R) ↦ x i j) (n i j) 0

Tactic:
exact ⟨n, 0, (I.mem_iff n).mp hn, rfl, rfl⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
mp : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) → I ≤ J
mpr : I ≤ J → LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J)
⊢ LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J) ↔ I ≤ J

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
le : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
xI : x ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
    ((of : (a : n → n → R) → Matrix n n R) fun (x_1 x_2 : n) ↦ x)

Tactic:
simp [xI]
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
le : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
xI : x ∈ I
⊢ Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n J)
    ((of : (a : n → n → R) → Matrix n n R) fun (x_1 x_2 : n) ↦ x)

Tactic:
specialize @le (of fun _ _ => x) (by simp [xI])
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
x : R
xI : x ∈ I
le :
  Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n J)
    ((of : (a : n → n → R) → Matrix n n R) fun (x_1 x_2 : n) ↦ x)
⊢ x ∈ J

Tactic:
simpa using le
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
MI : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) M
i j : n
⊢ (J.ringCon : (a : R) → R → Prop) (M i j) (0 i j)

Tactic:
IJ <| MI i j

Premises used: Set.Mem, setOf
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : NonAssocRing R
inst_1 : Fintype n
inst_2 : Nonempty n
inst_3 : DecidableEq n
I J : TwoSidedIdeal R
IJ : I ≤ J
M : Matrix n n R
MI : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) M
i j : n
⊢ (J.ringCon : (a : R) → R → Prop) (M i j) (0 i j)

Tactic:
exact IJ <| MI i j
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : Ring R
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
h :
  ∀ (x : Matrix n n R),
    Membership.mem (γ := Ideal (Matrix n n R))
        ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I) : Ideal (Matrix n n R)) x ↔
      Membership.mem (γ := Ideal (Matrix n n R)) (Ideal.matrix n ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x
⊢ Eq (α := Ideal (Matrix n n R))
    ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I) : Ideal (Matrix n n R))
    (Ideal.matrix n ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) : Ideal (Matrix n n R))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Ideal
Goal:
R : Type u_1
n : Type u_2
inst : Ring R
inst_1 : Fintype n
inst_2 : DecidableEq n
I : TwoSidedIdeal R
x : Matrix n n R
⊢ Membership.mem (γ := Ideal (Matrix n n R))
      ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I) : Ideal (Matrix n n R)) x ↔
    Membership.mem (γ := Ideal (Matrix n n R)) (Ideal.matrix n ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x

Tactic:
simp
-- 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 : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
simp : M p q ∈ I.jacobson
⊢ (I.jacobson.ringCon : (a : R) → R → Prop) (M p q) (0 p q)

Tactic:
simp only [zero_apply, ← mem_iff]

Premises used: Matrix.zero_apply, TwoSidedIdeal.mem_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 : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
rw : ∀ (y : R), ∃ (z : R), z * y * M p q + z - 1 ∈ I
⊢ M p q ∈ I.jacobson

Tactic:
rw [mem_jacobson_iff]

Premises used: TwoSidedIdeal.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 : TwoSidedIdeal R
M : Matrix n n R
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) M
p q : n
⊢ Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (M * single q p 1)

Tactic:
replace Mmem := mul_mem_right _ _ (single q p 1) Mmem
-- 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 : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem : Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (M * single q p 1)
⊢ ∀ (y : Matrix n n R),
    ∃ (z : Matrix n n R),
      Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) (z * y * (M * single q p 1) + z - 1)

Tactic:
rw [mem_jacobson_iff] at Mmem

Premises used: TwoSidedIdeal.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 : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem :
  ∀ (y : Matrix n n R),
    ∃ (z : Matrix n n R),
      Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I) (z * y * (M * single q p 1) + z - 1)
y : R
⊢ ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)

Tactic:
specialize Mmem (y • single p p 1)

Premises used: HSMul.hSMul, OfNat.ofNat, 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 : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem :
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
have :
  ∀ (N : Matrix n n R)
    (NxMI :
      Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
        (N * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + N - 1)),
    ∃ (z : R), z * y * M p q + z - 1 ∈ I
⊢ ∃ (z : R), z * y * M p q + z - 1 ∈ I

Tactic:
have ⟨N, NxMI⟩ := Mmem
-- 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 : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem :
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
N : Matrix n n R
NxMI :
  Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
    (N * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + N - 1)
h : N p p * y * M p q + N p p - 1 ∈ I
⊢ ∃ (z : R), z * y * M p q + z - 1 ∈ I

Tactic:
use N p 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 : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem :
  ∃ (z : Matrix n n R),
    Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
      (z * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + z - 1)
N : Matrix n n R
NxMI :
  Membership.mem (γ := TwoSidedIdeal (Matrix n n R)) (matrix n I)
    (N * HSMul.hSMul (β := Matrix n n R) y (single p p 1) * (M * single q p 1) + N - 1)
⊢ N p p * y * M p q + N p p - 1 ∈ I

Tactic:
simpa [mul_apply, single, ite_and] using NxMI p p

Premises used: Matrix.mul_apply, 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 : TwoSidedIdeal R
a : LE.le (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)
a₁ : LE.le (α := TwoSidedIdeal (Matrix n n R)) (matrix n I.jacobson) (jacobson (matrix n I))
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 : TwoSidedIdeal R
⊢ LE.le (α := TwoSidedIdeal (Matrix n n R)) (jacobson (matrix n I)) (matrix n I.jacobson)

Tactic:
apply jacobson_matrix_le

Premises used: _private.0.TwoSidedIdeal.jacobson_matrix_le
-- 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 : TwoSidedIdeal R
⊢ GE.ge (α := Ideal (Matrix n n R))
    ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (jacobson (matrix n I)) :
      Ideal (Matrix n n R))
    ((asIdeal : (a : TwoSidedIdeal (Matrix n n R)) → Ideal (Matrix n n R)) (matrix n I.jacobson) : Ideal (Matrix n n R))

Tactic:
simp [asIdeal_jacobson, asIdeal_matrix, Ideal.matrix_jacobson_le]

Premises used: TwoSidedIdeal.asIdeal_jacobson, Ideal.matrix_jacobson_le, TwoSidedIdeal.asIdeal_matrix
-- 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
⊢ Eq (α := TwoSidedIdeal (Matrix n n R)) (matrix n (jacobson ⊥)) (jacobson ⊥)

Tactic:
matrix_bot n (R := R) ▸ (jacobson_matrix _).symm

Premises used: TwoSidedIdeal.matrix_bot, TwoSidedIdeal.jacobson_matrix, Eq.rec, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
n : Type u_2
inst : Fintype n
α : Type u_3
inst_1 : NonAssocSemiring α
A B : Matrix n n ℕ
⊢ (A * B).map Nat.cast = HMul.hMul (α := Matrix n n α) (A.map Nat.cast) (B.map Nat.cast)

Tactic:
Matrix.map_mul (f := Nat.castRingHom α)

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
n : Type u_2
inst : Fintype n
α : Type u_3
inst_1 : NonAssocRing α
A B : Matrix n n ℤ
⊢ (A * B).map Int.cast = HMul.hMul (α := Matrix n n α) (A.map Int.cast) (B.map Int.cast)

Tactic:
Matrix.map_mul (f := Int.castRingHom α)

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
n : Type u_2
inst : Fintype n
α : Type u_3
inst_1 : DivisionRing α
inst_2 : CharZero α
A B : Matrix n n ℚ
⊢ (A * B).map Rat.cast = HMul.hMul (α := Matrix n n α) (A.map Rat.cast) (B.map Rat.cast)

Tactic:
Matrix.map_mul (f := Rat.castHom α)

Premises used: Matrix.map_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ A.den ≠ 0

Tactic:
simp [Matrix.den, Finset.lcm_eq_zero_iff]

Premises used: Matrix.den, Finset.lcm_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
⊢ A.num = 0 ↔ A = 0

Tactic:
simp [Matrix.num, ← ext_iff, A.den_ne_zero]

Premises used: Matrix.den_ne_zero, Matrix.num, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
r : ℕ
⊢ A.den ∣ r ↔ ∀ (i : m) (j : n), (A i j).den ∣ r

Tactic:
simp [Matrix.den]

Premises used: Matrix.den
-- Module: Mathlib.LinearAlgebra.Matrix.Integer
Goal:
m : Type u_1
n : Type u_2
inst : Fintype m
inst_1 : Fintype n
A : Matrix m n ℚ
i : m
j : n
obtain : ∀ (k : ℕ) (hk : A.den = (A i j).den * k), HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j
⊢ HDiv.hDiv (α := ℚ) (↑(A.num i j) : ℚ) (↑A.den : ℚ) = A i j

Tactic:
obtain ⟨k, hk⟩ := den_dvd_iff.mp (dvd_refl A.den) i j

Premises used: Matrix.den_dvd_iff, Iff.mp, Matrix.den, dvd_refl