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
inst_2 : Group E
inst_3 : IsTopologicalGroup E
inst_4 : Group X
f : E →* X
hf : IsQuotientMap.{u_1, u_2} (X := E) (Y := X) (⇑f : (a : E) → X)
disc : IsDiscrete (↑f.ker : Set E)
x x_1 : E
⊢ Eq.{u_2 + 1} (α := X) ((f : (a : E) → X) x : X) ((f : (a : E) → X) x_1 : X) ↔ x_1 * x⁻¹ ∈ f.ker
have rw : Eq.{u_2 + 1} (α := X) ((f : (a : E) → X) (x_1 * x⁻¹) : X) (1 : X) ↔ x_1 * x⁻¹ ∈ f.ker
Tactic: rw [eq_comm, ← mul_inv_eq_one, ← map_inv, ← map_mul]
-- Lean 4 proof step from Mathlib.Topology.Covering.Quotient (goal)
Goal:
G : Type u_4
inst : CommGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
e₁ e₂ : G
⊢ e₁⁻¹ * e₂ ∈ S ↔ e₂ * e₁⁻¹ ∈ S
have rw : e₂ * e₁⁻¹ ∈ S ↔ e₂ * e₁⁻¹ ∈ S
Tactic: rw [mul_comm]
-- 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
h : IsQuotientCoveringMap f G
⊢ IsCoveringMapOn f Set.univ
have this : ContinuousConstSMul G E
Tactic: have := h.toContinuousConstSMul
-- 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
this : ContinuousConstSMul G E
⊢ IsCoveringMapOn f Set.univ
have h₁ : f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} = Set.univ
Tactic: convert! ← h.isCoveringMapOn_of_smul_disjoint h.apply_eq_iff_mem_orbit fun 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
h₁ : f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} = Set.univ
⊢ IsCoveringMapOn f Set.univ
have convert! : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
Tactic: convert! ← h.isCoveringMapOn_of_smul_disjoint h.apply_eq_iff_mem_orbit fun 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
⊢ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥} = Set.univ
have h₁ : ∀ (x : X), x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
Tactic: refine Set.eq_univ_of_forall fun x ↦ ?_
-- 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
this : ContinuousConstSMul G E
x : X
⊢ x ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
have h₁ : ∀ (e : E), f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
Tactic: obtain ⟨e, rfl⟩ := h.surjective x
Cleared hypotheses: x
-- 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
this : ContinuousConstSMul G E
e : E
⊢ f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
have h₁ : ∀ (U : Set E) (hU : U ∈ 𝓝 e) (hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1),
  f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
Tactic: have ⟨U, hU, hGU⟩ := h.disjoint 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ f e ∈ f '' {e : E | Eq (α := Subgroup G) (MulAction.stabilizer G e) ⊥}
have hU₁ : e ∈ U
Tactic: replace hU := mem_of_mem_nhds hU
Cleared hypotheses: hU
-- 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
this : ContinuousConstSMul G E
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
have have : ∀ (U : Set E) (hU : U ∈ 𝓝 e) (hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1),
  ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g • e = e
Tactic: have ⟨U, hU, hGU⟩ := 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
h : IsQuotientCoveringMap f G
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
g : G
hg : ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty
⊢ g • e = e
have rw : HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 e = e
Tactic: rw [hGU g hg, one_smul]
-- 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
this : ContinuousConstSMul G E
e : E
U : Set E
hU : U ∈ 𝓝 e
hGU : ∀ (g : G), ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty → g = 1
g : G
hg : ((fun (x : E) ↦ g • x) '' U ∩ U).Nonempty
rw : HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 e = e
⊢ g • e = e
have rw₁ : e = e
Tactic: rw [hGU g hg, one_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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
⊢ g = 1
have this : IsCancelSMul G E
Tactic: have := h.2.2.2.1
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ g = 1
have apply : g • (↑x : E) = HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 (↑x : E)
Tactic: apply IsCancelSMul.right_cancel _ _ x.1
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ g • (↑x : E) = HSMul.hSMul.{u_3, u_1, u_1} (α := G) 1 (↑x : E)
have simp_rw : (↑y : E) = (↑x : E)
Tactic: simp_rw [← eq, one_smul]
-- 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 :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ (↑y : E) = (↑x : E)
have refine : Eq.{u_2 + 1} (α := X) (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) y).1 : X)
  (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X)
