awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hf : ContinuousAt (Y := M) (fun (x : G × H) ↦ (((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2) (1, 1)
hl : ∀ (x : G), ContinuousAt.{u_1, u_2} (X := H) (Y := M) (⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1
hr : ∀ (y : H), ContinuousAt.{w, u_2} (Y := M) (fun (x : G) ↦ (((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) 1
x_1 : G × H
x : G
y : H
⊢ ContinuousAt (Y := M) (fun (x : G × H) ↦ (((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2) (x, y)
have simp : ∀
  (hf :
    Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
      (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
      (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)),
  Tendsto (β := M)
    (fun (x_2 : G × H) ↦
      HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) x_2.2 : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) x_2.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) : Filter M)
Tactic: simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
M : Type u_2
inst_3 : CommMonoid M
inst_4 : TopologicalSpace M
inst_5 : ContinuousMul M
inst_6 : Group H
inst_7 : TopologicalSpace H
inst_8 : IsTopologicalGroup H
f : G →* H →* M
hl :
  ∀ (x : G),
    Tendsto.{u_1, u_2} (α := H) (β := M) ((⇑((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) : (a : H) → M) (𝓝 1)
      (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1) : Filter M)
hr :
  ∀ (y : H),
    Tendsto.{w, u_2} (β := M) (fun (x : G) ↦ ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)) (𝓝 1)
      (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) y) : Filter M)
x_1 : G × H
x : G
y : H
hf :
  Tendsto (β := M) (fun (x : G × H) ↦ ((((f : (a : G) → H →* M) x.1 : H →* M) : (a : H) → M) x.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 (((f : (a : G) → H →* M) 1 : (a : H) → M) 1) : Filter M)
⊢ Tendsto (β := M)
    (fun (x_2 : G × H) ↦
      HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) y : M) *
        HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) x_2.2 : M)
          ((((f : (a : G) → H →* M) x_2.1 : H →* M) : (a : H) → M) x_2.2 : M))
    (SProd.sprod (α := Filter G) (β := Filter H) (𝓝 1) (𝓝 1))
    (𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y) : Filter M)
have refine : 𝓝
    (HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y : M)
        (((f : (a : G) → H →* M) 1 : (a : H) → M) y : M) *
      HMul.hMul (α := M) (β := M) ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) 1 : M)
        (((f : (a : G) → H →* M) 1 : (a : H) → M) 1 : M)) =
  𝓝 ((((f : (a : G) → H →* M) x : H →* M) : (a : H) → M) y)
Tactic: refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
⊢ IsInducing.{w, u_1} (X := G) (Y := H) (⇑f : (a : G) → H) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
have rw : (∀ (x : G), 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)) ↔
  Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
Tactic: rw [Topology.isInducing_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
⊢ (∀ (x : G), 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)) ↔
    Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
have refine : ∀ (hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))) (x : G),
  𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)
Tactic: refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ 𝓝 x = comap.{w, u_1} (β := H) ((⇑f : (a : G) → H) : (a : G) → H) (𝓝 ((f : (a : G) → H) x) : Filter H)
have rw : Eq.{w + 1} (α := Filter G) (comap.{w, u_1} (β := H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
  (comap.{w, u_1} (β := H) ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H))
    (𝓝 1))
