awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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

Tactic:
exact ⟨fun h ↦
    let hA_T_nonneg : ∀ i j, 0 ≤ (Aᵀ) i j := fun i j => by
      simpa [Matrix.transpose_apply] using hA_nonneg j i
    IsIrreducible.transpose h,
   fun h ↦ IsIrreducible.transpose h⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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
rw : ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)
⊢ ¬Aᵀ.IsIrreducible

Tactic:
rw [isIrreducible_iff]

Premises used: Matrix.isIrreducible_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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
simp : (∀ (i j : n), 0 ≤ A j i) → ∃ (x : n) (x_1 : n), ∀ (x_2 : Path x x_1), x_2.length = 0
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)

Tactic:
simp only [transpose_apply, isSStronglyConnected_iff, not_and, not_forall, not_exists,
        not_lt, nonpos_iff_eq_zero]

Premises used: not_exists, not_lt, Matrix.transpose_apply, not_and, Classical.not_forall, nonpos_iff_eq_zero, Quiver.isSStronglyConnected_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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 : ∀ (i j : n), 0 ≤ A j i
⊢ ∃ (x : n) (x_1 : n), ∀ (x_2 : Path x x_1), x_2.length = 0

Tactic:
simp_all only [implies_true, not_true_eq_false]

Premises used: not_true_eq_false, implies_true
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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
rw : ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)
⊢ ¬A.IsIrreducible

Tactic:
rw [isIrreducible_iff]

Premises used: Matrix.isIrreducible_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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
⊢ ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)

Tactic:
simp_all only [not_forall, not_le, isSStronglyConnected_iff,
      not_and, not_exists, not_lt, nonpos_iff_eq_zero, isEmpty_Prop, IsEmpty.forall_iff]

Premises used: not_le, not_exists, not_lt, isEmpty_Prop, not_and, Classical.not_forall, IsEmpty.forall_iff, nonpos_iff_eq_zero, Quiver.isSStronglyConnected_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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

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]
-- Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
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_1 : ¬Aᵀ.IsIrreducible
this : ¬A.IsIrreducible
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible

Tactic:
simp_all only [not_forall, not_le]

Premises used: not_le, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
d : n → α
⊢ (diagonal d).IsDiag

Tactic:
fun _ _ =>
  Matrix.diagonal_apply_ne _

Premises used: Matrix.IsDiag, Pairwise, Matrix.diagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
inr : ∀ (hij : i ≠ j), diagonal A.diag i j = A i j
⊢ diagonal A.diag i j = A i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
inl₁ inl₂ : A i i = A i i
⊢ diagonal A.diag i i = A i i

Tactic:
rw [diagonal_apply_eq, diag]

Premises used: Matrix.diag, Matrix.diagonal_apply_eq
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
inr₁ inr₂ : Eq.{u_1 + 1} (α := α) 0 0
⊢ diagonal A.diag i j = A i j

Tactic:
rw [diagonal_apply_ne _ hij, h hij]

Premises used: Matrix.diagonal_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : DecidableEq n
A : Matrix n n α
⊢ A.IsDiag ↔ diagonal A.diag = A

Tactic:
⟨IsDiag.diagonal_diag, fun hd => hd ▸ isDiag_diagonal (diag A)⟩

Premises used: Matrix.diag, Eq.rec, Matrix.IsDiag.diagonal_diag, Iff.intro, Matrix.isDiag_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
inst_1 : Subsingleton n
A : Matrix n n α
⊢ A.IsDiag

Tactic:
fun i j h => (h <| Subsingleton.elim i j).elim

Premises used: False.elim, Matrix.IsDiag, Pairwise, Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
⊢ IsDiag.{u_1, u_4} (α := α) (n := n) 0

Tactic:
fun _ _ _ => rfl

Premises used: Matrix.IsDiag, Pairwise, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : DecidableEq n
inst_1 : Zero α
inst_2 : One α
⊢ IsDiag.{u_1, u_4} (α := α) (n := n) 1

Tactic:
fun _ _ =>
  one_apply_ne

