awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
h :
  ∀ (x : (G × G) × G × G),
    x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) =
      ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) x
⊢ Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : (G × G) × G × G
h : x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) =
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) x

Tactic:
simp only [Function.comp_apply, mul_inv_rev, inv_inv]

Premises used: inv_inv, Function.comp_apply, mul_inv_rev
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : (G × G) × G × G
h : x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)

Tactic:
rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]

Premises used: mul_assoc, Prod.fst, Inv.inv, mul_comm, Prod.snd
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))

Tactic:
have : (fun (x : (G × G) × (G × G)) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) =
    (fun (p : G × G) ↦ p.1 * p.2⁻¹)
      ∘ (fun (p : (G × G) × (G × G)) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) := by
    ext x
    simp only [Function.comp_apply, mul_inv_rev, inv_inv]
    rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]
    simp [mul_assoc]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
uniformContinuous_div :
  Tendsto (β := G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
⊢ UniformContinuous (β := G) fun (p : G × G) ↦ p.1 / p.2

Tactic:
simp only [UniformContinuous, div_eq_mul_inv, uniformity_prod_eq_prod,
    uniformity_eq_comap_nhds_one', prod_comap_comap_eq, ← nhds_prod_eq, tendsto_comap_iff,
    Function.comp_def, mul_inv_rev, inv_inv, tendsto_map'_iff]

Premises used: UniformContinuous, Filter.tendsto_map'_iff, Filter.tendsto_comap_iff, uniformity_prod_eq_prod, div_eq_mul_inv, Function.comp_def, inv_inv, Filter.prod_comap_comap_eq, nhds_prod_eq, mul_inv_rev, uniformity_eq_comap_nhds_one'
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
uniformContinuous_div :
  Tendsto.{u_1, u_1} (α := (G × G) × G × G) (β := G)
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
⊢ Tendsto (β := G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
apply : Tendsto (β := G) (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)
⊢ Tendsto.{u_1, u_1} (α := (G × G) × G × G) (β := G)
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
    (comap (β := G × G) (fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)

Tactic:
apply Tendsto.comp ?_ tendsto_comap

Premises used: Filter.tendsto_comap, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ 1 = HMul.hMul (α := G) 1 1⁻¹

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
nth_rewrite : Tendsto (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := G) 1 1⁻¹))
⊢ Tendsto (β := G) (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 1)

Tactic:
nth_rewrite 3 [show (1 : G) = 1 * 1⁻¹ by simp]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 * p.2⁻¹

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
this :
  Eq.{u_1 + 1} (α := (x : (G × G) × G × G) → G) (fun (x : (G × G) × G × G) ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹))
    ((fun (p : G × G) ↦ p.1 * p.2⁻¹) ∘ fun (p : (G × G) × G × G) ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
⊢ Tendsto (fun (p : G × G) ↦ p.1 * p.2⁻¹) (𝓝 (1, 1)) (𝓝 (HMul.hMul (α := G) 1 1⁻¹))

Tactic:
apply Continuous.tendsto (by fun_prop)

Premises used: Continuous.tendsto
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_2
u : UniformSpace G
inst : Group G
inst_1 : IsUniformGroup G
h : 𝓤 G = 𝓤 G
⊢ IsTopologicalGroup.rightUniformSpace G = u

Tactic:
ext : 1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Goal:
G : Type u_2
u : UniformSpace G
inst : Group G
inst_1 : IsUniformGroup G
h : comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1) = 𝓤 G
h₁ h₂ :
  Eq.{u_2 + 1} (α := Filter (G × G)) (comap (β := G) (fun (p : G × G) ↦ p.2 * p.1⁻¹) (𝓝 1))
    (comap (β := G) (fun (x : G × G) ↦ x.2 * x.1⁻¹) (𝓝 1))
⊢ 𝓤 G = 𝓤 G

Tactic:
rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_mul_inv_nhds_one]

Premises used: uniformity_eq_comap_mul_inv_nhds_one, uniformity_eq_comap_nhds_one'
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
simp :
  ∀ (s : Set ↥H),
    (∃ (a : Set G),
        IsOpen[inst_1] a ∧
          Eq (α := Set { x : ↥K // x ∈ (↑(H.subgroupOf K) : Set ↥K) })
            (Subtype.val (p := fun (x : ↥K) ↦ x ∈ (↑(H.subgroupOf K) : Set ↥K)) ⁻¹'
              Subtype.val (p := fun (x : G) ↦ x ∈ (↑K : Set G)) ⁻¹' a)
            ((⇑{ toFun := fun (g : ↥(H.subgroupOf K)) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(↑g : ↥K) : G) ⋯,
                    invFun := fun (g : ↥H) ↦
                      Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K)
                        (Subtype.mk (p := fun (x : G) ↦ x ∈ K) (↑g : G) ⋯) ⋯,
                    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ : ↥(H.subgroupOf K) ≃* ↥H } :
                (a : ↥(H.subgroupOf K)) → ↥H) ⁻¹'
              s)) ↔
      ∃ (t : Set G), IsOpen[inst_1] t ∧ Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G)) ⁻¹' t = s
