awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
⊢ IsOpen[inst] (f ⁻¹' W)
have h : f ⁻¹' W = ⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
Tactic: convert! isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
⊢ f ⁻¹' W = ⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
have h : ∀ (e : E),
  e ∈ f ⁻¹' W ↔
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
Tactic: ext e
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
⊢ e ∈ f ⁻¹' W ↔
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h : ∀ (hW : e ∈ f ⁻¹' W),
  Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
Tactic: refine ⟨fun hW ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
h :
  ∀ (hW : e ∈ f ⁻¹' W),
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
⊢ e ∈ f ⁻¹' W ↔
    Membership.mem (γ := Set E)
      (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h₁ : Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e →
  e ∈ f ⁻¹' W
Tactic: refine ⟨fun hW ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h : ∀ (e' : E) (he' : e' ∈ U) (hfe : f e' = f e),
  Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
Tactic: have ⟨e', he', hfe⟩ := hWU hW
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
e' : E
he' : e' ∈ U
hfe : f e' = f e
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h : ∀ (g' : G) (he' : (fun (m : G) ↦ m • e) g' ∈ U) (hfe : f ((fun (m : G) ↦ m • e) g') = f e),
  Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
Tactic: obtain ⟨g', rfl⟩ := hfG.mp hfe
Cleared hypotheses: e', he', hfe
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h : (fun (x : E) ↦ (g⁻¹ * g') • x) e ∈ f ⁻¹' W
Tactic: refine ⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
h : (fun (x : E) ↦ (g⁻¹ * g') • x) e ∈ f ⁻¹' W
⊢ Membership.mem (γ := Set E)
    (⋃ (i : G), (fun (x : E) ↦ i • x) ⁻¹' (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)) e
have h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) ((fun (x : E) ↦ (g⁻¹ * g') • x) e)
Tactic: refine ⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
⊢ Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
    ((fun (x : E) ↦ (g⁻¹ * g') • x) e)
have apply : Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ g • x) ((fun (x : E) ↦ (g⁻¹ * g') • x) e)) ((fun (m : G) ↦ m • e) g')
Tactic: apply Set.mem_of_eq_of_mem _ he'
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst] (f ⁻¹' W ∩ (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g)
e : E
hW : e ∈ f ⁻¹' W
g' : G
he' : (fun (m : G) ↦ m • e) g' ∈ U
hfe : f ((fun (m : G) ↦ m • e) g') = f e
simp_rw simp_rw₁ : g • (g⁻¹ * g') • e = g' • e
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ g • x) ((fun (x : E) ↦ (g⁻¹ * g') • x) e)) ((fun (m : G) ↦ m • e) g')
have simp_rw₂ : g • g⁻¹ • g' • e = g' • e
Tactic: simp_rw [mul_smul, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e₁ : E
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he : f e₁ = f e₂
⊢ e₁ = e₂
have he₁ : f (g • e₁) = f (g • e₂)
Tactic: rw [← pGE g, ← pGE g e₂] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e₁ : E
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he : f (g • e₁) = f (g • e₂)
⊢ e₁ = e₂
have refine_3 : ∀ (g' : G) (he : (fun (m : G) ↦ m • g • e₂) g' = g • e₁), e₁ = e₂
Tactic: have ⟨g', he⟩ := hfG.mp he
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
e₁ : E
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₁
e₂ : E
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g) e₂
he_1 : f (g • e₁) = f (g • e₂)
g' : G
he : (fun (m : G) ↦ m • g • e₂) g' = g • e₁
⊢ e₁ = e₂
have refine_3 : (fun (m : G) ↦ m • g • e₂) 1 = g • e₂
Tactic: rw [← smul_left_cancel_iff g, ← he, disjoint g' ⟨_, ⟨_, h₂, he⟩, h₁⟩]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst_5 : TopologicalSpace G
inst_6 : DiscreteTopology G
U : Set E
open_U : IsOpen[inst] U
disjoint : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g₁ g₂ : G
hne : g₁ ≠ g₂
e : E
h :
  Membership.mem (γ := Set E)
    ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₁ ⊓
      (fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₂)
    e
h₁ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₁) e
h₂ : Membership.mem (γ := Set E) ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) g₂) e
refine_5 refine_5₁ : (g₁ * g₂⁻¹) • g₂ • e = g₁ • e
⊢ Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ (g₁ * g₂⁻¹) • x) ((fun (x : E) ↦ g₂ • x) e)) ((fun (x : E) ↦ g₁ • x) e)
have refine_5₂ : g₁ • g₂⁻¹ • g₂ • e = g₁ • e
Tactic: simp_rw [mul_smul, inv_smul_smul]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this : TopologicalSpace G := ⊥
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})
have this₁ : DiscreteTopology G
Tactic: have : DiscreteTopology G := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this_2 : DiscreteTopology G
this : ∀ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}, ∃ (t : Trivialization G f), x ∈ t.baseSet
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})
have choose : ∀ (t : (x : X) → x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} → Trivialization G f)
  (ht : ∀ (x : X) (a : x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}), x ∈ (t x a).baseSet),
  IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})
Tactic: choose t ht using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
⊢ IsCoveringMapOn f (f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥})
have suffices : ∀ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}, ∃ (t : Trivialization G f), x ∈ t.baseSet
Tactic: suffices ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t : Trivialization G f, x ∈ t.baseSet by
    choose t ht using this; exact IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
⊢ ∃ (t : Trivialization G f), f e ∈ t.baseSet
have have : ∀ (U : Set E) (heU : U ∈ 𝓝 e) (hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e),
  ∃ (t : Trivialization G f), f e ∈ t.baseSet
Tactic: have ⟨U, heU, hU⟩ := disjoint e
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ ∃ (t : Trivialization G f), f e ∈ t.baseSet
have refine : ∀ (g : G) (hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty), g = 1
Tactic: refine ⟨hf.trivializationOfSMulDisjoint hfG (interior U) isOpen_interior
    fun g hg ↦ ?_, e, mem_interior_iff_mem_nhds.mpr heU, rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ g = 1
have rw : Membership.mem (γ := Subgroup G) (MulAction.stabilizer G e) g
Tactic: rw [← Subgroup.mem_bot, ← he]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
G : Type u_3
inst_2 : Group G
inst_3 : MulAction G E
hf : IsQuotientMap f
inst_4 : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this_1 : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : Membership.mem (γ := Set E) {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun (x : E) ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ (fun (x : E) ↦ g • x) '' interior U ∩ interior U ⊆ (fun (x : E) ↦ g • x) '' U ∩ U
have grw : (fun (x : E) ↦ g • x) '' U ∩ U ⊆ (fun (x : E) ↦ g • x) '' U ∩ U
Tactic: grw [interior_subset]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₂ * e₁⁻¹ ∈ G
e : E
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ g * x) '' U ∩ U).Nonempty → g = 1
s : ↥G
hs : ((fun (x : E) ↦ s • x) '' (U * {e}) ∩ (U * {e})).Nonempty
⊢ ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty
have obtain : ∀ (x : E) (hx : x ∈ U) (y : E) (hy : y ∈ U) (g : E)
  (he :
    Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) y g) ((fun (x : E) ↦ s • x) ((fun (x1 x2 : E) ↦ x1 * x2) x g))),
  ((fun (x : E) ↦ (↑s : E) * x) '' U ∩ U).Nonempty
