awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑k : ℝ))

Tactic:
(finite_le_nat n).eventually_all.2 fun k _ => hx.eventually_forall_le_dist_cast_div k

Premises used: Iff.mpr, Set.Finite.eventually_all, Set.Mem, setOf, Irrational.eventually_forall_le_dist_cast_div, Set.finite_le_nat
-- Module: Mathlib.Topology.Instances.Irrational
Goal:
x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑k : ℝ))
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x (↑r : ℝ)

Tactic:
simpa only [Rat.cast_def] using H r.den hr r.num

Premises used: Rat.num, Rat.den, Rat.cast_def
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace R
inst_1 : T2Space R
⊢ T2Space (Matrix m n R)

Tactic:
inferInstanceAs <| T2Space (m → n → R)

Premises used: _private.0.instT2SpaceMatrix._proof_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace R
inst_1 : Finite m
inst_2 : Finite n
inst_3 : DiscreteTopology R
⊢ DiscreteTopology (Matrix m n R)

Tactic:
inferInstanceAs <| DiscreteTopology (m → n → R)

Premises used: _private.0.instDiscreteTopologyMatrixOfFinite._proof_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
n : Type u_5
R : Type u_8
inst : Finite m
inst_1 : Finite n
inst_2 : TopologicalSpace R
S : Set R
hS : IsOpen S
⊢ IsOpen (X := Matrix m n R) S.matrix

Tactic:
Set.matrix_eq_pi ▸
    (isOpen_set_pi Set.finite_univ fun _ _ =>
    isOpen_set_pi Set.finite_univ fun _ _ => hS).preimage continuous_id

Premises used: Eq.rec, isOpen_set_pi, continuous_id, Set.finite_univ, IsOpen.preimage, Eq.symm, Set.matrix_eq_pi
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace R
S : Set R
hS : IsCompact S
⊢ IsCompact (X := Matrix m n R) S.matrix

Tactic:
isCompact_pi_infinite fun _ => isCompact_pi_infinite fun _ => hS

Premises used: Set.Mem, Matrix, setOf, isCompact_pi_infinite, instTopologicalSpaceMatrix._aux_1, Set.matrix
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : SMul α R
inst_3 : ContinuousConstSMul α R
⊢ ContinuousConstSMul α (Matrix m n R)

Tactic:
inferInstanceAs (ContinuousConstSMul α (m → n → R))

Premises used: _private.0.instContinuousConstSMulMatrix._proof_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace α
inst_3 : SMul α R
inst_4 : ContinuousSMul α R
⊢ ContinuousSMul α (Matrix m n R)

Tactic:
inferInstanceAs (ContinuousSMul α (m → n → R))

Premises used: _private.0.instContinuousSMulMatrix._proof_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Add R
inst_3 : ContinuousAdd R
⊢ ContinuousAdd (Matrix m n R)

Tactic:
Pi.continuousAdd

Premises used: Matrix, instTopologicalSpaceMatrix._aux_1, Pi.continuousAdd
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Neg R
inst_3 : ContinuousNeg R
⊢ ContinuousNeg (Matrix m n R)

Tactic:
Pi.continuousNeg

Premises used: Matrix, Pi.continuousNeg, instTopologicalSpaceMatrix._aux_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : AddGroup R
inst_3 : IsTopologicalAddGroup R
⊢ IsTopologicalAddGroup (Matrix m n R)

Tactic:
Pi.topologicalAddGroup

Premises used: Matrix, Pi.topologicalAddGroup, instTopologicalSpaceMatrix._aux_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
α : Type u_2
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace R
inst_1 : TopologicalSpace α
f : α → Matrix m n R
h : ∀ (i : m) (j : n), Continuous.{u_2, u_8} (Y := R) fun (a : α) ↦ f a i j
⊢ Continuous f

Tactic:
continuous_pi fun _ => continuous_pi fun _ => h _ _

Premises used: Matrix, continuous_pi, instTopologicalSpaceMatrix._aux_1
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix m n R
hA : Continuous A
i : m
j : n
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ A x i j

Tactic:
(continuous_apply_apply i j).comp hA

