awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = sSup (S₁ ∪ S₂)
have neg : s = sSup S₁ ⊔ sSup S₂
Tactic: rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup S₁ ⊔ sSup S₂
⊢ s = sSup (S₁ ∪ S₂)
have neg₁ : s = s ⊓ z₁ ⊔ sSup S₂
Tactic: rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup S₁ ⊔ sSup S₂
neg₁ : s = s ⊓ z₁ ⊔ sSup S₂
⊢ s = sSup (S₁ ∪ S₂)
have neg₂ : s = s ⊓ z₁ ⊔ s ⊓ z₂
Tactic: rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup S₁ ⊔ sSup S₂
neg₁ : s = s ⊓ z₁ ⊔ sSup S₂
neg₂ : s = s ⊓ z₁ ⊔ s ⊓ z₂
⊢ s = sSup (S₁ ∪ S₂)
have neg₃ : s = s ⊓ (z₁ ⊔ z₂)
Tactic: rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup S₁ ⊔ sSup S₂
neg₁ : s = s ⊓ z₁ ⊔ sSup S₂
neg₂ : s = s ⊓ z₁ ⊔ s ⊓ z₂
neg₃ : s = s ⊓ (z₁ ⊔ z₂)
⊢ s = sSup (S₁ ∪ S₂)
have neg₄ : s ≤ z₁ ⊔ z₂
Tactic: rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : IsClosed[inst] s
⊢ ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S
have lift : ∀ (s : Closeds α),
  ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ (↑s : Set α) = ⋃₀ S
