awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
h_prim : A.IsPrimitive
⊢ A.IsIrreducible
have obtain : ∀ (h_nonneg : ∀ (i j : n), 0 ≤ A i j) (k : ℕ) (hk_pos : k > 0) (hk_all : ∀ (i j : n), 0 < (A ^ k) i j), A.IsIrreducible
Tactic: obtain ⟨h_nonneg, k, hk_pos, hk_all⟩ := h_prim
Cleared hypotheses: h_prim
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
inst_2 : Fintype n
inst_3 : IsOrderedRing R
inst_4 : PosMulStrictMono R
inst_5 : Nontrivial R
inst_6 : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ A.IsIrreducible
have rw : ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
Tactic: rw [isIrreducible_iff_exists_pow_pos h_nonneg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
this : Quiver n := A.toQuiver
b c : n
q : Path i b
e : b ⟶ c
ih : Path b i
⊢ Path c i
have eT : 0 < Aᵀ c b
Tactic: have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
p : Path i j
this : Quiver n := A.toQuiver
⊢ Path j i
have nil : Path i i
Tactic: induction p with
  | nil =>
    exact (@Quiver.Path.nil _ (toQuiver Aᵀ) _)
  | @cons b c q e ih =>
    have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
    exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
i j : n
p : Path i j
this : Quiver n := A.toQuiver
nil : Path i i
⊢ Path j i
have cons : {b c : n} → (q : Path i b) → (e : b ⟶ c) → (ih : Path b i) → Path c i
Tactic: induction p with
  | nil =>
    exact (@Quiver.Path.nil _ (toQuiver Aᵀ) _)
  | @cons b c q e ih =>
    have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
    exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
⊢ Aᵀ.IsIrreducible
have hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
Tactic: have hA_T_nonneg : ∀ i j, 0 ≤ Aᵀ i j := fun i j => by
    simpa [Matrix.transpose_apply] using hA.nonneg j i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
⊢ Aᵀ.IsIrreducible
have refine : IsSStronglyConnected n
Tactic: refine ⟨hA_T_nonneg, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
⊢ ∃ (p : Path i j), 0 < p.length
have obtain : ∀ (p : Path j i) (hp_pos : 0 < p.length), ∃ (p : Path i j), 0 < p.length
Tactic: obtain ⟨p, hp_pos⟩ := hA.connected j i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this_1 : Quiver n := A.toQuiver
b : n
q : Path j b
e : b ⟶ i
hp_pos : 0 < (q.cons e).length
qT : Path i j := transposePath (q.cons e)
this : Quiver n := Aᵀ.toQuiver
⊢ ∃ (p : Path i j), 0 < p.length
have h : 0 < qT.length
Tactic: use qT
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
p : Path j i
hp_pos : 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length
have nil : ∀ (hp_pos : 0 < length.{u_1, 0} (V := n) (a := i) nil), ∃ (p : Path i i), 0 < p.length
Tactic: cases p with
  | nil =>
    simp at hp_pos
  | @cons b _ q e =>
    let qT := transposePath (A := A) (q.cons e)
    letI : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]
Cleared hypotheses: j, p, hp_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA : A.IsIrreducible
hA_T_nonneg : ∀ (i j : n), 0 ≤ Aᵀ i j
i j : n
this : Quiver n := A.toQuiver
p : Path j i
hp_pos : 0 < p.length
nil : ∀ (hp_pos : 0 < length.{u_1, 0} (V := n) (a := i) Path.nil), ∃ (p : Path i i), 0 < p.length
⊢ ∃ (p : Path i j), 0 < p.length
have cons : ∀ {b : n} (q : Path j b) (e : b ⟶ i) (hp_pos : 0 < (q.cons e).length), ∃ (p : Path i j), 0 < p.length
Tactic: cases p with
  | nil =>
    simp at hp_pos
  | @cons b _ q e =>
    let qT := transposePath (A := A) (q.cons e)
    letI : Quiver n := toQuiver Aᵀ
    use qT
    simp [qT, transposePath, Quiver.Path.length_comp, Quiver.Path.length_toPath]
