awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
right :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
right₁ :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
right :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
right₁ :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [continuous_const, continuous_neg, continuous_id']

Premises used: ContinuousNeg.continuous_neg, continuous_const, continuous_id'
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [continuous_const, continuous_neg, continuous_id']

Premises used: ContinuousNeg.continuous_neg, continuous_const, continuous_id'
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [continuous_const, continuous_neg, continuous_id']

Premises used: ContinuousNeg.continuous_neg, continuous_const, continuous_id'
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [continuous_const, continuous_neg, continuous_id']

Premises used: ContinuousNeg.continuous_neg, continuous_const, continuous_id'
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
α : Type u_4
inst_4 : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst_4, instTopologicalSpace] f
i : n
⊢ Continuous[instTopologicalSpaceMatrix, Pi.topologicalSpace] fun (A : Matrix n n R) ↦ A i

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
α : Type u_4
inst_4 : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst_4, instTopologicalSpace] f
i : n
⊢ Continuous[inst_4, instTopologicalSpaceMatrix] fun (x : α) ↦ (↑(f x) : Matrix n n R)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : Continuous[inst_3, inst_5] (⇑f : (a : R) → S)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (⇑(map f) : (a : SL n R) → SL n S)

Tactic:
IsInducing.subtypeVal.continuous_iff.mpr ?_

Premises used: Iff.mpr, Matrix.SpecialLinearGroup, Set.Mem, Topology.IsInducing.continuous_iff, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : Continuous[inst_3, inst_5] (⇑f : (a : R) → S)
refine :
  Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
    (Function.comp (β :=
      { x : Matrix n n S // Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x })
      (Subtype.val (p := fun (x : Matrix n n S) ↦
        Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x))
      (⇑(map f) : (a : SL n R) → SL n S))
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (⇑(map f) : (a : SL n R) → SL n S)

Tactic:
refine IsInducing.subtypeVal.continuous_iff.mpr ?_

Premises used: Iff.mpr, Topology.IsInducing.continuous_iff, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : Continuous[inst_3, inst_5] (⇑f : (a : R) → S)
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
    (Function.comp (β :=
      { x : Matrix n n S // Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x })
      (Subtype.val (p := fun (x : Matrix n n S) ↦
        Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x))
      (⇑(map f) : (a : SL n R) → SL n S))

Tactic:
(continuous_id.matrix_map hf).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, Continuous.matrix_map, continuous_id, Matrix.map
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : Continuous[inst_3, inst_5] (⇑f : (a : R) → S)
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
    (Function.comp (β :=
      { x : Matrix n n S // Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x })
      (Subtype.val (p := fun (x : Matrix n n S) ↦
        Membership.mem (γ := Set (Matrix n n S)) (fun (x : Matrix n n S) ↦ x.det = 1) x))
      (⇑(map f) : (a : SL n R) → SL n S))

Tactic:
exact (continuous_id.matrix_map hf).comp continuous_subtype_val

Premises used: continuous_subtype_val, Continuous.comp, Continuous.matrix_map, continuous_id
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : IsInducing.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (⇑(map f) : (a : SL n R) → SL n S)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
hf : IsEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] (⇑(map f) : (a : SL n R) → SL n S)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
inst_6 : IsTopologicalRing R
inst_7 : DiscreteTopology R
⊢ DiscreteTopology (SL n R)

Tactic:
inferInstanceAs <| DiscreteTopology (Subtype _)

Premises used: _private.0.Matrix.SpecialLinearGroup.instDiscreteTopology._proof_1
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : T1Space R
⊢ IsClosedEmbedding (X := { A : Matrix n n R // A.det = 1 }) (Subtype.val (p := fun (A : Matrix n n R) ↦ A.det = 1))

Tactic:
(isClosed_singleton.preimage continuous_id.matrix_det).isClosedEmbedding_subtypeVal

Premises used: Set.Mem, setOf, Continuous.matrix_det, continuous_id, Set.preimage, Set.singleton, IsClosed.preimage, IsClosed.isClosedEmbedding_subtypeVal, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
inst_6 : IsTopologicalRing R
inst_7 : T1Space R
hf : IsClosedEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ IsClosedEmbedding (X := SL n R) (Y := SL n S) (⇑(map f) : (a : SL n R) → SL n S)

Tactic:
(hf.matrix_map.comp isClosedEmbedding_val).of_comp .subtypeVal

Premises used: Topology.IsClosedEmbedding.comp, Matrix.SpecialLinearGroup.isClosedEmbedding_val, Topology.IsEmbedding.subtypeVal, Topology.IsClosedEmbedding.of_comp, Topology.IsClosedEmbedding.matrix_map
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
f : R →+* S
inst_6 : IsTopologicalRing R
inst_7 : T1Space R
⊢ T1Space (SL n R)

Tactic:
isClosedEmbedding_val.isEmbedding.t1Space

Premises used: Matrix.SpecialLinearGroup, Topology.IsClosedEmbedding.isEmbedding, Topology.IsEmbedding.t1Space, Matrix.SpecialLinearGroup.isClosedEmbedding_val
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
simp_rw :
  Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
      (Function.comp (β := (Matrix n n R)ˣ) Units.val (⇑toGL : (a : SL n R) → GL n R)) ∧
    Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
      (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)
⊢ Continuous[instTopologicalSpace, Units.instTopologicalSpaceUnits] (⇑toGL : (a : SL n R) → GL n R)

Tactic:
simp_rw [Units.continuous_iff, ← map_inv]

Premises used: map_inv, Units.continuous_iff
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
left :
  Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
    (Function.comp (β := (Matrix n n R)ˣ) Units.val (⇑toGL : (a : SL n R) → GL n R))
right :
  Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
    (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
      (Function.comp (β := (Matrix n n R)ˣ) Units.val (⇑toGL : (a : SL n R) → GL n R)) ∧
    Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
      (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
    (Function.comp (β := (Matrix n n R)ˣ) Units.val (⇑toGL : (a : SL n R) → GL n R))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
    (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
⊢ IsInducing (X := SL n R) (Y := GL n R) (⇑toGL : (a : SL n R) → GL n R)

Tactic:
.of_comp continuous_toGL Units.continuous_val (IsInducing.induced _)

Premises used: Matrix.SpecialLinearGroup.continuous_toGL, Units.continuous_val, Topology.IsInducing.induced, Topology.IsInducing.of_comp
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
⊢ IsEmbedding (X := SL n R) (Y := GL n R) (⇑toGL : (a : SL n R) → GL n R)

Tactic:
⟨isInducing_toGL, toGL_injective⟩

Premises used: Matrix.SpecialLinearGroup.toGL_injective, Matrix.SpecialLinearGroup.isInducing_toGL, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
A : Type u_4
inst_2 : CommRing A
h :
  ∀ (x : GL n A),
    Membership.mem (γ := Set (GL n A)) (Set.range (ι := SL n A) (⇑toGL : (a : SL n A) → GL n A)) x ↔
      Membership.mem (γ := Set (GL n A)) (Set.preimage (β := Aˣ) (⇑GeneralLinearGroup.det : (a : GL n A) → Aˣ) {1}) x
⊢ Eq (α := Set (GL n A)) (Set.range (ι := SL n A) (⇑toGL : (a : SL n A) → GL n A))
    (Set.preimage (β := Aˣ) (⇑GeneralLinearGroup.det : (a : GL n A) → Aˣ) {1})

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
A : Type u_4
inst_2 : CommRing A
x : GL n A
h : ∃ (y : SL n A), (↑y : Matrix n n A) = (↑x : Matrix n n A)
y : SL n A
hy : (↑y : Matrix n n A) = (↑x : Matrix n n A)
⊢ (↑x : Matrix n n A).det = 1

Tactic:
simp [← hy]
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
A : Type u_4
inst_2 : CommRing A
x : GL n A
⊢ Membership.mem (γ := Set (GL n A)) (Set.range (ι := SL n A) (⇑toGL : (a : SL n A) → GL n A)) x ↔
    Membership.mem (γ := Set (GL n A)) (Set.preimage (β := Aˣ) (⇑GeneralLinearGroup.det : (a : GL n A) → Aˣ) {1}) x

Tactic:
simpa [Units.ext_iff] using ⟨fun ⟨y, hy⟩ ↦ by simp [← hy], fun hx ↦ ⟨⟨x, hx⟩, rfl⟩⟩

Premises used: Units.ext_iff
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : T0Space R
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits]
    (⇑GeneralLinearGroup.det : (a : GL n R) → Rˣ)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : IsTopologicalRing R
inst_5 : T0Space R
⊢ IsClosed[Units.instTopologicalSpaceUnits] (Set.range (ι := SL n R) (⇑toGL : (a : SL n R) → GL n R))

Tactic:
simpa [range_toGL] using isClosed_singleton.preimage <| by fun_prop

Premises used: Matrix.SpecialLinearGroup.range_toGL, IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
inst_6 : Algebra R S
inst_7 : IsTopologicalRing S
inst_8 : ContinuousSMul R S
⊢ Continuous[instTopologicalSpace, Units.instTopologicalSpaceUnits] (⇑(mapGL S) : (a : SL n R) → GL n S)

Tactic:
continuous_toGL.comp
    (continuous_algebraMap_iff_smul R S |>.2 continuous_smul).specialLinearGroup_map

Premises used: Iff.mpr, Matrix.SpecialLinearGroup.continuous_toGL, Continuous.comp, continuous_algebraMap_iff_smul, Continuous.specialLinearGroup_map, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
inst_6 : Algebra R S
inst_7 : IsTopologicalRing S
h : IsInducing.{u_2, u_3} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsInducing (X := SL n R) (Y := GL n S) (⇑(mapGL S) : (a : SL n R) → GL n S)

Tactic:
isInducing_toGL.comp h.specialLinearGroup_map

Premises used: Topology.IsInducing.comp, Topology.IsInducing.specialLinearGroup_map, Matrix.SpecialLinearGroup.isInducing_toGL
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
inst_6 : Algebra R S
inst_7 : IsTopologicalRing S
h : IsEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsEmbedding (X := SL n R) (Y := GL n S) (⇑(mapGL S) : (a : SL n R) → GL n S)

Tactic:
isEmbedding_toGL.comp h.specialLinearGroup_map

Premises used: Topology.IsEmbedding.specialLinearGroup_map, Topology.IsEmbedding.comp, Matrix.SpecialLinearGroup.isEmbedding_toGL
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
n : Type u_1
R : Type u_2
S : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
inst_3 : TopologicalSpace R
inst_4 : CommRing S
inst_5 : TopologicalSpace S
inst_6 : Algebra R S
inst_7 : IsTopologicalRing S
inst_8 : IsTopologicalRing R
inst_9 : T1Space R
inst_10 : T1Space S
h : IsClosedEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsClosedEmbedding (X := SL n R) (Y := GL n S) (⇑(mapGL S) : (a : SL n R) → GL n S)

Tactic:
isClosedEmbedding_toGL.comp h.specialLinearGroup_map

Premises used: Matrix.SpecialLinearGroup.isClosedEmbedding_toGL, Topology.IsClosedEmbedding.comp, Topology.IsClosedEmbedding.specialLinearGroup_map
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
exists_closed_nhds_one_inv_eq_mul_subset hU

Premises used: exists_closed_nhds_one_inv_eq_mul_subset
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
obtain :
  ∀ (V : Set G) (V_mem : Membership.mem (γ := Filter G) (𝓝 1) V) (V_closed : IsClosed[inst] V) (V_symm : V⁻¹ = V)
    (VU : V * V ⊆ U), HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
obtain ⟨V, V_mem, V_closed, V_symm, VU⟩ : ∃ V ∈ 𝓝 (1 : G), IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U :=
    exists_closed_nhds_one_inv_eq_mul_subset hU

Premises used: nhds, exists_closed_nhds_one_inv_eq_mul_subset, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
x_1 : G
⊢ x_1 • V ∈ 𝓝 x_1

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
obtain :
  ∀ (s : Set G) (s_count : s.Countable) (hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ),
    HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
obtain ⟨s, s_count, hs⟩ : ∃ (s : Set G), s.Countable ∧ ⋃ g ∈ s, g • V = univ :=
    countable_cover_nhds_of_sigmaCompact fun _ ↦ by simpa

Premises used: Set.univ, countable_cover_nhds_of_sigmaCompact, Set
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
⊢ Nonempty X

Tactic:
have : Nonempty X := ⟨x⟩
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this : Nonempty X
have : ∀ (this : Encodable (↑s : Type u_1)), ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty

Tactic:
have : Encodable s := Countable.toEncodable s_count
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
this_1 : Nonempty X
this : Encodable (↑s : Type u_1)
hc : ∀ (i : ℕ × (↑s : Type u_1)), IsClosed[inst_1] (F i)
hU₁ : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) univ
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty

Tactic:
apply nonempty_interior_of_iUnion_of_closed

Premises used: nonempty_interior_of_iUnion_of_closed