awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
inr : Continuous C
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inl j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Premises used: Continuous.matrix_elem
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inr j)

Tactic:
Continuous.matrix_elem ?_ i j

Premises used: Matrix.fromBlocks, Continuous.matrix_elem, Sum.elim
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
inr : Continuous D
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inr j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Premises used: Continuous.matrix_elem
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous A

Tactic:
assumption
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous B

Tactic:
assumption
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous C

Tactic:
assumption
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous D

Tactic:
assumption
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq p
A : X → p → Matrix m n R
hA : Continuous A
⊢ Continuous (Y := Matrix (m × p) (n × p) R) fun (x : X) ↦ blockDiagonal (A x)

Tactic:
continuous_matrix fun ⟨i₁, i₂⟩ ⟨j₁, _j₂⟩ =>
    (((continuous_apply i₂).comp hA).matrix_elem i₁ j₁).if_const _ continuous_zero

Premises used: Continuous, Matrix.blockDiagonal, Continuous.comp, continuous_matrix, Continuous.matrix_elem, Continuous.if_const, Prod.mk, continuous_zero, continuous_apply, _private.0.Continuous.matrix_blockDiagonal.match_1, Eq
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix (m × p) (n × p) R
hA : Continuous A
⊢ Continuous (Y := (k : p) → Matrix m n R) fun (x : X) ↦ (A x).blockDiag

Tactic:
continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _

Premises used: continuous_matrix, Continuous.matrix_elem, continuous_pi, Prod.mk
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
dsimp : Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦
    blockDiagonal' (m' := m') (n' := n') (A a) (Sigma.mk (β := fun (i : l) ↦ m' i) i₁ i₂)
      (Sigma.mk (β := fun (i : l) ↦ n' i) j₁ j₂)

Tactic:
dsimp only [blockDiagonal'_apply']

Premises used: Matrix.blockDiagonal'_apply'
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
pos : ∀ (h : i₁ = j₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)
neg : ∀ (h : ¬i₁ = j₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ 0
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : i₁ = j₁
pos : ∀ (j₂ : n' i₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)

Tactic:
subst h
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₂ : n' i₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)

Tactic:
((continuous_apply i₁).comp hA).matrix_elem i₂ j₂

Premises used: Continuous.comp, Continuous.matrix_elem, cast, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₂ : n' i₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)

Tactic:
exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂

Premises used: Continuous.comp, Continuous.matrix_elem, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : ¬i₁ = j₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ 0

Tactic:
continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : ¬i₁ = j₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ 0

Tactic:
exact continuous_const

Premises used: continuous_const
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R
hA : Continuous A
⊢ Continuous (Y := (k : l) → Matrix.{u_9, u_10, u_8} (m' k) (n' k) R) fun (x : X) ↦
    (A x).blockDiag' (m' := m') (n' := n')

Tactic:
continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _

Premises used: continuous_matrix, Continuous.matrix_elem, continuous_pi, Sigma.mk
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
simp : IsClosed (X := Matrix m m R) (⋂ (i : m), ⋂ (i_1 : m), ⋂ (_ : b i_1 < b i), {x : Matrix m m R | x i i_1 = 0})
⊢ IsClosed (X := Matrix m m R) {M : Matrix m m R | M.BlockTriangular b}

Tactic:
simp only [BlockTriangular, Set.setOf_forall]

Premises used: Matrix.BlockTriangular, Set.setOf_forall
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
⊢ IsClosed (X := Matrix m m R) (⋂ (i : m), ⋂ (i_1 : m), ⋂ (_ : b i_1 < b i), {x : Matrix m m R | x i i_1 = 0})

Tactic:
isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun _ => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
refine : ∀ (i j : m), b j < b i → IsClosed (X := Matrix m m R) {x : Matrix m m R | x i j = 0}
⊢ IsClosed (X := Matrix m m R) (⋂ (i : m), ⋂ (i_1 : m), ⋂ (_ : b i_1 < b i), {x : Matrix m m R | x i i_1 = 0})

Tactic:
refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun _ => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
i j : m
h : b j < b i
⊢ IsClosed (X := Matrix m m R) {x : Matrix m m R | x i j = 0}

Tactic:
isClosed_eq (continuous_id.matrix_elem i j) continuous_const

Premises used: continuous_const, Continuous.matrix_elem, continuous_id, isClosed_eq
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
i j : m
h : b j < b i
⊢ IsClosed (X := Matrix m m R) {x : Matrix m m R | x i j = 0}

Tactic:
exact isClosed_eq (continuous_id.matrix_elem i j) continuous_const

Premises used: continuous_const, Continuous.matrix_elem, continuous_id, isClosed_eq
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix m n R
a : Matrix m n R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ (f x)ᵀ) aᵀ L

Tactic:
(hf.map (Matrix.transposeAddEquiv m n R) continuous_id.matrix_transpose :)

Premises used: HasSum.map, continuous_id, Matrix.transpose, Continuous.matrix_transpose, Matrix.transposeAddEquiv
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix m n R
hf : Summable f L
⊢ Summable (α := Matrix n m R) (fun (x : X) ↦ (f x)ᵀ) L

Tactic:
hf.hasSum.matrix_transpose.summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.matrix_transpose
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix m n R
⊢ Summable (α := Matrix n m R) (fun (x : X) ↦ (f x)ᵀ) L ↔ Summable f L

Tactic:
Summable.map_iff_of_equiv (Matrix.transposeAddEquiv m n R)
    continuous_id.matrix_transpose continuous_id.matrix_transpose

Premises used: continuous_id, Matrix.transpose, Continuous.matrix_transpose, Summable.map_iff_of_equiv, Matrix.transposeAddEquiv
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : T2Space R
f : X → Matrix m n R
⊢ Eq (α := Matrix n m R) (∑'[L] (x : X), f x)ᵀ (∑'[L] (x : X), (f x)ᵀ)

Tactic:
Function.LeftInverse.map_tsum f (g := transposeAddEquiv m n R) continuous_id.matrix_transpose
    continuous_id.matrix_transpose transpose_transpose

Premises used: Function.LeftInverse.map_tsum, Matrix.transpose_transpose, continuous_id, tsum, Matrix.transpose, Continuous.matrix_transpose
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : StarAddMonoid R
inst_3 : ContinuousStar R
f : X → Matrix m n R
a : Matrix m n R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ (f x)ᴴ) aᴴ L

Tactic:
(hf.map (Matrix.conjTransposeAddEquiv m n R) continuous_id.matrix_conjTranspose :)

Premises used: HasSum.map, Continuous.matrix_conjTranspose, continuous_id, Matrix.map, Matrix.conjTranspose, Matrix.conjTransposeAddEquiv
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : StarAddMonoid R
inst_3 : ContinuousStar R
f : X → Matrix m n R
hf : Summable f L
⊢ Summable (α := Matrix n m R) (fun (x : X) ↦ (f x)ᴴ) L

Tactic:
hf.hasSum.matrix_conjTranspose.summable

Premises used: HasSum.matrix_conjTranspose, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : StarAddMonoid R
inst_3 : ContinuousStar R
f : X → Matrix m n R
⊢ Summable (α := Matrix n m R) (fun (x : X) ↦ (f x)ᴴ) L ↔ Summable f L

Tactic:
Summable.map_iff_of_equiv (Matrix.conjTransposeAddEquiv m n R)
    continuous_id.matrix_conjTranspose continuous_id.matrix_conjTranspose

Premises used: Continuous.matrix_conjTranspose, continuous_id, Matrix.map, Matrix.conjTranspose, Summable.map_iff_of_equiv, Matrix.conjTransposeAddEquiv
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : StarAddMonoid R
inst_3 : ContinuousStar R
inst_4 : T2Space R
f : X → Matrix m n R
⊢ Eq (α := Matrix n m R) (∑'[L] (x : X), f x)ᴴ (∑'[L] (x : X), (f x)ᴴ)

Tactic:
Function.LeftInverse.map_tsum f (g := conjTransposeAddEquiv m n R)
    continuous_id.matrix_conjTranspose continuous_id.matrix_conjTranspose
    conjTranspose_conjTranspose

Premises used: Function.LeftInverse.map_tsum, Continuous.matrix_conjTranspose, continuous_id, Matrix.map, Matrix.conjTranspose, Matrix.conjTranspose_conjTranspose
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq n
f : X → n → R
a : n → R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ diagonal (f x)) (diagonal a) L

Tactic:
hf.map (diagonalAddMonoidHom n R) continuous_id.matrix_diagonal

Premises used: Matrix.diagonalAddMonoidHom, HasSum.map, continuous_id, Continuous.matrix_diagonal, Matrix.diagonal
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq n
f : X → n → R
hf : Summable f L
⊢ Summable (α := Matrix n n R) (fun (x : X) ↦ diagonal (f x)) L

Tactic:
hf.hasSum.matrix_diagonal.summable

Premises used: HasSum.matrix_diagonal, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq n
f : X → n → R
⊢ Summable (α := Matrix n n R) (fun (x : X) ↦ diagonal (f x)) L ↔ Summable f L

Tactic:
Summable.map_iff_of_leftInverse (Matrix.diagonalAddMonoidHom n R) (Matrix.diagAddMonoidHom n R)
    continuous_id.matrix_diagonal continuous_matrix_diag fun A => diag_diagonal A

Premises used: Matrix.diagonalAddMonoidHom, Summable.map_iff_of_leftInverse, Matrix.diag_diagonal, Matrix.diagAddMonoidHom, continuous_matrix_diag, continuous_id, Continuous.matrix_diagonal, Matrix.diagonal
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq n
inst_3 : T2Space R
f : X → n → R
⊢ Eq (α := Matrix n n R) (diagonal (∑'[L] (x : X), f x)) (∑'[L] (x : X), diagonal (f x))

Tactic:
Function.LeftInverse.map_tsum f (g := diagonalAddMonoidHom n R)
    continuous_id.matrix_diagonal continuous_matrix_diag diag_diagonal

Premises used: Function.LeftInverse.map_tsum, Matrix.diag_diagonal, continuous_matrix_diag, continuous_id, Continuous.matrix_diagonal, Matrix.diagonal
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix n n R
a : Matrix n n R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ (f x).diag) a.diag L

Tactic:
hf.map (diagAddMonoidHom n R) continuous_matrix_diag

Premises used: Matrix.diag, HasSum.map, Matrix.diagAddMonoidHom, continuous_matrix_diag
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix n n R
hf : Summable f L
⊢ Summable (α := (i : n) → R) (fun (x : X) ↦ (f x).diag) L

Tactic:
hf.hasSum.matrix_diag.summable

Premises used: HasSum.matrix_diag, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq p
f : X → p → Matrix m n R
a : p → Matrix m n R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ blockDiagonal (f x)) (blockDiagonal a) L