Premises used: Matrix.one_apply_ne, Matrix.IsDiag, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
β : Type u_2
n : Type u_4
inst : Zero α
inst_1 : Zero β
A : Matrix n n α
ha : A.IsDiag
f : α → β
hf : f 0 = 0
i j : n
h : i ≠ j
⊢ A.map f i j = 0

Tactic:
simp [ha h, hf]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : SubtractionMonoid α
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (-A) i j = 0

Tactic:
simp [ha h]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : SubtractionMonoid α
A : Matrix n n α
⊢ (-A).IsDiag ↔ A.IsDiag

Tactic:
⟨fun ha _ _ h => neg_eq_zero.1 (ha h), IsDiag.neg⟩

Premises used: neg_eq_zero, Matrix.IsDiag.neg, Iff.intro, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : AddZeroClass α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A + B) i j = 0

Tactic:
simp [ha h, hb h]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : SubtractionMonoid α
A B : Matrix n n α
ha : A.IsDiag
hb : B.IsDiag
i j : n
h : i ≠ j
⊢ (A - B) i j = 0

Tactic:
simp [ha h, hb h]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
R : Type u_3
n : Type u_4
inst : Zero α
inst_1 : SMulZeroClass R α
k : R
A : Matrix n n α
ha : A.IsDiag
i j : n
h : i ≠ j
⊢ (k • A) i j = 0

Tactic:
simp [ha h]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_6
inst : MulZeroOneClass α
inst_1 : DecidableEq n
k : α
⊢ (HSMul.hSMul (β := Matrix n n α) k 1).IsDiag

Tactic:
isDiag_one.smul k

Premises used: Matrix.isDiag_one, Matrix.IsDiag.smul
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
ha : A.IsDiag
⊢ Aᵀ.IsDiag

Tactic:
fun _ _ h =>
  ha h.symm

Premises used: Matrix.IsDiag, Ne.symm, Matrix.transpose, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
⊢ Aᵀ.IsDiag ↔ A.IsDiag

Tactic:
⟨IsDiag.transpose, IsDiag.transpose⟩

Premises used: Matrix.IsDiag.transpose, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
A : Matrix n n α
ha : A.IsDiag
⊢ Aᴴ.IsDiag

Tactic:
ha.transpose.map (star_zero _)

Premises used: Matrix.IsDiag.transpose, Matrix.IsDiag.map, star_zero, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ Aᴴᴴ.IsDiag

Tactic:
ha.conjTranspose

Premises used: Matrix.IsDiag.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
h : A = Aᴴᴴ
⊢ A.IsDiag

Tactic:
convert! ha.conjTranspose

Premises used: Matrix.IsDiag.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
A : Matrix n n α
ha : Aᴴ.IsDiag
⊢ A = Aᴴᴴ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix n n α
ha : A.IsDiag
f : m → n
hf : Injective f
⊢ (A.submatrix f f).IsDiag

Tactic:
fun _ _ h => ha (hf.ne h)

Premises used: Matrix.submatrix, Function.Injective.ne, Matrix.IsDiag, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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)
⊢ ¬a = c ∨ ¬b = d

Tactic:
simp only [Prod.mk_inj, Ne, not_and_or] at h

Premises used: Prod.mk_inj, Ne, not_and_or
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
inr : ∀ (hbd : ¬b = d), 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

Tactic:
rcases h with hac | hbd
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
hac : ¬a = c
⊢ Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0

Tactic:
simp [hA hac]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
hbd : ¬b = d
⊢ Eq (α := α) (kroneckerMap (fun (x1 x2 : α) ↦ x1 * x2) A B (a, b) (c, d)) 0

Tactic:
simp [hB hbd]
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
inst : Zero α
A : Matrix n n α
h : A.IsDiag
a : ∀ (i j : n), Aᵀ i j = A i j
⊢ A.IsSymm

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
neg : ∀ (g : ¬i = j), Aᵀ i j = A i j
⊢ Aᵀ i j = A i j

Tactic:
by_cases g : i = j
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
pos₁ pos₂ : A j j = A j j
⊢ Aᵀ i j = A i j