Tactic: obtain ⟨_, ⟨_, ⟨x, hx, _, rfl, rfl⟩, rfl⟩, y, hy, g, rfl, he⟩ := hs
Cleared hypotheses: e, hs
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
hf : IsQuotientMap f
inst_2 : Group E
inst_3 : IsTopologicalGroup E
G : Subgroup E
hG : IsDiscrete (↑G : Set E)
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G
e : E
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 1) U
left : U⁻¹ = U
disj : ∀ g ∈ G, ((fun (x : E) ↦ x * g) '' U ∩ U).Nonempty → g = 1
x : ↥G.op
s : E
hS : { unop' := s : PreOpposite E } ∈ G.op
hs :
  ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x) '' ({e} * U) ∩
      ({e} * U)).Nonempty
⊢ ((fun (x : E) ↦
          x *
            MulOpposite.unop
              (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
        U ∩
      U).Nonempty
have obtain : ∀ (x : E) (hx : x ∈ U) (g y : E) (hy : y ∈ U)
  (he :
    Eq.{u_1 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 * x2) g y)
      ((fun (x : E) ↦ Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS • x)
        ((fun (x1 x2 : E) ↦ x1 * x2) g x))),
  ((fun (x : E) ↦
          x *
            MulOpposite.unop
              (↑(Subtype.mk (p := fun (x : Eᵐᵒᵖ) ↦ x ∈ G.op) { unop' := s : PreOpposite E } hS) : Eᵐᵒᵖ)) ''
        U ∩
      U).Nonempty
Tactic: obtain ⟨_, ⟨_, ⟨_, rfl, x, hx, rfl⟩, rfl⟩, g, rfl, y, hy, he⟩ := hs
Cleared hypotheses: e, hs