Tactic:
hf.map (blockDiagonalAddMonoidHom m n p R) continuous_id.matrix_blockDiagonal

Premises used: HasSum.map, Matrix.blockDiagonal, Matrix.blockDiagonalAddMonoidHom, Continuous.matrix_blockDiagonal, continuous_id
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq p
f : X → p → Matrix m n R
hf : Summable f L
⊢ Summable (α := Matrix (m × p) (n × p) R) (fun (x : X) ↦ blockDiagonal (f x)) L

Tactic:
hf.hasSum.matrix_blockDiagonal.summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.matrix_blockDiagonal
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq p
f : X → p → Matrix m n R
⊢ Summable (α := Matrix (m × p) (n × p) R) (fun (x : X) ↦ blockDiagonal (f x)) L ↔ Summable f L

Tactic:
Summable.map_iff_of_leftInverse (blockDiagonalAddMonoidHom m n p R)
    (blockDiagAddMonoidHom m n p R) continuous_id.matrix_blockDiagonal
    continuous_id.matrix_blockDiag fun A => blockDiag_blockDiagonal A

Premises used: Continuous.matrix_blockDiag, Summable.map_iff_of_leftInverse, Matrix.blockDiagonal, Matrix.blockDiagonalAddMonoidHom, Matrix.blockDiag_blockDiagonal, Continuous.matrix_blockDiagonal, continuous_id, Matrix.blockDiagAddMonoidHom
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq p
inst_3 : T2Space R
f : X → p → Matrix m n R
⊢ Eq (α := Matrix (m × p) (n × p) R) (blockDiagonal (∑'[L] (x : X), f x)) (∑'[L] (x : X), blockDiagonal (f x))

Tactic:
Function.LeftInverse.map_tsum (g := blockDiagonalAddMonoidHom m n p R) f
    continuous_id.matrix_blockDiagonal continuous_id.matrix_blockDiag blockDiag_blockDiagonal

Premises used: Continuous.matrix_blockDiag, Function.LeftInverse.map_tsum, Matrix.blockDiagonal, Matrix.blockDiag_blockDiagonal, Continuous.matrix_blockDiagonal, continuous_id
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix (m × p) (n × p) R
a : Matrix (m × p) (n × p) R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ (f x).blockDiag) a.blockDiag L

