awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
⊢ γ • x ∉ V₀
have pos : ∀ (H : γ ∈ bad_Γ_set), γ • x ∉ V₀
Tactic: by_cases H : γ ∈ bad_Γ_set
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
pos : ∀ (H : γ ∈ bad_Γ_set), γ • x ∉ V₀
⊢ γ • x ∉ V₀
have neg : ∀ (H : γ ∉ bad_Γ_set), γ • x ∉ V₀
Tactic: by_cases H : γ ∈ bad_Γ_set
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (hypothesis)
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
Γ : Type u_4
inst : Group Γ
T : Type u_5
inst_1 : TopologicalSpace T
inst_2 : MulAction Γ T
inst_3 : T2Space T
inst_4 : LocallyCompactSpace T
inst_5 : ContinuousConstSMul Γ T
inst_6 : ProperlyDiscontinuousSMul Γ T
this : Setoid T := MulAction.orbitRel Γ T
Q : Type u_5 := Quotient (MulAction.orbitRel Γ T)
f : T → Q := Quotient.mk'
f_op : IsOpenMap f
i : Quotient (MulAction.orbitRel Γ T)
x₀ : T
j : Quotient (MulAction.orbitRel Γ T)
y₀ : T
hxy : f x₀ ≠ f y₀
hγx₀y₀ : ∀ (γ : Γ), γ • x₀ ≠ y₀
K₀ : Set T
hK₀ : IsCompact K₀
K₀_in : K₀ ∈ 𝓝 x₀
L₀ : Set T
hL₀ : IsCompact L₀
L₀_in : L₀ ∈ 𝓝 y₀
bad_Γ_set : Set Γ := {γ : Γ | ((fun (x : T) ↦ γ • x) '' K₀ ∩ L₀).Nonempty}
bad_Γ_finite : bad_Γ_set.Finite
u v : (γ : Γ) → Set T
hu : ∀ (γ : Γ), u γ ∈ 𝓝 (γ • x₀)
hv : ∀ (γ : Γ), v γ ∈ 𝓝 y₀
u_v_disjoint : ∀ (γ : Γ), Disjoint (u γ) (v γ)
U₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, (fun (x : T) ↦ γ • x) ⁻¹' u γ
U₀ : Set T := U₀₀ ∩ K₀
V₀₀ : Set T := ⋂ γ ∈ bad_Γ_set, v γ
V₀ : Set T := V₀₀ ∩ L₀
U_nhds : f '' U₀ ∈ 𝓝 (f x₀)
V_nhds : f '' V₀ ∈ 𝓝 (f y₀)
x : T
x_in_U₀₀ : x ∈ U₀₀
x_in_K₀ : x ∈ K₀
γ : Γ
H : γ ∉ bad_Γ_set
h' : γ • x ∈ L₀
⊢ False
have H₁ : γ • K₀ ∩ L₀ = ∅
Tactic: simp only [bad_Γ_set, image_smul, not_nonempty_iff_eq_empty, mem_setOf_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : AddMonoid α
inst_2 : DistribMulAction G₀ α
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ Membership.mem (γ := Filter α) (𝓝 0) s
have refine : Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ c • s ∈ 𝓝 (HSMul.hSMul (β := α) c 0)
Tactic: refine Iff.trans ?_ (smul_mem_nhds_smul_iff₀ hc)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ConstMulAction (goal)
Goal:
α : Type u_2
G₀ : Type u_6
inst : GroupWithZero G₀
inst_1 : AddMonoid α
inst_2 : DistribMulAction G₀ α
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ c • s ∈ 𝓝 (HSMul.hSMul (β := α) c 0)
have rw : Membership.mem (γ := Filter α) (𝓝 0) (c • s) ↔ Membership.mem (γ := Filter α) (𝓝 0) (c • s)
Tactic: rw [smul_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
⊢ Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits
    (TopologicalSpace.induced val inst ⊓ TopologicalSpace.induced (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) inst)
have simp : Eq (α := TopologicalSpace Mˣ)
  (TopologicalSpace.induced (Function.comp (β := M × Mᵐᵒᵖ) Prod.fst (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ)) inst ⊓
    TopologicalSpace.induced (Function.comp (β := M × Mᵐᵒᵖ) (unop ∘ Prod.snd) (⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ))
      inst)
  (TopologicalSpace.induced val inst ⊓ TopologicalSpace.induced (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) inst)
Tactic: simp only [isInducing_embedProduct.1, instTopologicalSpaceProd, induced_inf,
    instTopologicalSpaceMulOpposite, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
⊢ IsEmbedding.{u_4, u_4} (X := Mˣ) val
have refine : Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits (TopologicalSpace.induced val inst_1)
Tactic: refine ⟨⟨?_⟩, val_injective⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
⊢ Eq (α := TopologicalSpace Mˣ) instTopologicalSpaceUnits (TopologicalSpace.induced val inst_1)
have rw : ∀ (x : Mˣ), ContinuousAt (Y := M) (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) x
Tactic: rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
    @continuous_iff_continuousAt _ _ (.induced _ _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_4
inst : Monoid M
inst_1 : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x : M | IsUnit x}
hf : ∀ (u : Mˣ), f (↑u : M) = (↑u⁻¹ : M)
u : Mˣ
s : Set M
hs : Membership.mem (γ := Filter M) (𝓝 ((fun (u : Mˣ) ↦ (↑u⁻¹ : M)) u)) s
⊢ Membership.mem (γ := Filter M) (Filter.map (fun (u : Mˣ) ↦ (↑u⁻¹ : M)) (𝓝 u)) s
have simp : ∀ (hs : s ∈ 𝓝 (f (↑u : M))),
  Membership.mem (γ := Filter Mˣ) (comap val (𝓝 (↑u : M))) ((fun (u : Mˣ) ↦ f (↑u : M)) ⁻¹' s)
Tactic: simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (hypothesis)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
⊢ IsOpen[instTopologicalSpaceUnits]
    (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U))
have hg_openMap : IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
  (Prod.map (⇑f : (a : M) → N)
    (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
      (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
Tactic: have hg_openMap := hf.prodMap <| opHomeomorph.isOpenMap.comp (hf.comp opHomeomorph.symm.isOpenMap)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
⊢ IsOpen[instTopologicalSpaceUnits]
    (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U))
have refine : ∀ (y : Nˣ),
  Membership.mem (γ := Set Nˣ)
      (Set.preimage (β := N × Nᵐᵒᵖ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ)
        (Prod.map (⇑f : (a : M) → N)
            (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))) ''
          U))
      y ↔
    Membership.mem (γ := Set Nˣ)
      (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U)) y
Tactic: refine ⟨_, hg_openMap U hU, Set.ext fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
y : Nˣ
⊢ Membership.mem (γ := Set Nˣ)
      (Set.preimage (β := N × Nᵐᵒᵖ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ)
        (Prod.map (⇑f : (a : M) → N)
            (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))) ''
          U))
      y ↔
    Membership.mem (γ := Set Nˣ)
      (Set.image (α := Mˣ) (⇑(map f) : (a : Mˣ) → Nˣ) ((⇑(embedProduct M) : (a : Mˣ) → M × Mᵐᵒᵖ) ⁻¹' U)) y
have simp : (∃ (a : M) (a_1 : M),
    (a, op a_1) ∈ U ∧
      (f : (a : M) → N) a = (↑y : N) ∧
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
          op (↑y⁻¹ : N)) ↔
  ∃ (x : Mˣ), ((↑x : M), op (↑x⁻¹ : M)) ∈ U ∧ (map f : (a : Mˣ) → Nˣ) x = y
Tactic: simp only [embedProduct, OneHom.coe_mk, Set.mem_preimage, Set.mem_image, Prod.mk.injEq,
    Prod.map, Prod.exists, MulOpposite.exists, MonoidHom.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
y : Nˣ
⊢ (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) ↔
    ∃ (x : Mˣ), ((↑x : M), op (↑x⁻¹ : M)) ∈ U ∧ (map f : (a : Mˣ) → Nˣ) x = y
have refine_1 : (∃ (a : M) (a_1 : M),
    (a, op a_1) ∈ U ∧
      (f : (a : M) → N) a = (↑y : N) ∧
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
          op (↑y⁻¹ : N)) →
  ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
    (hb :
      Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
          (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
        op (↑y⁻¹ : N)),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (a * b) : N) ((f : (a : M) → N) 1 : N)
Tactic: refine ⟨fun ⟨a, b, h, ha, hb⟩ ↦ ⟨⟨a, b, hf_inj ?_, hf_inj ?_⟩, ?_⟩,
    fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf_inj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hf : IsOpenMap.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap :
  IsOpenMap.{u_1, u_2} (X := M × Mᵐᵒᵖ) (Y := N × Nᵐᵒᵖ)
    (Prod.map (⇑f : (a : M) → N)
      (Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
        (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M))))
y : Nˣ
refine_1 :
  (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) →
    ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
      (hb :
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
          op (↑y⁻¹ : N)),
      Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (a * b) : N) ((f : (a : M) → N) 1 : N)
⊢ (∃ (a : M) (a_1 : M),
      (a, op a_1) ∈ U ∧
        (f : (a : M) → N) a = (↑y : N) ∧
          Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
              (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
            op (↑y⁻¹ : N)) ↔
    ∃ (x : Mˣ), ((↑x : M), op (↑x⁻¹ : M)) ∈ U ∧ (map f : (a : Mˣ) → Nˣ) x = y
have refine_2 : (∃ (a : M) (a_1 : M),
    (a, op a_1) ∈ U ∧
      (f : (a : M) → N) a = (↑y : N) ∧
        Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
            (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op a_1) =
          op (↑y⁻¹ : N)) →
  ∀ (a b : M) (h : (a, op b) ∈ U) (ha : (f : (a : M) → N) a = (↑y : N))
    (hb :
      Function.comp (β := N) (⇑opHomeomorph : (a : N) → Nᵐᵒᵖ)
          (Function.comp (β := M) (⇑f : (a : M) → N) (⇑(Homeomorph.symm opHomeomorph) : (a : Mᵐᵒᵖ) → M)) (op b) =
        op (↑y⁻¹ : N)),
    Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (b * a) : N) ((f : (a : M) → N) 1 : N)
Tactic: refine ⟨fun ⟨a, b, h, ha, hb⟩ ↦ ⟨⟨a, b, hf_inj ?_, hf_inj ?_⟩, ?_⟩,
    fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsInducing.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsInducing.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)