Premises used: Continuous.comp, continuous_apply_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
α : Type u_2
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace R
inst_1 : TopologicalSpace α
f : α → m → n → R
⊢ (Continuous (Y := Matrix m n R) fun (x : α) ↦ (of : (a : m → n → R) → Matrix m n R) (f x)) ↔ Continuous f

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
S : Type u_7
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace S
A : X → Matrix m n S
f : S → R
hA : Continuous A
hf : Continuous f
⊢ Continuous (Y := Matrix m n R) fun (x : X) ↦ (A x).map f

Tactic:
continuous_matrix fun _ _ => hf.comp <| hA.matrix_elem _ _

Premises used: Continuous.comp, continuous_matrix, Continuous.matrix_elem
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix m n R
hA : Continuous A
⊢ Continuous (Y := Matrix n m R) fun (x : X) ↦ (A x)ᵀ

Tactic:
continuous_matrix fun i j => hA.matrix_elem j i

Premises used: continuous_matrix, Continuous.matrix_elem
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Star R
inst_3 : ContinuousStar R
A : X → Matrix m n R
hA : Continuous A
⊢ Continuous (Y := Matrix n m R) fun (x : X) ↦ (A x)ᴴ

Tactic:
hA.matrix_transpose.matrix_map continuous_star

Premises used: ContinuousStar.continuous_star, Continuous.matrix_map, Continuous.matrix_transpose, Matrix.conjTranspose
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Star R
inst_3 : ContinuousStar R
⊢ ContinuousStar (Matrix m m R)

Tactic:
⟨continuous_id.matrix_conjTranspose⟩

Premises used: Continuous.matrix_conjTranspose, ContinuousStar.mk, continuous_id
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
ι : Type u_11
A : X → n → R
hA : Continuous A
⊢ Continuous (Y := Matrix n ι R) fun (x : X) ↦ replicateCol ι (A x)

Tactic:
continuous_matrix fun i _ => (continuous_apply i).comp hA

Premises used: Continuous.comp, continuous_matrix, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
ι : Type u_11
A : X → n → R
hA : Continuous A
⊢ Continuous (Y := Matrix ι n R) fun (x : X) ↦ replicateRow ι (A x)

Tactic:
continuous_matrix fun _ _ => (continuous_apply _).comp hA

Premises used: Continuous.comp, continuous_matrix, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq n
A : X → n → R
hA : Continuous A
⊢ Continuous (Y := Matrix n n R) fun (x : X) ↦ diagonal (A x)

Tactic:
continuous_matrix fun i _ => ((continuous_apply i).comp hA).if_const _ continuous_zero

Premises used: Continuous.comp, continuous_matrix, Continuous.if_const, continuous_zero, continuous_apply, Eq
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : Mul R
inst_4 : AddCommMonoid R
inst_5 : ContinuousAdd R
inst_6 : ContinuousMul R
A B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ ∑ i : n, A x i * B x i

Tactic:
fun_prop
-- 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 : Fintype n
inst_3 : Mul R
inst_4 : AddCommMonoid R
inst_5 : ContinuousAdd R
inst_6 : ContinuousMul R
A : X → Matrix m n R
B : X → Matrix n p R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := Matrix m p R) fun (x : X) ↦ A x * B x

Tactic:
continuous_matrix fun _ _ =>
    continuous_finsetSum _ fun _ _ => (hA.matrix_elem _ _).mul (hB.matrix_elem _ _)

Premises used: Finset.univ, continuous_matrix, Continuous.matrix_elem, Continuous.mul, continuous_finsetSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
α : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
S : Type u_7
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : Mul R
inst_4 : AddCommMonoid R
inst_5 : ContinuousAdd R
inst_6 : ContinuousMul R
⊢ ContinuousMul (Matrix n n R)

Tactic:
⟨continuous_fst.matrix_mul continuous_snd⟩

Premises used: continuous_snd, continuous_fst, ContinuousMul.mk, Continuous.matrix_mul
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Mul R
inst_3 : ContinuousMul R
A : X → m → R
B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := Matrix m n R) fun (x : X) ↦ vecMulVec (A x) (B x)

Tactic:
continuous_matrix fun _ _ => ((continuous_apply _).comp hA).mul ((continuous_apply _).comp hB)

Premises used: Continuous.comp, continuous_matrix, Continuous.mul, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : NonUnitalNonAssocSemiring R
inst_3 : ContinuousAdd R
inst_4 : ContinuousMul R
inst_5 : Fintype n
A : X → Matrix m n R
B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := m → R) fun (x : X) ↦ A x *ᵥ B x

