awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
hS' : ∀ {g : Γ} (hg : g ∈ G), ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H
g : Γ
simp :
  g ∈ G →
    (g • K ∩ L).Nonempty →
      ∃ (i : Γ), g * i⁻¹ ∈ H ∧ (∃ (x : i ∈ G), Subtype.mk (p := fun (a : Γ) ↦ a ∈ G) i ⋯ ∈ S) ∧ (g • K ∩ L).Nonempty
⊢ Membership.mem (γ := Set Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty} g →
    Membership.mem (γ := Set Γ)
      (⋃ i ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S,
        (fun (g : Γ) ↦ g * i) <$> {g : Γ | g ∈ H ∧ (g • i • K ∩ L).Nonempty})
      g

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
hS' : ∀ {g : Γ} (hg : g ∈ G), ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H
g : Γ
⊢ g ∈ G →
    (g • K ∩ L).Nonempty →
      ∃ (i : Γ), g * i⁻¹ ∈ H ∧ (∃ (x : i ∈ G), Subtype.mk (p := fun (a : Γ) ↦ a ∈ G) i ⋯ ∈ S) ∧ (g • K ∩ L).Nonempty

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hGH : G ≤ H
inst_4 : G.IsFiniteRelIndex H
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α

Tactic:
⟨fun _ ↦ .ofFiniteRelIndex H G, (properlyDiscontinuousSMul_of_le · hGH)⟩

Premises used: ProperlyDiscontinuousSMul.ofFiniteRelIndex, Subgroup.properlyDiscontinuousSMul_of_le, Iff.intro
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
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
⊢ (G ⊓ H).IsFiniteRelIndex H

Tactic:
have : IsFiniteRelIndex (G ⊓ H) H := ⟨Subgroup.inf_relIndex_right G H ▸ h.1⟩
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
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
⊢ (G ⊓ H).IsFiniteRelIndex G

Tactic:
have : IsFiniteRelIndex (G ⊓ H) G := ⟨Subgroup.inf_relIndex_left G H ▸ h.2⟩
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
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_1 : (G ⊓ H).IsFiniteRelIndex H
this : (G ⊓ H).IsFiniteRelIndex G
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥(G ⊓ H)) α

Tactic:
(properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_left).symm

Premises used: Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex, Set.Mem, inf_le_left, Iff.symm
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
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_1 : (G ⊓ H).IsFiniteRelIndex H
this : (G ⊓ H).IsFiniteRelIndex G
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥(G ⊓ H)) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α

Tactic:
properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_right

Premises used: Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex, inf_le_right
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
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_1 : (G ⊓ H).IsFiniteRelIndex H
this : (G ⊓ H).IsFiniteRelIndex G
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α

Tactic:
calc ProperlyDiscontinuousSMul G α ↔ ProperlyDiscontinuousSMul ↑(G ⊓ H) α :=
    (properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_left).symm
  _ ↔ ProperlyDiscontinuousSMul H α :=
    properlyDiscontinuousSMul_iff_of_isFiniteRelIndex inf_le_right