Tactic:
(hf.map (blockDiagAddMonoidHom m n p R) <| Continuous.matrix_blockDiag continuous_id :)

Premises used: Continuous.matrix_blockDiag, HasSum.map, Matrix.blockDiag, continuous_id, Matrix.blockDiagAddMonoidHom
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
f : X → Matrix (m × p) (n × p) R
hf : Summable f L
⊢ Summable (α := (k : p) → Matrix m n R) (fun (x : X) ↦ (f x).blockDiag) L

Tactic:
hf.hasSum.matrix_blockDiag.summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.matrix_blockDiag
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq l
f : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
a : (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hf : HasSum f a L
⊢ HasSum (fun (x : X) ↦ blockDiagonal' (m' := m') (n' := n') (f x)) (blockDiagonal' (m' := m') (n' := n') a) L

Tactic:
hf.map (blockDiagonal'AddMonoidHom m' n' R) continuous_id.matrix_blockDiagonal'

Premises used: HasSum.map, continuous_id, Matrix.blockDiagonal'AddMonoidHom, Matrix.blockDiagonal', Continuous.matrix_blockDiagonal'
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq l
f : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hf : Summable f L
⊢ Summable (α := Matrix ((i : l) × m' i) ((i : l) × n' i) R) (fun (x : X) ↦ blockDiagonal' (m' := m') (n' := n') (f x))
    L

Tactic:
hf.hasSum.matrix_blockDiagonal'.summable

Premises used: HasSum.matrix_blockDiagonal', HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : AddCommMonoid R
inst_1 : TopologicalSpace R
L : SummationFilter X
inst_2 : DecidableEq l
f : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
⊢ Summable (α := Matrix ((i : l) × m' i) ((i : l) × n' i) R) (fun (x : X) ↦ blockDiagonal' (m' := m') (n' := n') (f x))
      L ↔
    Summable f L

Tactic:
Summable.map_iff_of_leftInverse (blockDiagonal'AddMonoidHom m' n' R)
    (blockDiag'AddMonoidHom m' n' R) continuous_id.matrix_blockDiagonal'
    continuous_id.matrix_blockDiag' fun A => blockDiag'_blockDiagonal' A

Premises used: Summable.map_iff_of_leftInverse, Matrix.blockDiag'AddMonoidHom, Matrix.blockDiag'_blockDiagonal', continuous_id, Continuous.matrix_blockDiag', Matrix.blockDiagonal'AddMonoidHom, Matrix.blockDiagonal', Continuous.matrix_blockDiagonal'