Tactic:
rw [g, transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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

Tactic:
simp [h g, h (Ne.symm g)]

Premises used: Ne.symm
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : m
hij : Ne (α := m ⊕ n) (Sum.inl i) (Sum.inl j)
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0

Tactic:
ha (ne_of_apply_ne _ hij)

Premises used: Matrix.fromBlocks, ne_of_apply_ne, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : m
hij : Ne (α := m ⊕ n) (Sum.inl i) (Sum.inl j)
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inl j) = 0

Tactic:
exact ha (ne_of_apply_ne _ hij)

Premises used: ne_of_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : m
j : n
hij : Sum.inl i ≠ Sum.inr j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inl i) (Sum.inr j) = 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i : n
j : m
hij : Sum.inr i ≠ Sum.inl j
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inl j) = 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : n
hij : Ne (α := m ⊕ n) (Sum.inr i) (Sum.inr j)
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0

Tactic:
hd (ne_of_apply_ne _ hij)

Premises used: Matrix.fromBlocks, ne_of_apply_ne, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Zero α
A : Matrix m m α
D : Matrix n n α
ha : A.IsDiag
hd : D.IsDiag
i j : n
hij : Ne (α := m ⊕ n) (Sum.inr i) (Sum.inr j)
⊢ Matrix.fromBlocks A 0 0 D (Sum.inr i) (Sum.inr j) = 0

Tactic:
exact hd (ne_of_apply_ne _ hij)

Premises used: ne_of_apply_ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
mpr : A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag → (fromBlocks A B C D).IsDiag
⊢ (fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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

Tactic:
⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩

Premises used: And.intro, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
mp₃ : ∀ (i j : n) (hij : i ≠ j), (fun (i j : n) ↦ D i j = 0) i j
⊢ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

Tactic:
refine ⟨fun i j hij => ?_, ext fun i j => ?_, ext fun i j => ?_, fun i j hij => ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i j : m
hij : i ≠ j
⊢ (fun (i j : m) ↦ A i j = 0) i j

Tactic:
h (Sum.inl_injective.ne hij)

Premises used: Matrix.fromBlocks, Sum.inl_injective, Function.Injective.ne, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i j : m
hij : i ≠ j
⊢ (fun (i j : m) ↦ A i j = 0) i j

Tactic:
exact h (Sum.inl_injective.ne hij)

Premises used: Sum.inl_injective, Function.Injective.ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i : m
j : n
⊢ B i j = 0 i j

Tactic:
h Sum.inl_ne_inr

Premises used: Matrix.fromBlocks, Sum.inl_ne_inr, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i : m
j : n
⊢ B i j = 0 i j

Tactic:
exact h Sum.inl_ne_inr

Premises used: Sum.inl_ne_inr
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i : n
j : m
⊢ C i j = 0 i j

Tactic:
h Sum.inr_ne_inl

Premises used: Matrix.fromBlocks, Sum.inr_ne_inl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i : n
j : m
⊢ C i j = 0 i j

Tactic:
exact h Sum.inr_ne_inl

Premises used: Sum.inr_ne_inl
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i j : n
hij : i ≠ j
⊢ (fun (i j : n) ↦ D i j = 0) i j

Tactic:
h (Sum.inr_injective.ne hij)

Premises used: Matrix.fromBlocks, Sum.inr_injective, Function.Injective.ne, Sum.elim
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
i j : n
hij : i ≠ j
⊢ (fun (i j : n) ↦ D i j = 0) i j

Tactic:
exact h (Sum.inr_injective.ne hij)

Premises used: Sum.inr_injective, Function.Injective.ne
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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 α
ha : A.IsDiag
hb : B = 0
hc : C = 0
hd : D.IsDiag
⊢ (fromBlocks A 0 0 D).IsDiag

Tactic:
IsDiag.fromBlocks ha hd

Premises used: Matrix.IsDiag.fromBlocks
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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 α
ha : A.IsDiag
hb : B = 0
hc : C = 0
hd : D.IsDiag
⊢ (fromBlocks A B C D).IsDiag

Tactic:
convert! IsDiag.fromBlocks ha hd

Premises used: Matrix.IsDiag.fromBlocks
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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
rw : (Matrix.fromBlocks A 0 0ᵀ D).IsDiag
⊢ (Matrix.fromBlocks A 0 C D).IsDiag

Tactic:
rw [← (isSymm_fromBlocks_iff.1 h).2.1]

Premises used: And.right, And.left, Iff.mp, Matrix.isSymm_fromBlocks_iff
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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 0ᵀ D).IsDiag