Tactic: rw [← nhds_translation_mul_inv, ← nhds_translation_mul_inv (f x), Filter.comap_comap, hf,
    Filter.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ Eq.{w + 1} (α := Filter G)
    (comap.{w, u_1} (β := H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap.{w, u_1} (β := H)
      ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) (𝓝 1))
have e_m : Eq (α := G → H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹)
  ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Group H
inst_4 : TopologicalSpace H
inst_5 : IsTopologicalGroup H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
hf : Eq.{w + 1} (α := Filter G) (𝓝 1) (comap.{w, u_1} (β := H) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ Eq (α := G → H) (comp (β := G) (⇑f : (a : G) → H) fun (x_1 : G) ↦ x_1 * x⁻¹)
    ((fun (x_1 : H) ↦ HMul.hMul (β := H) x_1 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H))
have e_m : ∀ (x_1 : G),
  Eq.{u_1 + 1} (α := H) (comp (β := G) (⇑f : (a : G) → H) (fun (x_2 : G) ↦ x_2 * x⁻¹) x_1)
    (((fun (x_2 : H) ↦ HMul.hMul (β := H) x_2 (((f : (a : G) → H) x)⁻¹ : H)) ∘ (⇑f : (a : G) → H)) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
⊢ IsOpenMap.{w, u_1} (X := G) (Y := H) (⇑f : (a : G) → H) ↔
    LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
have refine : ∀ (h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))) (x : G),
  LE.le.{u_1} (α := Filter H) (𝓝 ((f : (a : G) → H) x) : Filter H) (map (⇑f : (a : G) → H) (𝓝 x) : Filter H)
Tactic: refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
⊢ LE.le.{u_1} (α := Filter H) (𝓝 ((f : (a : G) → H) x) : Filter H) (map (⇑f : (a : G) → H) (𝓝 x) : Filter H)
have this : Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
  (𝓝 ((f : (a : G) → H) x) : Filter H)
Tactic: have : Filter.map (f x * ·) (𝓝 1) = 𝓝 (f x) := by
    simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
      (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
⊢ LE.le.{u_1} (α := Filter H) (𝓝 ((f : (a : G) → H) x) : Filter H) (map (⇑f : (a : G) → H) (𝓝 x) : Filter H)
have rw : LE.le.{u_1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1))
  (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))
Tactic: rw [← map_mul_left_nhds_one x, Filter.map_map, Function.comp_def, ← this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : Type u_1
inst_3 : Monoid H
inst_4 : TopologicalSpace H
inst_5 : ContinuousConstSMul H H
F : Type u_2
inst_6 : FunLike F G H
inst_7 : MonoidHomClass F G H
f : F
h : LE.le.{u_1} (α := Filter H) (𝓝 1) (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1))
x : G
this :
  Eq.{u_1 + 1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1) : Filter H)
    (𝓝 ((f : (a : G) → H) x) : Filter H)
⊢ LE.le.{u_1} (α := Filter H) (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1) (𝓝 1))
    (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))
have refine : LE.le.{u_1} (α := Filter H)
  (map (fun (x_1 : H) ↦ HMul.hMul (α := H) ((f : (a : G) → H) x : H) x_1)
    (map.{w, u_1} (α := G) (⇑f : (a : G) → H) (𝓝 1)))
  (map (fun (x_1 : G) ↦ (f : (a : G) → H) (x * x_1)) (𝓝 1))