Premises used: Subgroup.properlyDiscontinuousSMul_iff_of_isFiniteRelIndex, Membership.mem, inf_le_right, Subtype, ProperlyDiscontinuousSMul, inf_le_left, Iff.symm, Min.min
-- Module: Mathlib.Topology.Algebra.Group.Extension
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
H : Subgroup G
inst_3 : H.Normal
hH : IsClosed (↑H : Set G)
⊢ IsClosed (X := G) (Set.range (ι := ↥H) (⇑H.subtype : (a : ↥H) → G))

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.Group.Extension
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
H : Subgroup G
inst_3 : H.Normal
hH : IsClosed (↑H : Set G)
⊢ Function.MulExact (M := ↥H) (N := G) (P := G ⧸ H) (⇑H.subtype : (a : ↥H) → G)
    (⇑(QuotientGroup.mk' H) : (a : G) → G ⧸ H)

Tactic:
simp [Function.MulExact]

Premises used: Function.MulExact
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ IsTopologicalGroup α

Tactic:
haveI := g.toIsTopologicalGroup
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this_1 : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous[instTopologicalSpaceProd, g.toTopologicalSpace] fun (p : α × α) ↦ p.1 * p.2

Tactic:
continuous_mul

Premises used: continuous_mul
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this_1 : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous[instTopologicalSpaceProd, g.toTopologicalSpace] fun (p : α × α) ↦ p.1 * p.2

Tactic:
exact continuous_mul

Premises used: continuous_mul
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this_1 : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous[g.toTopologicalSpace, g.toTopologicalSpace] Inv.inv

Tactic:
continuous_inv

Premises used: ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
this_1 : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous[g.toTopologicalSpace, g.toTopologicalSpace] Inv.inv

Tactic:
exact continuous_inv

Premises used: ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
f g : GroupTopology α
h : f.toTopologicalSpace = g.toTopologicalSpace
mk :
  ∀ (toTopologicalSpace : TopologicalSpace α) (toIsTopologicalGroup : IsTopologicalGroup α)
    (h :
      { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup :
            GroupTopology α }.toTopologicalSpace =
        g.toTopologicalSpace),
    { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup : GroupTopology α } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
g : GroupTopology α
toTopologicalSpace : TopologicalSpace α
toIsTopologicalGroup : IsTopologicalGroup α
h :
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup :
        GroupTopology α }.toTopologicalSpace =
    g.toTopologicalSpace
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 }
⊢ { toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup : GroupTopology α } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
toTopologicalSpace : TopologicalSpace α
toIsTopologicalGroup : IsTopologicalGroup α
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:
congr
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
f g : GroupTopology α
h : Eq.{u + 1} (α := Set α → Prop) TopologicalSpace.IsOpen TopologicalSpace.IsOpen
⊢ f = g

Tactic:
toTopologicalSpace_injective <| TopologicalSpace.ext h