Tactic:
ha.fromBlocks hd

Premises used: Matrix.IsDiag.fromBlocks, Matrix.transpose
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
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 0ᵀ D).IsDiag

Tactic:
exact ha.fromBlocks hd

Premises used: Matrix.IsDiag.fromBlocks
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Fintype n
inst_1 : Mul α
inst_2 : AddCommMonoid α
A : Matrix m n α
⊢ (A * Aᵀ).IsDiag ↔ A.HasOrthogonalRows

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matrix.HasOrthogonalRows, Matrix.IsDiag, Matrix.transpose, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.IsDiag
Goal:
α : Type u_1
n : Type u_4
m : Type u_5
inst : Fintype m
inst_1 : Mul α
inst_2 : AddCommMonoid α
A : Matrix m n α
⊢ (Aᵀ * A).IsDiag ↔ A.HasOrthogonalCols

Tactic:
Iff.rfl

Premises used: Iff.rfl, Matrix.HasOrthogonalRows, Matrix.IsDiag, Matrix.HasOrthogonalCols, Matrix.transpose, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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
f : α → β → γ
A : Matrix l m α
B : Matrix n p β
i : l × n
j : m × p
⊢ kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)

Tactic:
rfl

Premises used: Matrix.kroneckerMap, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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
f : α → β → γ
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f Aᵀ Bᵀ = (kroneckerMap f A B)ᵀ

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
α' : Type u_4
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
f : α' → β → γ
g : α → α'
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f (A.map g) B = kroneckerMap (fun (a : α) (b : β) ↦ f (g a) b) A B

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
β' : Type u_6
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
f : α → β' → γ
g : β → β'
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap f A (B.map g) = kroneckerMap (fun (a : α) (b : β) ↦ f a (g b)) A B

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
α : Type u_3
β : Type u_5
γ : Type u_7
γ' : Type u_8
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
f : α → β → γ
g : γ → γ'
A : Matrix l m α
B : Matrix n p β
⊢ (kroneckerMap f A B).map g = kroneckerMap (fun (a : α) (b : β) ↦ g (f a b)) A B

Tactic:
ext fun _ _ => rfl

Premises used: Matrix.ext, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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
f : α → β → γ
A : Matrix l m α
B : Matrix n p β
r : l' → l
c : m' → m
⊢ kroneckerMap f (A.submatrix r c) B = (kroneckerMap f A B).submatrix (Prod.map r id) (Prod.map c id)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.kroneckerMap, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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
n' : Type u_17
p' : Type u_18
f : α → β → γ
A : Matrix l m α
B : Matrix n p β
r : n' → n
c : p' → p
⊢ kroneckerMap f A (B.submatrix r c) = (kroneckerMap f A B).submatrix (Prod.map id r) (Prod.map id c)

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.kroneckerMap, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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 : α → β → γ
A : Matrix l m α
B : Matrix n p β
r : l' → l
c : m' → m
r' : n' → n
c' : p' → p
⊢ kroneckerMap f (A.submatrix r c) (B.submatrix r' c') = (kroneckerMap f A B).submatrix (Prod.map r r') (Prod.map c c')

Tactic:
rfl

Premises used: Matrix.submatrix, Matrix.kroneckerMap, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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 γ
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
B : Matrix n p β
⊢ Eq (α := Matrix (l × n) (m × p) γ) (kroneckerMap f 0 B) 0

Tactic:
ext fun _ _ => hf _

Premises used: Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
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 γ
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
⊢ Eq (α := Matrix (l × n) (m × p) γ) (kroneckerMap f A 0) 0

Tactic:
ext fun _ _ => hf _

Premises used: Prod.fst, Matrix.ext