Tactic:
continuous_pi fun i => ((continuous_apply i).comp hA).dotProduct hB

Premises used: Continuous.comp, continuous_pi, Continuous.dotProduct, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : NonUnitalNonAssocSemiring R
inst_3 : ContinuousAdd R
inst_4 : ContinuousMul R
inst_5 : Fintype m
A : X → m → R
B : X → Matrix m n R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := n → R) fun (x : X) ↦ A x ᵥ* B x

Tactic:
continuous_pi fun _i => hA.dotProduct <| continuous_pi fun _j => hB.matrix_elem _ _

Premises used: Continuous.matrix_elem, continuous_pi, Continuous.dotProduct
-- 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 l n R
hA : Continuous A
e₁ : m → l
e₂ : p → n
⊢ Continuous (Y := Matrix m p R) fun (x : X) ↦ (A x).submatrix e₁ e₂

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

Premises used: continuous_matrix, 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 l n R
hA : Continuous A
e₁ : l ≃ m
e₂ : n ≃ p
⊢ Continuous (Y := Matrix m p R) fun (x : X) ↦ (reindex e₁ e₂ : (a : Matrix l n R) → Matrix m p R) (A x)

Tactic:
hA.matrix_submatrix _ _

Premises used: Matrix.submatrix, Continuous.matrix_submatrix
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous (Y := (i : n) → R) fun (x : X) ↦ (A x).diag

Tactic:
continuous_pi fun _ => hA.matrix_elem _ _

Premises used: Continuous.matrix_elem, continuous_pi
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
n : Type u_5
R : Type u_8
inst : TopologicalSpace R
⊢ Continuous (X := Matrix n n R) diag

Tactic:
show Continuous fun x : Matrix n n R => Matrix.diag x from continuous_id.matrix_diag

Premises used: continuous_id, Continuous.matrix_diag
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : AddCommMonoid R
inst_4 : ContinuousAdd R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ (A x).trace

Tactic:
continuous_finsetSum _ fun _ _ => hA.matrix_elem _ _

Premises used: Continuous.matrix_elem, Matrix.trace, continuous_finsetSum
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
simp_rw :
  Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦
    ∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A x ((σ : (a : n) → n) i) i)
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ (A x).det

Tactic:
simp_rw [Matrix.det_apply]

Premises used: Matrix.det_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦
    ∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A x ((σ : (a : n) → n) i) i)

Tactic:
continuous_finsetSum _ fun l _ => Continuous.const_smul ?_ _

Premises used: Equiv.Perm.sign, continuous_finsetSum, Continuous.const_smul, DFunLike.coe
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
refine :
  ∀ (l : Equiv.Perm n),
    Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ l →
      Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ ∏ i : n, A x ((l : (a : n) → n) i) i
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦
    ∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A x ((σ : (a : n) → n) i) i)

Tactic:
refine continuous_finsetSum _ fun l _ => Continuous.const_smul ?_ _

Premises used: continuous_finsetSum, Continuous.const_smul
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
h : Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ l
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ ∏ i : n, A x ((l : (a : n) → n) i) i

Tactic:
continuous_finsetProd _ fun l _ => hA.matrix_elem _ _

Premises used: Continuous.matrix_elem, continuous_finsetProd, DFunLike.coe
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
h : Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ l
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ ∏ i : n, A x ((l : (a : n) → n) i) i

Tactic:
exact continuous_finsetProd _ fun l _ => hA.matrix_elem _ _

Premises used: Continuous.matrix_elem, continuous_finsetProd
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : DecidableEq n
i : n
A : X → Matrix m n R
B : X → m → R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := Matrix m n R) fun (x : X) ↦ (A x).updateCol i (B x)

Tactic:
continuous_matrix fun _j k =>
    (continuous_apply k).comp <|
      ((continuous_apply _).comp hA).update i ((continuous_apply _).comp hB)

Premises used: Continuous.comp, continuous_matrix, Continuous.update, continuous_apply
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : DecidableEq m
i : m
A : X → Matrix m n R
B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := Matrix m n R) fun (x : X) ↦ (A x).updateRow i (B x)

Tactic:
hA.update i hB