Tactic: lift s to Closeds α using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
⊢ ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ (↑s : Set α) = ⋃₀ S
have rcases : ∀ (S : Set (Closeds α)) (hSf : S.Finite) (hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)),
  ∃ (S_1 : Set (Set α)),
    S_1.Finite ∧ (∀ t ∈ S_1, IsClosed[inst] t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ (↑(sSup S) : Set α) = ⋃₀ S_1
Tactic: rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
⊢ ∃ (S_1 : Set (Set α)),
    S_1.Finite ∧ (∀ t ∈ S_1, IsClosed[inst] t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ (↑(sSup S) : Set α) = ⋃₀ S_1
have refine : (↑(sSup S) : Set α) = ⋃₀ (SetLike.coe '' S)
Tactic: refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
    ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
⊢ (↑(sSup S) : Set α) = ⋃₀ (SetLike.coe '' S)
have lift : ∀ (S : Finset (Closeds α)) (hS : ∀ t ∈ (↑S : Set (Closeds α)), IsIrreducible (↑t : Set α)),
  (↑(sSup (↑S : Set (Closeds α))) : Set α) = ⋃₀ (SetLike.coe '' (↑S : Set (Closeds α)))
Tactic: lift S to Finset (Closeds α) using hSf
Cleared hypotheses: S, hSf, hS
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
⊢ (irreducibleComponents α).Finite
have obtain : ∀ (S : Set (Set α)) (hSf : S.Finite) (hSc : ∀ t ∈ S, IsClosed[inst] t) (hSi : ∀ t ∈ S, IsIrreducible t)
  (hSU : Set.univ = ⋃₀ S), (irreducibleComponents α).Finite
Tactic: obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
    NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ (irreducibleComponents α).Finite
have refine : ∀ (s : Set α) (hs : s ∈ irreducibleComponents α), s ∈ S
Tactic: refine hSf.subset fun s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
have lift : ∀ (S : Finset (Set α)) (hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t)
  (hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t) (hSU : Set.univ = ⋃₀ (↑S : Set (Set α))), s ∈ (↑S : Set (Set α))
Tactic: lift S to Finset (Set α) using hSf
Cleared hypotheses: S, hSf, hSc, hSi, hSU
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t
hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t
hSU : Set.univ = ⋃₀ (↑S : Set (Set α))
⊢ s ∈ (↑S : Set (Set α))
have rcases : ∀ (t : Set α) (htS : t ∈ S) (ht : s ⊆ t), s ∈ (↑S : Set (Set α))
Tactic: rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t
hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t
hSU : Set.univ = ⋃₀ (↑S : Set (Set α))
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ (↑S : Set (Set α))
have rwa : t ∈ (↑S : Set (Set α))
Tactic: rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z
have hα : (irreducibleComponents α).Finite
Tactic: have hα : (irreducibleComponents α).Finite := finite_irreducibleComponents
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z
have hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
Tactic: have hZ := closure_sUnion_irreducibleComponents_diff_singleton hα Z H
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z
have refine_1 : IsOpen[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ
Tactic: refine ⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
refine_1 : IsOpen[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z
have refine_2 : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty
Tactic: refine ⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ IsOpen[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ
have refine_1 : IsClosed[inst] (⋃ i ∈ irreducibleComponents α \ {Z}, i)
Tactic: rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty
have refine_2 : ∀ (hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅), closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ ≠ Z
Tactic: contrapose! hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
⊢ closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ ≠ Z
have refine_2 : Z.Nonempty
Tactic: rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
a b : α
hab : a ≤ b
⊢ Membership.mem (γ := Set (Set α)) (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α)) {a, b}
have h : Eq (α := Set α) ((fun (c : Chain α) ↦ (range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (Chain.pair a b hab)) {a, b}
Tactic: use Chain.pair a b hab
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
⊢ ωScottContinuous f ↔ Continuous[inst_1, _] f
have rw : ScottContinuousOn (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α)) f ↔ Continuous[inst_1, _] f
Tactic: rw [ωScottContinuous, scottContinuousOn_iff_continuous (fun a b hab => by
    use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
rw : ScottContinuousOn (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α)) f ↔ Continuous[inst_1, _] f
⊢ ωScottContinuous f ↔ Continuous[inst_1, _] f
have rw₁ : Continuous[inst_1, _] f ↔ Continuous[inst_1, _] f
Tactic: rw [ωScottContinuous, scottContinuousOn_iff_continuous (fun a b hab => by
    use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ t
⊢ ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ ⋃₀ s
have h : ∀ (x : α), Membership.mem (⋃₀ s) = sSup s
Tactic: convert! CompleteLattice.ωScottContinuous.sSup hs
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)
have left : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ ωSup c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
c : Chain α
left : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ ωSup c
⊢ IsωSup c (ωSup c)
have right : ∀ (y : α), (∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ y) → ωSup c ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
hse : s ⊆ e.source
⊢ IsOpen[inst_1] ((↑e : X → Y) '' s)
have rw : IsOpen[inst_1] (e.target ∩ (↑e.symm : Y → X) ⁻¹' s)
Tactic: rw [(image_eq_target_inter_inv_preimage (e := e) hse)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen[inst] ((↑e.symm : Y → X) '' t) ↔ IsOpen[inst_1] t
have refine : ∀ (h : IsOpen[inst] ((↑e.symm : Y → X) '' t)), IsOpen[inst_1] t
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
⊢ (↑e.symm : Y → X) '' t ⊆ e.source
have rw : e.source ∩ (↑e : X → Y) ⁻¹' t ⊆ e.source
Tactic: rw [e.symm_image_eq_source_inter_preimage hs]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
⊢ IsOpen[inst_1] t
have hs' : (↑e.symm : Y → X) '' t ⊆ e.source
Tactic: have hs' : e.symm '' t ⊆ e.source := by
    rw [e.symm_image_eq_source_inter_preimage hs]
    apply Set.inter_subset_left
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
h : IsOpen[inst] ((↑e.symm : Y → X) '' t)
hs' : (↑e.symm : Y → X) '' t ⊆ e.source
⊢ IsOpen[inst_1] t
have rw : IsOpen[inst_1] ((↑e.toPartialEquiv : X → Y) '' (↑e.symm : Y → X) '' t)
Tactic: rw [← e.image_symm_image_of_subset_target hs]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst] s
have rw : IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst_1] ((↑e.symm.symm : X → Y) '' s)
Tactic: rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
rw : IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst_1] ((↑e.symm.symm : X → Y) '' s)
⊢ IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst] s
have rw₁ : IsOpen[inst_1] ((↑e : X → Y) '' s) ↔ IsOpen[inst_1] ((↑e : X → Y) '' s)
Tactic: rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) x)) ⊓ 𝓟 e.source
have lift : ∀ (x : { x : X // x ∈ e.source }), 𝓝 (↑x : X) = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X))) ⊓ 𝓟 e.source
Tactic: lift x to e.source using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : { x : X // x ∈ e.source }
⊢ 𝓝 (↑x : X) = comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X))) ⊓ 𝓟 e.source
have rw : map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
    (comap.{u_1, u_3} (β := (↑e.target : Type u_3))
      (⇑e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3))
      (comap (Subtype.val (p := fun (x : Y) ↦ x ∈ e.target))
        (𝓝 (↑((e.toHomeomorphSourceTarget : (a : (↑e.source : Type u_1)) → (↑e.target : Type u_3)) x) : Y)))) =
  map (α := { x : X // x ∈ e.source }) (Subtype.val (p := fun (x : X) ↦ x ∈ e.source))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ e.source)) (comap (↑e : X → Y) (𝓝 ((↑e : X → Y) (↑x : X)))))
Tactic: rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
    e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ e.source
have rw : Membership.mem (γ := Set X) univ x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
inst_4 : TopologicalSpace Z
inst_5 : TopologicalSpace Z'
e : OpenPartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ e.target
have rw : Membership.mem (γ := Set Y) univ x
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpenEmbedding (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y))
have refine : ∀ (V : Set (↑e.source : Type u_1)) (hV : IsOpen[instTopologicalSpaceSubtype] V),
  IsOpen[inst_1] (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) '' V)
Tactic: refine .of_continuous_injective_isOpenMap (e.continuousOn.comp_continuous
    continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
V : Set (↑e.source : Type u_1)
hV : IsOpen[instTopologicalSpaceSubtype] V
⊢ IsOpen[inst_1] (e.source.restrict (π := fun (a : X) ↦ Y) (↑e : X → Y) '' V)
have rw : IsOpen[inst_1] ((↑e : X → Y) '' Subtype.val (p := fun (x : X) ↦ x ∈ e.source) '' V)
Tactic: rw [Set.restrict_eq, Set.image_comp]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : X
⊢ (↑(toOpenPartialHomeomorph f h).symm : Y → X) (f x) = x
have h₁ : x ∈ (toOpenPartialHomeomorph f h).source
Tactic: rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.left_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : IsOpenEmbedding f
inst_2 : Nonempty X
x : Y
hx : x ∈ range f
⊢ f ((↑(toOpenPartialHomeomorph f h).symm : Y → X) x) = x
have h₁ : x ∈ (toOpenPartialHomeomorph f h).target
Tactic: rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.right_inv]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Opens X
hs : Nonempty.{u_1 + 1} ↥s
⊢ (s.openPartialHomeomorphSubtypeCoe hs).target = (↑s : Set X)
have simp : {x : X | x ∈ s.carrier} = (↑s : Set X)
Tactic: simp only [openPartialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (goal)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have obtain : ∀ (x : X) (y : Y), eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
Tactic: obtain ⟨⟨x, y⟩, -⟩ := id h
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have this : Nonempty X
Tactic: haveI : Nonempty X := ⟨x⟩
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Constructions (hypothesis)
Goal:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace X'
inst_2 : TopologicalSpace Y
inst_3 : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this : Nonempty X
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
have this₁ : Nonempty X'
Tactic: haveI : Nonempty X' := ⟨eX x⟩