Tactic: refine (Filter.map_mono h).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
⊢ IsOpen[inst_4] ((⇑φ : (a : A) → B) '' U)
have rw : IsOpen[inst_1] (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
Tactic: rw [← hφ.isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
⊢ IsOpen[inst_1] (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
have suffices : Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
  (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)
Tactic: suffices ⇑φ ⁻¹' ⇑φ '' U = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
        exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
⊢ Eq.{u_1 + 1} (α := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U))
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U)
have h : ∀ (x : A),
  Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x ↔
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x : A
⊢ Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x ↔
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
have h : Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x →
  Membership.mem (γ := Set A)
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x : A
h :
  Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x →
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
⊢ Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x ↔
    Membership.mem (γ := Set A)
      (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
have h₁ : Membership.mem (γ := Set A)
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x →
  Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x y : A
hyU : y ∈ U
hyx : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) y : B) ((φ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A)
    (⋃ (k : A), ⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k), (fun (x : A) ↦ x * k) ⁻¹' U) x
have h : Membership.mem (γ := Set A)
  (⋃ (_ : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) (x⁻¹ * y)), (fun (x_1 : A) ↦ x_1 * (x⁻¹ * y)) ⁻¹' U) x
Tactic: apply Set.mem_iUnion_of_mem (x⁻¹ * y)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
⊢ Membership.mem (γ := Set A) (preimage.{u_1, u_2} (β := B) (⇑φ : (a : A) → B) ((⇑φ : (a : A) → B) '' U)) x
have right : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)
Tactic: use x * k, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)
have right : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) k : B) = (φ : (a : A) → B) x
Tactic: rw [map_mul, hk, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
right : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) k : B) = (φ : (a : A) → B) x
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)
have right₁ : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) (1 : B) = (φ : (a : A) → B) x
Tactic: rw [map_mul, hk, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
A : Type u_1
inst : Group A
inst_1 : TopologicalSpace A
inst_2 : ContinuousMul A
B : Type u_2
inst_3 : Group B
inst_4 : TopologicalSpace B
F : Type u_3
inst_5 : FunLike F A B
inst_6 : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap.{u_1, u_2} (X := A) (Y := B) (⇑φ : (a : A) → B)
U : Set A
hU : IsOpen[inst_1] U
x k : A
hk : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) k : B) (1 : B)
hx :
  Membership.mem (γ := Set A)
    ((fun (h : Membership.mem (γ := Subgroup A) (ker (↑φ : A →* B)) k) ↦ ((fun (x : A) ↦ x * k) ⁻¹' U : Set A)) hk) x
right : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) k : B) = (φ : (a : A) → B) x
right₁ : HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) x : B) (1 : B) = (φ : (a : A) → B) x
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) (x * k) : B) ((φ : (a : A) → B) x : B)
have right₂ : Eq.{u_2 + 1} (α := B) ((φ : (a : A) → B) x : B) ((φ : (a : A) → B) x : B)
Tactic: rw [map_mul, hk, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (𝓝 1)
x : G
⊢ 𝓝 x = 𝓝 x
have rw : comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
Tactic: rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (𝓝 1)
x : G
rw : comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
⊢ 𝓝 x = 𝓝 x
have rw₁ : Eq.{u_1 + 1} (α := Filter G) (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
  (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
Tactic: rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : Group G
t t' : TopologicalSpace G
tg : IsTopologicalGroup G
tg' : IsTopologicalGroup G
h : Eq.{u_1 + 1} (α := Filter G) (𝓝 1) (𝓝 1)
x : G
rw : comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1) = 𝓝 x
rw₁ :
  Eq.{u_1 + 1} (α := Filter G) (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
    (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
⊢ 𝓝 x = 𝓝 x
have rw₂ : Eq.{u_1 + 1} (α := Filter G) (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
  (comap (β := G) (fun (x_1 : G) ↦ x_1 * x⁻¹) (𝓝 1))
Tactic: rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
⊢ ContinuousInv G
have refine : ∀ (x₀ : G), ContinuousAt (Y := G) (fun (a : G) ↦ a⁻¹) x₀
Tactic: refine ⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hconj : ∀ (x₀ : G), Tendsto (β := G) (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)
x₀ : G
⊢ ContinuousAt (Y := G) (fun (a : G) ↦ a⁻¹) x₀
have this : Tendsto (β := G) (fun (x : G) ↦ x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (fun (x : G) ↦ x₀⁻¹ * x) (𝓝 1))
Tactic: have : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (x₀⁻¹ * ·) (𝓝 1)) :=
    (tendsto_map.comp <| hconj x₀).comp hinv
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Basic (goal)
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
hmul :
  Tendsto (β := G) (uncurry fun (x1 x2 : G) ↦ x1 * x2) (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1) (𝓝 1)) (𝓝 1)
hinv : Tendsto (β := G) (fun (x : G) ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun (x : G) ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ Eq.{u + 1} (α := Filter G) (map (fun (x : G) ↦ x₀ * x * x₀⁻¹) (𝓝 1)) (𝓝 1)
have rw : Eq.{u + 1} (α := Filter G) (map (α := G) ((fun (x : G) ↦ x * x₀⁻¹) ∘ fun (x : G) ↦ x * x₀) (𝓝 1)) (𝓝 1)
Tactic: rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]