have refine : IsInducing.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
  (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))
Tactic: refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Constructions (goal)
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : Monoid M
inst_2 : TopologicalSpace N
inst_3 : Monoid N
f : M →* N
hf : IsEmbedding.{u_1, u_2} (X := M) (Y := N) (⇑f : (a : M) → N)
⊢ IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := Nˣ) (⇑(map f) : (a : Mˣ) → Nˣ)
have refine : IsEmbedding.{u_1, u_2} (X := Mˣ) (Y := N × Nᵐᵒᵖ)
  (Function.comp (β := Nˣ) (⇑(embedProduct N) : (a : Nˣ) → N × Nᵐᵒᵖ) (⇑(map f) : (a : Mˣ) → Nˣ))
Tactic: refine .of_comp (continuous_map hf.continuous) continuous_embedProduct ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
⊢ e = e'
have h₁ : ∀ (p : P₁), Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) p : P₂) ((e' : (a : P₁) → P₂) p : P₂)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e e' : P₁ ≃ᴬ[k] P₂
h : e.toContinuousAffineMap = e'.toContinuousAffineMap
p : P₁
⊢ Eq.{u_3 + 1} (α := P₂) ((e : (a : P₁) → P₂) p : P₂) ((e' : (a : P₁) → P₂) p : P₂)
have h₁ : Eq.{u_3 + 1} (α := P₂) ((e.toContinuousAffineMap : (a : P₁) → P₂) p : P₂)
  ((e'.toContinuousAffineMap : (a : P₁) → P₂) p : P₂)
Tactic: simp_rw [← coe_toContinuousAffineMap, h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₂
⊢ Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm : (a : P₂) → P₁) '' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
have rw : Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm.symm : (a : P₁) → P₂) ⁻¹' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
e : P₁ ≃ᴬ[k] P₂
s : Set P₂
rw : Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm.symm : (a : P₁) → P₂) ⁻¹' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
⊢ Eq.{u_2 + 1} (α := Set P₁) ((⇑e.symm : (a : P₂) → P₁) '' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
have rw₁ : Eq.{u_2 + 1} (α := Set P₁) ((⇑e : (a : P₁) → P₂) ⁻¹' s) ((⇑e : (a : P₁) → P₂) ⁻¹' s)
Tactic: rw [e.symm.image_eq_preimage_symm, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((↑e₁ : P₁ ≃ᵃ[k] P₂).prodCongr (↑e₂ : P₃ ≃ᵃ[k] P₄)).toFun a
have dsimp : Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((e₁ : (a : P₁) → P₂) a.1, (e₂ : (a : P₃) → P₄) a.2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineEquiv (goal)
Goal:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AddTorsor V₁ P₁
inst_4 : TopologicalSpace P₁
inst_5 : AddCommGroup V₂
inst_6 : Module k V₂
inst_7 : AddTorsor V₂ P₂
inst_8 : TopologicalSpace P₂
inst_9 : AddCommGroup V₃
inst_10 : Module k V₃
inst_11 : AddTorsor V₃ P₃
inst_12 : TopologicalSpace P₃
inst_13 : AddCommGroup V₄
inst_14 : Module k V₄
inst_15 : AddTorsor V₄ P₄
inst_16 : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous (Y := P₁ × P₃) fun (a : P₂ × P₄) ↦ ((↑e₁ : P₁ ≃ᵃ[k] P₂).prodCongr (↑e₂ : P₃ ≃ᵃ[k] P₄)).invFun a
have dsimp : Continuous (Y := P₁ × P₃) fun (a : P₂ × P₄) ↦ ((e₁.symm : (a : P₂) → P₁) a.1, (e₂.symm : (a : P₄) → P₃) a.2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : (↑f : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)
⊢ f = g
have mk : ∀ (toAffineMap : P →ᵃ[R] Q) (cont : Continuous toAffineMap.toFun)
  (h : (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)),
  { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
g : P →ᴬ[R] Q
toAffineMap : P →ᵃ[R] Q
cont : Continuous toAffineMap.toFun
h : (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) = (↑g : P →ᵃ[R] Q)
⊢ { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = g
have mk : ∀ (toAffineMap_1 : P →ᵃ[R] Q) (cont_1 : Continuous toAffineMap_1.toFun)
  (h :
    (↑{ toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } : P →ᵃ[R] Q) =
      (↑{ toAffineMap := toAffineMap_1, cont := cont_1 : P →ᴬ[R] Q } : P →ᵃ[R] Q)),
  { toAffineMap := toAffineMap, cont := cont : P →ᴬ[R] Q } = { toAffineMap := toAffineMap_1, cont := cont_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f g : P →ᴬ[R] Q
h : Eq (α := C(P, Q)) (↑f : C(P, Q)) (↑g : C(P, Q))
⊢ f = g
have h₁ : ∀ (a : P), Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) a : Q) ((g : (a : P) → Q) a : Q)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
h : Continuous (↑f : P →ᵃ[R] Q).toFun
⊢ { toAffineMap := (↑f : P →ᵃ[R] Q), cont := h : P →ᴬ[R] Q } = f
have h₁ : ∀ (x : P),
  Eq.{u_5 + 1} (α := Q) (({ toAffineMap := (↑f : P →ᵃ[R] Q), cont := h : P →ᴬ[R] Q } : (a : P) → Q) x : Q)
    ((f : (a : P) → Q) x : Q)
Tactic: ext