Cleared hypotheses: p, hp_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
have pos : ∀ (hA_nonneg : ∀ (i j : n), 0 ≤ A i j), Aᵀ.IsIrreducible ↔ A.IsIrreducible
Tactic: by_cases hA_nonneg : ∀ i j, 0 ≤ A i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
pos : ∀ (hA_nonneg : ∀ (i j : n), 0 ≤ A i j), Aᵀ.IsIrreducible ↔ A.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
have neg : ∀ (hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j), Aᵀ.IsIrreducible ↔ A.IsIrreducible
Tactic: by_cases hA_nonneg : ∀ i j, 0 ≤ A i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬Aᵀ.IsIrreducible
have rw : ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)
Tactic: rw [isIrreducible_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)
have simp : (∀ (i j : n), 0 ≤ A j i) → ∃ (x : n) (x_1 : n), ∀ (x_2 : Path x x_1), x_2.length = 0
Tactic: simp only [transpose_apply, isSStronglyConnected_iff, not_and, not_forall, not_exists,
        not_lt, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
have this : ¬Aᵀ.IsIrreducible
Tactic: have : ¬ Aᵀ.IsIrreducible := by
      rw [isIrreducible_iff]
      simp only [transpose_apply, isSStronglyConnected_iff, not_and, not_forall, not_exists,
        not_lt, nonpos_iff_eq_zero]
      intro a; simp_all only [implies_true, not_true_eq_false]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (goal)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬A.IsIrreducible
have rw : ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)
Tactic: rw [isIrreducible_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Irreducible.Defs (hypothesis)
Goal:
n : Type u_1
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
have this₁ : ¬A.IsIrreducible
Tactic: have : ¬ A.IsIrreducible := by
      rw [isIrreducible_iff]; simp_all only [not_forall, not_le, isSStronglyConnected_iff,
      not_and, not_exists, not_lt, nonpos_iff_eq_zero, isEmpty_Prop, IsEmpty.forall_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ diagonal A.diag i j = A i j
have inl : diagonal A.diag i i = A i i
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
inl : diagonal A.diag i i = A i i
⊢ diagonal A.diag i j = A i j
have inr : ∀ (hij : i ≠ j), diagonal A.diag i j = A i j
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i
have inl : A.diag i = A i i
Tactic: rw [diagonal_apply_eq, diag]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
inl : A.diag i = A i i
⊢ diagonal A.diag i i = A i i
have inl₁ : A i i = A i i
Tactic: rw [diagonal_apply_eq, diag]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ diagonal A.diag i j = A i j
have inr : 0 = A i j
Tactic: rw [diagonal_apply_ne _ hij, h hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
inr : 0 = A i j
⊢ diagonal A.diag i j = A i j
have inr₁ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [diagonal_apply_ne _ hij, h hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A.IsDiag
have h : A = Aᴴᴴ
Tactic: convert! ha.conjTranspose
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (hypothesis)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : (a, b) ≠ (c, d)
⊢ Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
have h₁ : ¬a = c ∨ ¬b = d
Tactic: simp only [Prod.mk_inj, Ne, not_and_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
⊢ Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
have inl : ∀ (hac : ¬a = c), Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
Tactic: rcases h with hac | hbd
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : MulZeroClass α
A : Matrix m m α
B : Matrix n n α
hA : A.IsDiag
hB : B.IsDiag
a : m
b : n
c : m
d : n
h : ¬a = c ∨ ¬b = d
inl : ∀ (hac : ¬a = c), Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
⊢ Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
have inr : ∀ (hbd : ¬b = d), Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0
Tactic: rcases h with hac | hbd
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
⊢ A.IsSymm
have a : ∀ (i j : n), Aᵀ i j = A i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ Aᵀ i j = A i j
have pos : ∀ (g : i = j), Aᵀ i j = A i j
Tactic: by_cases g : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
pos : ∀ (g : i = j), Aᵀ i j = A i j
⊢ Aᵀ i j = A i j
have neg : ∀ (g : ¬i = j), Aᵀ i j = A i j
Tactic: by_cases g : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
⊢ Aᵀ i j = A i j
have pos : Aᵀ j j = A j j
Tactic: rw [g, transpose_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
pos : Aᵀ j j = A j j
⊢ Aᵀ i j = A i j
have pos₁ : A j j = A j j
Tactic: rw [g, transpose_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
⊢ (fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mp : (fromBlocks A B C D).IsDiag → A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
mp : (fromBlocks A B C D).IsDiag → A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
⊢ (fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mpr : A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag → (fromBlocks A B C D).IsDiag
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mp : ∀ (i j : m) (hij : i ≠ j), (fun (i j : m) ↦ A i j = 0) i j
Tactic: refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
mp : ∀ (i j : m) (hij : i ≠ j), (fun (i j : m) ↦ A i j = 0) i j
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mp₁ : ∀ (i : m) (j : n), B i j = 0 i j
Tactic: refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
mp : ∀ (i j : m) (hij : i ≠ j), (fun (i j : m) ↦ A i j = 0) i j
mp₁ : ∀ (i : m) (j : n), B i j = 0 i j
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mp₂ : ∀ (i : n) (j : m), C i j = 0 i j
Tactic: refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
mp : ∀ (i j : m) (hij : i ≠ j), (fun (i j : m) ↦ A i j = 0) i j
mp₁ : ∀ (i : m) (j : n), B i j = 0 i j
mp₂ : ∀ (i : n) (j : m), C i j = 0 i j
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
have mp₃ : ∀ (i j : n) (hij : i ≠ j), (fun (i j : n) ↦ D i j = 0) i j
Tactic: refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.IsDiag (goal)
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 C D).IsDiag
have rw : (Matrix.fromBlocks A 0 0ᵀ D).IsDiag
Tactic: rw [← (isSymm_fromBlocks_iff.1 h).2.1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) = single (i₁, i₂) (j₁, j₂) (f a b)
have a₁ : ∀ (i₁' : l) (i₂' : n) (j₁' : m) (j₂' : p),
  kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    single (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')
Tactic: ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq l
inst_4 : DecidableEq m
inst_5 : DecidableEq n
inst_6 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    single (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')
have a₁ : f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
  if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero β
inst_2 : Zero γ
inst_3 : DecidableEq m
inst_4 : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun (mn : m × n) ↦ f (a mn.1) (b mn.2)
have a₁ : ∀ (i₁ : m) (i₂ : n) (j₁ : m) (j₂ : n),
  kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun (mn : m × n) ↦ f (a mn.1) (b mn.2)) (i₁, i₂) (j₁, j₂)
Tactic: ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero β
inst_1 : Zero γ
inst_2 : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun (i : n) ↦ A.map fun (a : α) ↦ f a (b i)
have a : ∀ (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : n),
  kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) =
    blockDiagonal (fun (i : n) ↦ A.map fun (a : α) ↦ f a (b i)) (i₁, i₂) (j₁, j₂)
Tactic: ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst : Zero α
inst_1 : Zero γ
inst_2 : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) γ) → Matrix (l × m) (l × n) γ)
      (blockDiagonal fun (i : l) ↦ B.map fun (b : β) ↦ f (a i) b)
have a₁ : ∀ (i₁ : l) (i₂ : m) (j₁ : l) (j₂ : n),
  kroneckerMap f (diagonal a) B (i₁, i₂) (j₁, j₂) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l) : (a : Matrix (m × l) (n × l) γ) → Matrix (l × m) (l × n) γ)
      (blockDiagonal fun (i : l) ↦ B.map fun (b : β) ↦ f (a i) b) (i₁, i₂) (j₁, j₂)
Tactic: ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ Eq (α := Matrix (l' × n') (m' × p') γ)
    (kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M)
      ((reindex en ep : (a : Matrix n p β) → Matrix n' p' β) N))
    ((reindex (el.prodCongr en) (em.prodCongr ep) : (a : Matrix (l × n) (m × p) γ) → Matrix (l' × n') (m' × p') γ)
      (kroneckerMap f M N))
have a : ∀ (i : l') (i' : n') (j : m') (j' : p'),
  kroneckerMap f ((reindex el em : (a : Matrix l m α) → Matrix l' m' α) M)
      ((reindex en ep : (a : Matrix n p β) → Matrix n' p' β) N) (i, i') (j, j') =
    (reindex (el.prodCongr en) (em.prodCongr ep) : (a : Matrix (l × n) (m × p) γ) → Matrix (l' × n') (m' × p') γ)
      (kroneckerMap f M N) (i, i') (j, j')
Tactic: ext ⟨i, i'⟩ ⟨j, j'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Kronecker (goal)
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst : Semiring S
inst_1 : Semiring R
inst_2 : Fintype m
inst_3 : Fintype m'
inst_4 : NonUnitalNonAssocSemiring α
inst_5 : NonUnitalNonAssocSemiring β
inst_6 : NonUnitalNonAssocSemiring γ
inst_7 : Module R α
inst_8 : Module R γ
inst_9 : Module S β
inst_10 : Module S γ
inst_11 : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm :
  ∀ (a b : α) (a' b' : β),
    (((f : (a : α) → β →ₗ[S] γ) (a * b) : β →ₗ[S] γ) : (a : β) → γ) (a' * b') =
      HMul.hMul (α := γ) (β := γ) ((((f : (a : α) → β →ₗ[S] γ) a : β →ₗ[S] γ) : (a : β) → γ) a' : γ)
        ((((f : (a : α) → β →ₗ[S] γ) b : β →ₗ[S] γ) : (a : β) → γ) b' : γ)
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ (((kroneckerMapBilinear f : (a : Matrix l n α) → Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) (A * B) :
          Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) :
        (a : Matrix l' n' β) → Matrix (l × l') (n × n') γ)
      (A' * B') =
    HMul.hMul (α := Matrix (l × l') (m × m') γ) (β := Matrix (m × m') (n × n') γ)
      ((((kroneckerMapBilinear f : (a : Matrix l m α) → Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) A :
              Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) :
            (a : Matrix l' m' β) → Matrix (l × l') (m × m') γ)
          A' :
        Matrix (l × l') (m × m') γ)
      ((((kroneckerMapBilinear f : (a : Matrix m n α) → Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) B :
              Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) :
            (a : Matrix m' n' β) → Matrix (m × m') (n × n') γ)
          B' :
        Matrix (m × m') (n × n') γ)
have a : ∀ (i : l) (i' : l') (j : n) (j' : n'),
  (((kroneckerMapBilinear f : (a : Matrix l n α) → Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) (A * B) :
          Matrix l' n' β →ₗ[S] Matrix (l × l') (n × n') γ) :
        (a : Matrix l' n' β) → Matrix (l × l') (n × n') γ)
      (A' * B') (i, i') (j, j') =
    HMul.hMul (α := Matrix (l × l') (m × m') γ) (β := Matrix (m × m') (n × n') γ)
      ((((kroneckerMapBilinear f : (a : Matrix l m α) → Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) A :
              Matrix l' m' β →ₗ[S] Matrix (l × l') (m × m') γ) :
            (a : Matrix l' m' β) → Matrix (l × l') (m × m') γ)
          A' :
        Matrix (l × l') (m × m') γ)
      ((((kroneckerMapBilinear f : (a : Matrix m n α) → Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) B :
              Matrix m' n' β →ₗ[S] Matrix (m × m') (n × n') γ) :
            (a : Matrix m' n' β) → Matrix (m × m') (n × n') γ)
          B' :
        Matrix (m × m') (n × n') γ)
      (i, i') (j, j')
Tactic: ext ⟨i, i'⟩ ⟨j, j'⟩