Tactic: refine congr($(H.injective <| Prod.ext (Subtype.ext ?_) <| hy.trans hx.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
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left : DiscreteTopology.{u_1} (↑(f ⁻¹' {f e}) : Type u_1)
U : Set X
heU : f e ∈ U
hU : IsOpen[inst_1] U
hfU : IsOpen[inst] (f ⁻¹' U)
H : (↑(f ⁻¹' U) : Type u_1) ≃ₜ Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)
hH :
  ∀ (x : (↑(f ⁻¹' U) : Type u_1)),
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X) = f (↑x : E)
g : G
x : { x : E // x ∈ f ⁻¹' U }
hx :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    x
y : { x : E // x ∈ f ⁻¹' U }
hy :
  Membership.mem (γ := Set { x : E // x ∈ f ⁻¹' U })
    (Set.preimage (β := (↑(f ⁻¹' {f e}) : Type u_1))
      (Function.comp (β := Prod.{u_2, u_1} (↑U : Type u_2) (↑(f ⁻¹' {f e}) : Type u_1)) Prod.snd
        (⇑H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)))
      {((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1))
            (Subtype.mk (p := fun (x : E) ↦ x ∈ f ⁻¹' U) e heU)).2})
    y
eq : (↑y : E) = (fun (x : E) ↦ g • x) (↑x : E)
this : IsCancelSMul G E
⊢ Eq.{u_2 + 1} (α := X) (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) y).1 : X)
    (↑((H : (a : (↑(f ⁻¹' U) : Type u_1)) → (↑U : Type u_2) × (↑(f ⁻¹' {f e}) : Type u_1)) x).1 : X)
have simp_rw : f (↑y : E) = f (↑x : E)
Tactic: simp_rw [hH]
-- Lean 4 proof step from Mathlib.Topology.Defs.Induced (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
h : ∀ t_1 ∈ S, ∃ (t_2 : Set Y), IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S
have choose! : ∀ (g : (t : Set X) → Set Y) (hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)) (hfg : ∀ t ∈ S, f ⁻¹' g t = t),
  ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S
Tactic: choose! g hgo hfg using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Defs.Induced (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ ∃ (t_1 : Set Y), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = ⋃₀ S
have refine : f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S
Tactic: refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Defs.Induced (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
S : Set (Set X)
g : (t : Set X) → Set Y
hgo : ∀ t_1 ∈ S, IsOpen[t] (g t_1)
hfg : ∀ t ∈ S, f ⁻¹' g t = t
⊢ f ⁻¹' ⋃₀ (g '' S) = ⋃₀ S
have rw : Eq.{u_1 + 1} (α := Set X) (⋃ y ∈ S, f ⁻¹' g y) (⋃ i ∈ S, i)
Tactic: rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : s ∈ 𝓝 a
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)
have hs₁ : ∃ (i_1 : Set β), (i a ∈ i_1 ∧ IsOpen[inst_1] i_1) ∧ i ⁻¹' i_1 ⊆ s
Tactic: rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
hs : ∃ (i_1 : Set β), (i a ∈ i_1 ∧ IsOpen[inst_1] i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)
have rcases : ∀ (U : Set β) (sub : i ⁻¹' U ⊆ s) (haU : i a ∈ U) (hUo : IsOpen[inst_1] U), closure[inst_1] (i '' s) ∈ 𝓝 (i a)
Tactic: rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
s : Set α
a : α
di : IsDenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen[inst_1] U
⊢ closure[inst_1] (i '' s) ∈ 𝓝 (i a)
have refine : U ⊆ closure[inst_1] (i '' s)
Tactic: refine mem_of_superset (hUo.mem_nhds haU) ?_
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s
have refine : ∀ (H : Dense (i '' s)) (x : α), x ∈ closure[inst] s
Tactic: refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure[inst] s
have rw : Membership.mem (γ := Set α) univ x
Tactic: rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅
have refine : ∀ (x : α) (hx : x ∈ interior s), False
Tactic: refine eq_empty_iff_forall_notMem.2 fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : x ∈ interior s
⊢ False
have hx₁ : s ∈ 𝓝 x
Tactic: rw [mem_interior_iff_mem_nhds] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
⊢ False
have this : closure[inst_1] (i '' s) ∈ 𝓝 (i x)
Tactic: have := di.closure_image_mem_nhds hx
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : closure[inst_1] (i '' s) ∈ 𝓝 (i x)
⊢ False
have this₁ : i '' s ∈ 𝓝 (i x)
Tactic: rw [(hs.image di.continuous).isClosed.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : T2Space β
di : IsDenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
⊢ False
have rcases : ∀ (y : β) (hyi : y ∈ (range i)ᶜ) (hys : y ∈ i '' s), False
Tactic: rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
Tactic: have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
have lim1₁ : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
Tactic: replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
Cleared hypotheses: lim1
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
have lim1₁ : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
Tactic: rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1
Cleared hypotheses: lim1
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
Tactic: have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
-- Lean 4 proof step from Mathlib.Topology.DenseEmbedding (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
i : α → β
inst_2 : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
have lim2₁ : comap i (map h (𝓝 d)) ≤ 𝓝 a
Tactic: rw [← di.nhds_eq_comap] at lim2
Cleared hypotheses: lim2