Premises used: Function.update, Matrix, dite, Continuous.update, instTopologicalSpaceMatrix._aux_1, Matrix.updateRow
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous (Y := n → R) fun (x : X) ↦ ((A x).cramer : (a : n → R) → n → R) (B x)

Tactic:
continuous_pi fun _ => (hA.matrix_updateCol _ hB).matrix_det

Premises used: continuous_pi, Continuous.matrix_det, Continuous.matrix_updateCol
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous (Y := Matrix n n R) fun (x : X) ↦ (A x).adjugate

Tactic:
continuous_matrix fun _j k =>
    (hA.matrix_transpose.matrix_updateCol k continuous_const).matrix_det

Premises used: continuous_const, continuous_matrix, Continuous.matrix_det, Continuous.matrix_updateCol, Continuous.matrix_transpose
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
n : Type u_5
R : Type u_8
inst : TopologicalSpace R
inst_1 : Fintype n
inst_2 : DecidableEq n
inst_3 : CommRing R
inst_4 : IsTopologicalRing R
A : Matrix n n R
h : ContinuousAt Ring.inverse A.det
⊢ ContinuousAt Inv.inv A

Tactic:
(h.comp continuous_id.matrix_det.continuousAt).smul continuous_id.matrix_adjugate.continuousAt

Premises used: Continuous.matrix_adjugate, ContinuousAt.smul, Continuous.matrix_det, Ring.inverse, dite, Continuous.continuousAt, continuous_id, ContinuousAt.comp
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_11
n : Type u_12
R : Type u_13
S : Type u_14
inst : TopologicalSpace R
inst_1 : TopologicalSpace S
f : R → S
hf : IsInducing f
⊢ IsInducing (Y := Matrix m n S) fun (x : Matrix m n R) ↦ x.map f

Tactic:
IsInducing.piMap fun _ : m ↦ (IsInducing.piMap fun _ : n ↦ hf)

Premises used: Matrix, Pi.map, instTopologicalSpaceMatrix._aux_1, Matrix.map, Topology.IsInducing.piMap
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_11
n : Type u_12
R : Type u_13
S : Type u_14
inst : TopologicalSpace R
inst_1 : TopologicalSpace S
f : R → S
hf : IsEmbedding f
⊢ IsEmbedding (Y := Matrix m n S) fun (x : Matrix m n R) ↦ x.map f

Tactic:
IsEmbedding.piMap fun _ : m ↦ (IsEmbedding.piMap fun _ : n ↦ hf)

Premises used: Matrix, Pi.map, Topology.IsEmbedding.piMap, instTopologicalSpaceMatrix._aux_1, Matrix.map
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_11
n : Type u_12
R : Type u_13
S : Type u_14
inst : TopologicalSpace R
inst_1 : TopologicalSpace S
f : R → S
hf : IsClosedEmbedding f
⊢ IsClosedEmbedding (Y := Matrix m n S) fun (x : Matrix m n R) ↦ x.map f

Tactic:
IsClosedEmbedding.piMap fun _ : m ↦ (IsClosedEmbedding.piMap fun _ : n ↦ hf)

Premises used: Matrix, Topology.IsClosedEmbedding.piMap, Pi.map, instTopologicalSpaceMatrix._aux_1, Matrix.map
-- Module: Mathlib.Topology.Instances.Matrix
Goal:
m : Type u_11
n : Type u_12
R : Type u_13
S : Type u_14
inst : TopologicalSpace R
inst_1 : TopologicalSpace S
f : R → S
inst_2 : Finite m
inst_3 : Finite n
hf : IsOpenEmbedding f
⊢ IsOpenEmbedding (Y := Matrix m n S) fun (x : Matrix m n R) ↦ x.map f

Tactic:
IsOpenEmbedding.piMap fun _ : m ↦ (IsOpenEmbedding.piMap fun _ : n ↦ hf)

Premises used: Matrix, Topology.IsOpenEmbedding.piMap, Pi.map, instTopologicalSpaceMatrix._aux_1, Matrix.map
-- 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.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl i) (Sum.inl 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 : n
j : l
inl : Continuous A
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl 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 : n
j : m
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl 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 : n
j : m
inl : Continuous B
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl 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 : p
j : l
⊢ 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:
Continuous.matrix_elem ?_ i j

Premises used: Matrix.fromBlocks, Continuous.matrix_elem, Sum.elim