awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst_1] s
have inr : IsOpen[inst] (f ⁻¹' s ∩ (φ e).source)
Tactic: rw [← (φ e).isOpen_symm_image_iff_of_subset_target this,
      (φ e).symm_image_eq_source_inter_preimage this, (hφ e).2, inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst] (f ⁻¹' s ∩ (φ e).source)
have h₁ : f ⁻¹' s ∩ (φ e).source = f ⁻¹' s ∩ V' e
Tactic: convert! h using 1
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ f ⁻¹' s ∩ (φ e).source = f ⁻¹' s ∩ V' e
have h₁ : ∀ (e' : E) (h : e' ∈ f ⁻¹' s ∩ (φ e).source), e' ∈ V (↑e : E)
Tactic: refine inter_eq_inter_iff_left.mpr ⟨fun e' h ↦ h.2.2, fun e' h ↦ ⟨?_ , h.2⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h_1 : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_2 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this_4 : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
s : Set X
hs : s ⊆ U'
h_3 : IsOpen[inst] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
e' : E
h : e' ∈ f ⁻¹' s ∩ (φ e).source
⊢ e' ∈ V (↑e : E)
have h₁ : ∀ e'' ∈ V (↑e : E), ∀ (mem : e'' ∈ (φ e).source) (eq : f e'' = f e'), e' ∈ V (↑e : E)
Tactic: have ⟨e'', ⟨_, mem⟩, eq⟩ := mem_iInter.mp (hs h.1).2 e
-- Lean 4 proof step from Mathlib.Topology.Covering.Basic (goal)
Goal:
E : Type u_1
X : Type u_2
inst : TopologicalSpace E
inst_1 : TopologicalSpace X
f : E → X
inst_2 : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ (φ : OpenPartialHomeomorph E X), e ∈ φ.source ∧ (↑φ : E → X) = f
this_1 : DiscreteTopology.{u_1} (↑(f ⁻¹' {x}) : Type u_1)
φ : (e : (↑(f ⁻¹' {x}) : Type u_1)) → OpenPartialHomeomorph E X
hφ : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), (↑e : E) ∈ (φ e).source ∧ (↑(φ e) : E → X) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : (e : (↑(f ⁻¹' {x}) : Type u_1)) → Set E := fun (e : (↑(f ⁻¹' {x}) : Type u_1)) ↦ V (↑e : E) ∩ (φ e).source
hV' : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), IsOpen[inst] (V' e)
this_2 : ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ (e : (↑(f ⁻¹' {x}) : Type u_1)), V' e
h_1 : Nonempty.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst_1] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ (e : (↑(f ⁻¹' {x}) : Type u_1)), f '' V' e
this_3 : Finite.{u_1 + 1} (↑(f ⁻¹' {x}) : Type u_1)
hU' : IsOpen[inst_1] U'
hUV : ∀ (e : (↑(f ⁻¹' {x}) : Type u_1)), U' ⊆ f '' V' e
this : Nonempty E
e : (↑(f ⁻¹' {x}) : Type u_1)
⊢ InjOn f (V' e)
have h₁ : (↑(φ e) : E → X) = f
Tactic: convert! ← (φ e).injOn.mono inter_subset_right
-- 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
S S' : Subgroup G
eq : S = S'
⊢ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S ↔ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S'
have rw : IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S' ↔ IsQuotientCoveringMap.{u_1, u_2, u_3} f ↥S'
Tactic: rw [eq]
-- 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
h : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
⊢ g = g'
have have : ∀ (U : Set E) (heU : U ∈ 𝓝 e) (hU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1), g = g'
Tactic: have ⟨U, heU, hU⟩ := h.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
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
⊢ IsQuotientCoveringMap f G
have h₁ : f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f)
Tactic: convert! h.homeomorph_comp φ.symm
-- 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
Y : Type u_4
inst_4 : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap.{u_1, u_4, u_3} (X := Y) ((⇑φ : (a : X) → Y) ∘ f) G
⊢ f = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f)
have h₁ : ∀ (x : E), f x = Function.comp.{u_1 + 1, u_4 + 1, u_2 + 1} (β := Y) (⇑φ.symm : (a : Y) → X) ((⇑φ : (a : X) → Y) ∘ f) x
Tactic: ext
-- 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
⊢ Trivialization G f
have pGE : ∀ (g : G) (e : E), f (g • e) = f e
Tactic: have pGE (g : G) e : f (g • e) = f e := hfG.mpr ⟨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
⊢ f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
have h : ∀ (e : E), e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) 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
e : E
⊢ e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
have h : e ∈ f ⁻¹' f '' U →
  ∀ (e' : E) (heU : e' ∈ U) (he : f e' = f e), Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
Tactic: refine ⟨fun ⟨e', heU, 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
e : E
h :
  e ∈ f ⁻¹' f '' U →
    ∀ (e' : E) (heU : e' ∈ U) (he : f e' = f e), Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
⊢ e ∈ f ⁻¹' f '' U ↔ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
have h₁ : Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e → e ∈ f ⁻¹' f '' U
Tactic: refine ⟨fun ⟨e', heU, 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
e : E
h : e ∈ f ⁻¹' f '' U
e' : E
heU : e' ∈ U
he : f e' = f e
⊢ Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
have h : ∀ (g : G) (heU : (fun (m : G) ↦ m • e) g ∈ U) (he : f ((fun (m : G) ↦ m • e) g) = f e),
  Membership.mem (γ := Set E) (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U) e
Tactic: obtain ⟨g, rfl⟩ := hfG.mp he
Cleared hypotheses: e', heU, he
-- 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
⊢ Trivialization G f
have preim_im : f ⁻¹' f '' U = ⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U
Tactic: have preim_im : f ⁻¹' f '' U = ⋃ g : G, (g • ·) ⁻¹' U := by
    ext e; refine ⟨fun ⟨e', heU, he⟩ ↦ ?_, ?_⟩
    · obtain ⟨g, rfl⟩ := hfG.mp he; exact ⟨_, ⟨g, rfl⟩, heU⟩
    · intro ⟨_, ⟨g, rfl⟩, hg⟩; exact ⟨_, hg, pGE g e⟩
-- 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
⊢ Trivialization G f
have this : Nonempty (X → E)
Tactic: have : Nonempty (X → E) := ⟨Function.surjInv hf.surjective⟩
-- 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)
⊢ Trivialization G f
have refine_1 : IsOpen[inst_1] (f '' U)
Tactic: refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.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
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)
refine_1 : IsOpen[inst_1] (f '' U)
⊢ Trivialization G f
have refine_2 : ∀ (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)
Tactic: refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.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
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)
refine_1 : IsOpen[inst_1] (f '' U)
refine_2 :
  ∀ (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)
⊢ Trivialization G f
have refine_3 : ∀ (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₂
Tactic: refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.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
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)
refine_1 : IsOpen[inst_1] (f '' U)
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (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₂
⊢ Trivialization G f
have refine_4 : ∀ (i : G), Set.SurjOn f ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) i) (f '' U)
Tactic: refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.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
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)
refine_1 : IsOpen[inst_1] (f '' U)
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (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₂
refine_4 : ∀ (i : G), Set.SurjOn f ((fun (g : G) ↦ ((fun (x : E) ↦ g • x) ⁻¹' U : Set E)) i) (f '' U)
⊢ Trivialization G f
have refine_5 : ∀ {g₁ g₂ : G} (hne : g₁ ≠ g₂) (e : E),
  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),
      Eq.{u_1 + 1} (α := E) ((fun (x : E) ↦ (g₁ * g₂⁻¹) • x) ((fun (x : E) ↦ g₂ • x) e)) ((fun (x : E) ↦ g₁ • x) e)
Tactic: refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.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
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)
⊢ IsOpen[inst_1] (f '' U)
have refine_1 : IsOpen[inst] (⋃ (g : G), (fun (x : E) ↦ g • x) ⁻¹' U)
Tactic: rw [← hf.isOpen_preimage, preim_im]