awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (hypothesis)
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
h : G.Commensurable H
this : (G ⊓ H).IsFiniteRelIndex H
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α
have this₁ : (G ⊓ H).IsFiniteRelIndex G
Tactic: have : IsFiniteRelIndex (G ⊓ H) G := ⟨Subgroup.inf_relIndex_left G H ▸ h.2⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (hypothesis)
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous[instTopologicalSpaceProd, g.toTopologicalSpace] fun (p : α × α) ↦ p.1 * p.2
have this₁ : IsTopologicalGroup α
Tactic: haveI := g.toIsTopologicalGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (hypothesis)
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous[g.toTopologicalSpace, g.toTopologicalSpace] Inv.inv
have this₁ : IsTopologicalGroup α
Tactic: haveI := g.toIsTopologicalGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (goal)
Goal:
α : Type u
inst : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
⊢ f = g
have mk : ∀ (toTopologicalSpace : TopologicalSpace α) (toIsTopologicalGroup : IsTopologicalGroup α)
  (h :
    { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup :
          GroupTopology α }.toTopologicalSpace =
      g.toTopologicalSpace),
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup : GroupTopology α } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (goal)
Goal:
α : Type u
inst : Group α
g : GroupTopology α
toTopologicalSpace : TopologicalSpace α
toIsTopologicalGroup : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup :
        GroupTopology α }.toTopologicalSpace =
    g.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup : GroupTopology α } = g
have mk : ∀ (toTopologicalSpace_1 : TopologicalSpace α) (toIsTopologicalGroup_1 : IsTopologicalGroup α)
  (h :
    { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup :
          GroupTopology α }.toTopologicalSpace =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalGroup := toIsTopologicalGroup_1 :
          GroupTopology α }.toTopologicalSpace),
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup : GroupTopology α } =
    { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalGroup := toIsTopologicalGroup_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (hypothesis)
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Group α
_t : TopologicalSpace α := ⊥
⊢ Continuous[instTopologicalSpaceProd, _t] fun (p : α × α) ↦ p.1 * p.2
have this : DiscreteTopology α
Tactic: haveI := discreteTopology_bot α
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.GroupTopology (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst : Group β
f : α → β
⊢ Continuous[t, (coinduced f).toTopologicalSpace] f
have rw : ∀ (t_1 : TopologicalSpace β),
  Membership.mem (γ := Set (TopologicalSpace β))
      (image (α := GroupTopology β) toTopologicalSpace
        {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace})
      t_1 →
    Continuous[t, _] f
Tactic: rw [continuous_sInf_rng]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] (⇑det : (a : GL n R) → Rˣ)
have simp_rw : Continuous[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ)) ∧
  Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : R)
Tactic: simp_rw [Units.continuous_iff, ← map_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ)) ∧
    Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : R)
have left : Continuous[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ))
⊢ Continuous[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ)) ∧
    Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : R)
have right : Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, Units.instTopologicalSpaceUnits] (⇑upperRightHom : (a : R) → GL (Fin 2) R)
have simp : (Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]) ∧
  Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]
Tactic: simp only [continuous_induced_rng, Function.comp_def, upperRightHom_apply,
    Units.embedProduct_apply, Units.inv_mk, continuous_prodMk, MulOpposite.unop_op]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ (Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]) ∧
    Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]
have left : Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
left : Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]
⊢ (Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]) ∧
    Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]
have right : Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]
have left : ∀ (i j : Fin 2), Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] i j
Tactic: refine continuous_matrix fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
i j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] i j
have left : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
i j : Fin 2
left : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] i j
have left₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have left : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
left :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have left₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have left : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
left :
  Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have left₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]
have right : ∀ (i j : Fin 2), Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] i j
Tactic: refine continuous_matrix fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
i j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] i j
have right : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
i j : Fin 2
right : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] i j
have right₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have right : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j
have right₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have right : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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, ⋯⟩)
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have right₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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)
have 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))
Tactic: refine IsInducing.subtypeVal.continuous_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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, Units.instTopologicalSpaceUnits] (⇑toGL : (a : SL n R) → GL n R)
have 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)
Tactic: simp_rw [Units.continuous_iff, ← map_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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)) ∧
    Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
      (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)
have left : Continuous[instTopologicalSpace, instTopologicalSpaceMatrix]
  (Function.comp (β := (Matrix n n R)ˣ) Units.val (⇑toGL : (a : SL n R) → GL n R))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
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))
⊢ 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)
have right : Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun (x : SL n R) ↦
  (↑((toGL : (a : SL n R) → (Matrix n n R)ˣ) x⁻¹) : Matrix n n R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Matrix (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
A : Type u_4
inst_2 : CommRing A
⊢ 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})
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have 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
Tactic: obtain ⟨s, s_count, hs⟩ : ∃ (s : Set G), s.Countable ∧ ⋃ g ∈ s, g • V = univ :=
    countable_cover_nhds_of_sigmaCompact fun _ ↦ by simpa
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
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}
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
have this : Nonempty X
Tactic: have : Nonempty X := ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
have have : ∀ (this : Encodable (↑s : Type u_1)), ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
Tactic: have : Encodable s := Countable.toEncodable s_count
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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)
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
have hc : ∀ (i : ℕ × (↑s : Type u_1)), IsClosed[inst_1] (F i)
Tactic: apply nonempty_interior_of_iUnion_of_closed
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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)
⊢ ∃ (i : ℕ × (↑s : Type u_1)), (interior (F i)).Nonempty
have hU₁ : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ℕ × (↑s : Type u_1)), F i) univ
Tactic: apply nonempty_interior_of_iUnion_of_closed
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
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)
n : ℕ
g : G
hg : g ∈ s
⊢ IsClosed[inst_1] (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))
have hc : IsCompact (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))
Tactic: apply IsCompact.isClosed