⊢ ∀ (s : Set ↥H),
    IsOpen[instTopologicalSpaceSubtype] ((⇑(subgroupOfEquivOfLe hHK) : (a : ↥(H.subgroupOf K)) → ↥H) ⁻¹' s) ↔
      IsOpen[instTopologicalSpaceSubtype] s

Tactic:
simp only [subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal.isOpen_iff,
      exists_exists_and_eq_and]

Premises used: Topology.IsInducing.isOpen_iff, exists_exists_and_eq_and, Subgroup.subgroupOfEquivOfLe, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
s : Set ↥H
t : Set G
h : IsOpen[inst_1] t
⊢ (∀ (a : G) (b : a ∈ H), a ∈ t ↔ Subtype.mk (p := fun (a : G) ↦ a ∈ H) a b ∈ s) →
    ∀ (a : G) (b : a ∈ K) (b_1 : Subtype.mk (p := fun (a : G) ↦ a ∈ K) a b ∈ H.subgroupOf K),
      a ∈ t ↔ Subtype.mk (p := fun (x : G) ↦ x ∈ H) a ⋯ ∈ s

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ ∀ (s : Set ↥H),
    (∃ (a : Set G),
        IsOpen[inst_1] a ∧
          Eq (α := Set { x : ↥K // x ∈ (↑(H.subgroupOf K) : Set ↥K) })
            (Subtype.val (p := fun (x : ↥K) ↦ x ∈ (↑(H.subgroupOf K) : Set ↥K)) ⁻¹'
              Subtype.val (p := fun (x : G) ↦ x ∈ (↑K : Set G)) ⁻¹' a)
            ((⇑{ toFun := fun (g : ↥(H.subgroupOf K)) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (↑(↑g : ↥K) : G) ⋯,
                    invFun := fun (g : ↥H) ↦
                      Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K)
                        (Subtype.mk (p := fun (x : G) ↦ x ∈ K) (↑g : G) ⋯) ⋯,
                    left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ : ↥(H.subgroupOf K) ≃* ↥H } :
                (a : ↥(H.subgroupOf K)) → ↥H) ⁻¹'
              s)) ↔
      ∃ (t : Set G), IsOpen[inst_1] t ∧ Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G)) ⁻¹' t = s

Tactic:
simpa [Set.ext_iff] using fun s ↦ exists_congr
      fun t ↦ and_congr_right fun _ ↦ ⟨fun aux g hgh ↦ aux g (hHK hgh) hgh, by grind⟩

Premises used: and_congr_right, exists_congr, Iff.intro, Set.ext_iff
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
g : ↥H
⊢ Eq (α := ↥(H.subgroupOf K))
    ((ContinuousMulEquiv.symm (subgroupOfContinuousMulEquivOfLe hHK) : (a : ↥H) → ↥(H.subgroupOf K)) g :
      ↥(H.subgroupOf K))
    (Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) (Subtype.mk (p := fun (x : G) ↦ x ∈ K) (↑g : G) ⋯) ⋯ :
      ↥(H.subgroupOf K))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H K : Subgroup G
hHK : H ≤ K
⊢ (↑(subgroupOfContinuousMulEquivOfLe hHK) : ↥(H.subgroupOf K) ≃* ↥H) = subgroupOfEquivOfLe hHK

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology G

Tactic:
⟨fun hH ↦ ?_, fun hG ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
refine : ∀ (hH : DiscreteTopology.{u_1} ↥H), DiscreteTopology G
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology G

Tactic:
refine ⟨fun hH ↦ ?_, fun hG ↦ inferInstance⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
this : IsOpen[inst_1] (↑H : Set G)
rw : IsOpen[inst_1] {1}
rw₁ : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (pure 1)
rw₂ : Eq.{u_1 + 1} (α := Filter G) (𝓝 (↑1 : G)) (pure (↑1 : G))
rw₃ :
  Eq.{u_1 + 1} (α := Filter G)
    (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (𝓝 1))
    (pure (↑1 : G))
