awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B Bᴴ D).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
have rw : (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
Tactic: rw [← isHermitian_submatrix_equiv (Equiv.sumComm n m), Equiv.sumComm_apply,
    fromBlocks_submatrix_sum_swap_sum_swap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Hermitian (goal)
Goal:
α : Type u_1
m : Type u_3
n : Type u_4
inst : CommRing α
inst_1 : StarRing α
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
hD : D.IsHermitian
⊢ (Matrix.fromBlocks D Bᴴ B A).IsHermitian ↔ (A - B * D⁻¹ * Bᴴ).IsHermitian
have h : B = Bᴴᴴ
Tactic: convert! IsHermitian.fromBlocks₁₁ _ _ hD
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j : n
⊢ (M • N) i j ∈ (↑I.toAddSubmonoid : Set R)
have rw : ∑ j_1 : n, M i j_1 * N j_1 j ∈ (↑I.toAddSubmonoid : Set R)
Tactic: rw [smul_eq_mul, mul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : Membership.mem (γ := Set (Matrix n n R)) (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup I.matrix)) N
i j : n
⊢ ∑ j_1 : n, M i j_1 * N j_1 j ∈ (↑I.toAddSubmonoid : Set R)
have h : ∀ (c : n), Membership.mem (γ := Finset n) Finset.univ c → M i c * N c j ∈ I.toAddSubmonoid
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
I J : Ideal R
eq : Eq (α := Ideal (Matrix n n R)) (matrix n I) (matrix n J)
⊢ I = J
have h : ∀ (x : R), x ∈ I ↔ x ∈ J
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : Nonempty n
I J : Ideal R
eq : Eq (α := Ideal (Matrix n n R)) (matrix n I) (matrix n J)
x : R
⊢ x ∈ I ↔ x ∈ J
have this : (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J
Tactic: have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := Ideal (Matrix n n R)) (matrix n ⊥) ⊥
have h : ∀ (M : Matrix n n R),
  Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊥) M ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊥ M
Tactic: ext M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
⊢ Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊥) M ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊥ M
have h : (∀ (i j : n), M i j = 0) ↔ M = 0
Tactic: simp only [mem_matrix, mem_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0
have h : (∀ (i j : n), M i j = 0) → M = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
h : (∀ (i j : n), M i j = 0) → M = 0
⊢ (∀ (i j : n), M i j = 0) ↔ M = 0
have h₁ : M = 0 → ∀ (i j : n), M i j = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
⊢ M = 0
have h : ∀ (i j : n), M i j = 0 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Semiring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := Ideal (Matrix n n R)) (matrix n ⊤) ⊤
have h : ∀ (x : Matrix n n R),
  Membership.mem (γ := Ideal (Matrix n n R)) (matrix n ⊤) x ↔ Membership.mem (γ := Ideal (Matrix n n R)) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
Goal:
R : Type u_1
inst : Ring R
n : Type u_2
inst_1 : Fintype n
inst_2 : DecidableEq n
I : Ideal R
⊢ ∀ x ∈ I.jacobson, ∀ (i j : n), Membership.mem (γ := Ideal (Matrix n n R)) (jacobson (matrix n I)) (single i j x)
have 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)
Tactic: simp_rw [Ideal.mem_jacobson_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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 : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * M * single p q x + z - 1)
have 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)
Tactic: have ⟨z, zMx⟩ := xIJ (M q p)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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))
⊢ ∃ (z : Matrix n n R), Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (z * M * single p q x + z - 1)
have h : Membership.mem (γ := Ideal (Matrix n n R)) (matrix n I) (N * M * single p q x + N - 1)
Tactic: use N
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i j ∈ (↑I.toAddSubmonoid : Set R)
have h : HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
Tactic: obtain rfl | qj := eq_or_ne q j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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)
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i j ∈ (↑I.toAddSubmonoid : Set R)
have h₁ : ∀ (qj : q ≠ j), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
have pos : ∀ (iq : i = q), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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)
⊢ HSub.hSub (β := Matrix n n R) (N * M * single p q x + N) 1 i q ∈ (↑I.toAddSubmonoid : Set R)
have neg : ∀ (iq : ¬i = q), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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)
have 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)
Tactic: convert! I.mul_mem_left (-M i p * x) zMx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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 = -M i p * x * (z * M q p * x + z - 1)
have 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))
Tactic: simp [iq, N, single, mul_apply, sum_apply, ite_and, sub_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ Membership.mem (γ := Submodule (Matrix n n R) (Matrix n n R)) (jacobson (matrix n I) : Ideal (Matrix n n R)) M
have 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))
Tactic: rw [matrix_eq_sum_single M]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ 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))
have 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))
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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))
have 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))
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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')
Tactic: refine ⟨fun h ↦ by simpa using h i j, fun h i' j' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')
have inl : ∀ (hi : i ≠ i'), (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'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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')
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i' j') (Matrix.single i j y i' j')
have inr : (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'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')
have inr : ∀ (hj : j ≠ 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'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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')
⊢ (c : (a : R) → R → Prop) (Matrix.single i j x i j') (Matrix.single i j y i j')
have inr₁ : (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'
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (hypothesis)
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
⊢ (I : (a : R) → R → Prop) r s ↔ (J : (a : R) → R → Prop) r s
have 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)
Tactic: have := congr_fun (DFunLike.congr_fun eq (Matrix.of fun _ _ ↦ r)) (Matrix.of fun _ _ ↦ s)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ ofMatrix (matrix n c) = c
have H : ∀ (x y : R), (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
have H : (ofMatrix (matrix n c) : (a : R) → R → Prop) x y → (c : (a : R) → R → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
have H₁ : (c : (a : R) → R → Prop) x y → (ofMatrix (matrix n c) : (a : R) → R → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
have H : ∀ (inhabited_h : Inhabited n), (c : (a : R) → R → Prop) x y
Tactic: inhabit n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
have H : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (ofMatrix (matrix n c) : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y
have H₁ : (c : (a : R) → R → Prop) x y → (ofMatrix (matrix n 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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)
⊢ matrix n c.ofMatrix = c
have 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
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
have 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))
Tactic: rw [matrix_eq_sum_single x, matrix_eq_sum_single y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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)
have 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)
Tactic: refine ⟨fun h ↦ h i j, fun h i' j' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ 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)
have 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
Tactic: ext x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Ideal (goal)
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
⊢ (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
have 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: constructor