Premises used: TopologicalSpace.ext, GroupTopology.toTopologicalSpace_injective
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
x y : GroupTopology α
⊢ x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
⊢ Eq.{u + 1} (α := TopologicalSpace α) (toTopologicalSpace ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Group α
_t : TopologicalSpace α := ⊥
⊢ DiscreteTopology α

Tactic:
haveI := discreteTopology_bot α
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : Group α
_t : TopologicalSpace α := ⊥
this : DiscreteTopology α
⊢ Continuous[instTopologicalSpaceProd, _t] fun (p : α × α) ↦ p.1 * p.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
⊢ Eq.{u + 1} (α := TopologicalSpace α) (toTopologicalSpace ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
x y : GroupTopology α
⊢ (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
s : Set (GroupTopology α)
⊢ (sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u
inst : Group α
ι : Sort u_1
s : ι → GroupTopology α
⊢ Eq.{u + 1} (α := TopologicalSpace α) (toTopologicalSpace (⨅ (i : ι), s i)) (⨅ (i : ι), (s i).toTopologicalSpace)

Tactic:
congr_arg sInf (range_comp _ _).symm

Premises used: Set.range_comp, iInf, congr_arg, Eq.symm, InfSet.sInf
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst : Group β
f : α → β
rw :
  ∀ (t_1 : TopologicalSpace β),
    Membership.mem (γ := Set (TopologicalSpace β))
        (image (α := GroupTopology β) toTopologicalSpace
          {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace})
        t_1 →
      Continuous[t, _] f
⊢ Continuous[t, (coinduced f).toTopologicalSpace] f

Tactic:
rw [continuous_sInf_rng]

Premises used: continuous_sInf_rng
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst : Group β
f : α → β
t' : GroupTopology β
ht' :
  Membership.mem (γ := Set (GroupTopology β))
    {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace} t'
⊢ Continuous[t, t'.toTopologicalSpace] f

Tactic:
continuous_iff_coinduced_le.2 ht'

Premises used: Iff.mpr, continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Algebra.Group.GroupTopology
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst : Group β
f : α → β
t' : GroupTopology β
ht' :
  Membership.mem (γ := Set (GroupTopology β))
    {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace} t'
⊢ Continuous[t, t'.toTopologicalSpace] f

Tactic:
exact continuous_iff_coinduced_le.2 ht'

Premises used: Iff.mpr, continuous_iff_coinduced_le
-- 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 : α → GL n R
hf : Continuous[inst_4, Units.instTopologicalSpaceUnits] 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 : α → GL n R
hf : Continuous[inst_4, Units.instTopologicalSpaceUnits] 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[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] (⇑(map f) : (a : GL n R) → GL n S)

Tactic:
(continuous_id.matrix_map hf).units_map

Premises used: Continuous.units_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 : IsInducing.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ IsInducing (X := GL n R) (Y := GL n S) (⇑(map f) : (a : GL n R) → GL n S)

Tactic:
hf.matrix_map.units_map

Premises used: Topology.IsInducing.units_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 : IsEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ IsEmbedding (X := GL n R) (Y := GL n S) (⇑(map f) : (a : GL n R) → GL n S)

Tactic:
hf.matrix_map.units_map

Premises used: Topology.IsEmbedding.units_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 : T0Space R
hf : IsClosedEmbedding.{u_2, u_3} (X := R) (Y := S) (⇑f : (a : R) → S)
⊢ IsClosedEmbedding (X := GL n R) (Y := GL n S) (⇑(map f) : (a : GL n R) → GL n S)

Tactic:
hf.matrix_map.units_map

Premises used: Topology.IsClosedEmbedding.units_map
-- 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[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)
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] (⇑det : (a : GL n R) → 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[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑det : (a : GL n R) → Rˣ))
right : Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : 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)

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[Units.instTopologicalSpaceUnits, inst_3] (Function.comp (β := Rˣ) Units.val (⇑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
⊢ Continuous[Units.instTopologicalSpaceUnits, inst_3] fun (x : GL n R) ↦ (↑((det : (a : GL n R) → Rˣ) x⁻¹) : R)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
simp :
  (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, Units.instTopologicalSpaceUnits] (⇑upperRightHom : (a : R) → GL (Fin 2) R)

Tactic:
simp only [continuous_induced_rng, Function.comp_def, upperRightHom_apply,
    Units.embedProduct_apply, Units.inv_mk, continuous_prodMk, MulOpposite.unop_op]

Premises used: Matrix.GeneralLinearGroup.upperRightHom_apply, Units.inv_mk, Function.comp_def, MulOpposite.unop_op, continuous_prodMk, Units.embedProduct_apply, continuous_induced_rng
-- Module: Mathlib.Topology.Algebra.Group.Matrix
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]
right : 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]

Tactic:
constructor
-- 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, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]

Tactic:
continuous_matrix fun i j ↦ ?_

Premises used: continuous_matrix
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
left : ∀ (i j : Fin 2), Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] i j
⊢ Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, x; 0, 1]

Tactic:
refine continuous_matrix fun i j ↦ ?_

Premises used: continuous_matrix
-- Module: Mathlib.Topology.Algebra.Group.Matrix
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
left₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, a; 0, 1] i j

Tactic:
fin_cases i
-- 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
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, ⋯⟩)
left₁ :
  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
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, ⋯⟩)
left₁ :
  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:
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]

Tactic:
continuous_matrix fun i j ↦ ?_

Premises used: continuous_matrix
-- Module: Mathlib.Topology.Algebra.Group.Matrix
Goal:
R : Type u_4
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
right : ∀ (i j : Fin 2), Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] i j
⊢ Continuous[inst_1, instTopologicalSpaceMatrix] fun (x : R) ↦ !![1, -x; 0, 1]

Tactic:
refine continuous_matrix fun i j ↦ ?_

Premises used: continuous_matrix
-- Module: Mathlib.Topology.Algebra.Group.Matrix
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
right₁ : Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
⊢ Continuous[inst_1, inst_1] fun (a : R) ↦ !![1, -a; 0, 1] i j

Tactic:
fin_cases i