rw₄ :
  Eq.{u_1 + 1} (α := Filter G)
    (Filter.map (α := { x : G // x ∈ (↑H : Set G) }) (Subtype.val (p := fun (x : G) ↦ x ∈ (↑H : Set G))) (pure 1))
    (pure (↑1 : G))
rw₅ rw₆ : Eq.{u_1 + 1} (α := Filter G) (pure (↑1 : G)) (pure (↑1 : G))
⊢ DiscreteTopology G

Tactic:
rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, IsOpen.isOpenEmbedding_subtypeVal, Subgroup.coe_one, isOpen_singleton_iff_nhds_eq_pure, nhds_discrete, Filter.map_pure, discreteTopology_iff_isOpen_singleton_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
suffices : IsOpen[inst_1] (↑H : Set G)
⊢ DiscreteTopology G

Tactic:
suffices IsOpen (H : Set G) by
    rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
H.isOpen_of_isClosed_of_finiteIndex Subgroup.isClosed_of_discrete

Premises used: Subgroup.isOpen_of_isClosed_of_finiteIndex, Subgroup.isClosed_of_discrete
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H : Subgroup G
inst_4 : H.FiniteIndex
hH : DiscreteTopology.{u_1} ↥H
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
exact H.isOpen_of_isClosed_of_finiteIndex Subgroup.isClosed_of_discrete

Premises used: Subgroup.isOpen_of_isClosed_of_finiteIndex, Subgroup.isClosed_of_discrete
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst_4 : H.IsFiniteRelIndex K
⊢ (H.subgroupOf K).FiniteIndex

Tactic:
haveI : (H.subgroupOf K).FiniteIndex := IsFiniteRelIndex.to_finiteIndex_subgroupOf
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst_4 : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
rw : DiscreteTopology.{u_1} ↥(H.subgroupOf K) ↔ DiscreteTopology.{u_1} ↥K
rw₁ rw₂ : DiscreteTopology.{u_1} ↥K ↔ DiscreteTopology.{u_1} ↥K
⊢ DiscreteTopology.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥K

Tactic:
rw [← (subgroupOfContinuousMulEquivOfLe hHK).discreteTopology_iff,
    discreteTopology_iff_of_finiteIndex]

Premises used: Homeomorph.discreteTopology_iff, Subgroup.subgroupOfContinuousMulEquivOfLe, Subgroup.discreteTopology_iff_of_finiteIndex, ContinuousMulEquiv.toHomeomorph
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : T2Space G
H K : Subgroup G
h : H.Commensurable K
⊢ DiscreteTopology.{u_2} ↥H ↔ DiscreteTopology.{u_2} ↥K

Tactic:
calc DiscreteTopology H ↔ DiscreteTopology ↑(H ⊓ K) :=
    haveI : IsFiniteRelIndex (H ⊓ K) H := ⟨Subgroup.inf_relIndex_left H K ▸ h.2⟩
    (Subgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_left).symm
  _ ↔ DiscreteTopology K :=
    haveI : IsFiniteRelIndex (H ⊓ K) K := ⟨Subgroup.inf_relIndex_right H K ▸ h.1⟩
    Subgroup.discreteTopology_iff_of_isFiniteRelIndex inf_le_right

Premises used: Trans.trans, inf_le_right, Subgroup.discreteTopology_iff_of_isFiniteRelIndex, inf_le_left, Iff.symm
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hf : TendstoUniformlyOn f g p K
hg : ∀ x ∈ K, g x ≤ u
⊢ ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)

Tactic:
simp only [tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero,
    tendsto_iff_eventually, eventually_comap, Prod.forall] at *

Premises used: tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero, Prod.forall, Filter.eventually_comap, Filter.tendsto_iff_eventually
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
enter :
  ∀ (p_1 : β × β → Prop),
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)

Tactic:
enter [2]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_2 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_2 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_2 (g x.2, f x.1 x.2)
p_1 : β × β → Prop
rw :
  (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a b : β), -a + b = y → p_1 (a, b)) →
    ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)

Tactic:
rw [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
enter :
  ∀ (p_1 : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a b : β), -a + b = y → p_1 (a, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)

Tactic:
enter [2]; rw [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
⊢ ∀ (a : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a_2 b : β), -a_2 + b = y → a (a_2, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, a (g x.2, f x.1 x.2)

Tactic:
conv at hf => enter [2]; rw [eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ (a : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a_2 b : β), -a_2 + b = y → a (a_2, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, a (g x.2, f x.1 x.2)
⊢ Membership.mem (γ := Set β) {b : β | b < -u + v} 0

Tactic:
simp [huv]
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ (a : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a_2 b : β), -a_2 + b = y → a (a_2, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, a (g x.2, f x.1 x.2)
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, (fun (x : β × β) ↦ -x.1 + x.2 < -u + v) (g x.2, f x.1 x.2)

Tactic:
have hf2 := hf (fun x ↦ -x.1 + x.2 < -u + v) ⟨_, (isOpen_gt' (-u + v)).mem_nhds (by simp [huv]),
    fun y hy a b hab ↦ (hab.symm ▸ hy :)⟩
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ (a : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a_2 b : β), -a_2 + b = y → a (a_2, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, a (g x.2, f x.1 x.2)
hf2 : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, (fun (x : β × β) ↦ -x.1 + x.2 < -u + v) (g x.2, f x.1 x.2)
h : ∀ (i : ι) (hi : ∀ y ∈ K, -g y + f i y < -u + v) (x : α) (hx : x ∈ K), f i x < v
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v

Tactic:
filter_upwards [eventually_prod_principal_iff.mp hf2] with i hi x hx

Premises used: Filter.eventually_prod_principal_iff, Iff.mp