awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
have h_ant₁ : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
Tactic: rw [Ici, ← antitone_add_nat_iff_antitoneOn_nat_Ici] at h_ant
Cleared hypotheses: h_ant, h_bdd
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : Antitone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
have rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨅ (x : ℕ), f (x + k)))
Tactic: rw [← tendsto_add_atTop_iff_nat k, ← range_add_eq_image_Ici, sInf_range]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : Monotone f
h_bdd : BddAbove (range f)
⊢ IsLUB (range f) x
have rw : IsLUB (range f) (⨆ (i : ι), f i)
Tactic: rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciSup h_mon h_bdd)]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : Nonempty ι
inst_2 : IsDirected ι fun (x1 x2 : ι) ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) x
have rw : IsGLB (range f) (⨅ (i : ι), f i)
Tactic: rw [tendsto_nhds_unique h_tto (tendsto_atTop_ciInf h_ant h_bdd)]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ IsLUB (f '' Ici k) x
have rw : IsLUB (f '' Ici k) (sSup (f '' Ici k))
Tactic: rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici h_mon h_bdd)]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
f : ℕ → ℝ
k : ℕ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ IsGLB (f '' Ici k) x
have rw : IsGLB (f '' Ici k) (sInf (f '' Ici k))
Tactic: rw [tendsto_nhds_unique h_tto
    (Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici h_ant h_bdd)]
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
have refine : (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ 1) (⇑SignType.sign : (a : α) → SignType)
Tactic: refine (continuousAt_const : ContinuousAt (fun _ => (1 : SignType)) a).congr ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : 0 < a
⊢ (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ 1) (⇑SignType.sign : (a : α) → SignType)
have rw : ∃ (t : Set α),
  (∀ y ∈ t, Eq (α := SignType) (1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t
Tactic: rw [Filter.EventuallyEq, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
have refine : (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ -1) (⇑SignType.sign : (a : α) → SignType)
Tactic: refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : PartialOrder α
inst_3 : DecidableLT α
inst_4 : OrderTopology α
a : α
h : a < 0
⊢ (nhds a).EventuallyEq (β := SignType) (fun (x : α) ↦ -1) (⇑SignType.sign : (a : α) → SignType)
have rw : ∃ (t : Set α),
  (∀ y ∈ t, Eq (α := SignType) (-1 : SignType) ((SignType.sign : (a : α) → SignType) y : SignType)) ∧ IsOpen t ∧ a ∈ t
Tactic: rw [Filter.EventuallyEq, eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
have inl : ∀ (h_neg : a < 0), ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
Tactic: rcases h.lt_or_gt with (h_neg | h_pos)
-- Lean 4 proof step from Mathlib.Topology.Instances.Sign (goal)
Goal:
α : Type u_1
inst : Zero α
inst_1 : TopologicalSpace α
inst_2 : LinearOrder α
inst_3 : OrderTopology α
a : α
h : a ≠ 0
inl : ∀ (h_neg : a < 0), ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
⊢ ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
have inr : ∀ (h_pos : 0 < a), ContinuousAt (Y := SignType) (⇑SignType.sign : (a : α) → SignType) a
Tactic: rcases h.lt_or_gt with (h_neg | h_pos)
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
have inl : DiscreteTopology ↥(AddSubgroup.zmultiples 0)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
inl : DiscreteTopology ↥(AddSubgroup.zmultiples 0)
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
have inr : ∀ (ha : a ≠ 0), DiscreteTopology ↥(AddSubgroup.zmultiples a)
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 0)
have inl : DiscreteTopology ↥⊥
Tactic: rw [AddSubgroup.zmultiples_zero_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples a)
have inr : ∃ (t : Set ℝ),
  IsOpen t ∧
    Eq (α := Set ↥(AddSubgroup.zmultiples a))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' t) {0}
Tactic: rw [discreteTopology_iff_isOpen_singleton_zero, isOpen_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ (t : Set ℝ),
    IsOpen t ∧
      Eq (α := Set ↥(AddSubgroup.zmultiples a))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' t) {0}
have inr : Eq (α := Set ↥(AddSubgroup.zmultiples a))
  (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|) {0}
Tactic: refine ⟨ball 0 |a|, isOpen_ball, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Eq (α := Set ↥(AddSubgroup.zmultiples a))
    (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
    {0}
have inr : ∀ (x : ℝ) (hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x),
  Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
x : ℝ
hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x
⊢ Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) x hx)
have inr : ∀ (k : ℤ) (hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) (k • a)),
  Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) ⁻¹' ball 0 |a|)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) (k • a) hx) ↔
    Membership.mem (γ := Set ↥(AddSubgroup.zmultiples a)) {0}
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) x) (k • a) hx)
Tactic: obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : Membership.mem (γ := AddSubgroup ℝ) (AddSubgroup.zmultiples a) (k • a)
⊢ LT.lt (α := ℝ) |(↑k : ℝ)| 1 ↔ |k| < 1
have norm_cast : |k| < 1 ↔ |k| < 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)
have apply : IsDiscrete (↑(AddMonoidHom.range (castAddHom ℝ)) : Set ℝ)
Tactic: apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
⊢ IsDiscrete (↑(AddMonoidHom.range (castAddHom ℝ)) : Set ℝ)
have rw : DiscreteTopology ↥(AddSubgroup.zmultiples 1)
Tactic: rw [range_castAddHom, SetLike.isDiscrete_iff_discreteTopology]
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
a : ℝ
ha : a ≠ 0
⊢ Tendsto (α := ℤ) (⇑((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a : ℤ →+ ℝ) : (a : ℤ) → ℝ) Filter.cofinite (cocompact ℝ)
have apply : IsDiscrete (↑(AddMonoidHom.range (G := ℤ) ((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a)) : Set ℝ)
Tactic: apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
a : ℝ
ha : a ≠ 0
⊢ IsDiscrete (↑(AddMonoidHom.range (G := ℤ) ((zmultiplesHom ℝ : (a : ℝ) → ℤ →+ ℝ) a)) : Set ℝ)
have rw : DiscreteTopology ↥(AddSubgroup.zmultiples a)
Tactic: rw [AddSubgroup.range_zmultiplesHom, SetLike.isDiscrete_iff_discreteTopology]
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
a : ℝ
⊢ Tendsto (α := ↥(zmultiples a)) (⇑(AddSubgroup.subtype (zmultiples a)) : (a : ↥(zmultiples a)) → ℝ) Filter.cofinite
    (cocompact ℝ)
have refine : IsDiscrete (↑(zmultiples a) : Set ℝ)
Tactic: refine (zmultiples a).tendsto_coe_cofinite_of_discrete ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ZMultiples (goal)
Goal:
a : ℝ
⊢ IsDiscrete (↑(zmultiples a) : Set ℝ)
have rw : DiscreteTopology ↥(zmultiples a)
Tactic: rw [SetLike.isDiscrete_iff_discreteTopology]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ (closure[inst] s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
have rw : (s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
  (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Tactic: rw [closure_inter_open_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ (s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
have rw : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
  (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Tactic: rw [closure_inter_open_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
have rw : IsOpen[inst] (u ∩ v)
Tactic: rw [closure_inter_open_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
⊢ (closure[inst] s ∩ u).Nonempty → (closure[inst] s ∩ v).Nonempty → (closure[inst] s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
have iterate : IsOpen[inst] (u ∩ v)
Tactic: iterate 3 rw [closure_inter_open_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ IsClosed[inst] s
have rw : s = closure[inst] s
Tactic: rw [← closure_eq_iff_isClosed, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
⊢ irreducibleComponents X = {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s}
have h : ∀ (s : Set X),
  s ∈ irreducibleComponents X ↔
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
⊢ s ∈ irreducibleComponents X ↔
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
have h : s ∈ irreducibleComponents X →
  Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
h :
  s ∈ irreducibleComponents X →
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
⊢ s ∈ irreducibleComponents X ↔
    Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
have h₁ : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s →
  s ∈ irreducibleComponents X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
⊢ s ∈ irreducibleComponents X
have h : ∀ (x : Set X) (h : IsIrreducible x) (e : s ≤ x), x ≤ s
Tactic: refine ⟨H.1.2, fun x h e => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
s : Set X
H : Membership.mem (γ := Set (Set X)) {s : Set X | Maximal (fun (x : Set X) ↦ IsClosed[inst] x ∧ IsIrreducible x) s} s
x : Set X
h : IsIrreducible x
e : s ≤ x
⊢ x ≤ s
have this : closure[inst] x ≤ s
Tactic: have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
⊢ ∃ u ∈ irreducibleComponents X, s ⊆ u
have obtain : ∀ (u : Set X) (hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u),
  ∃ u ∈ irreducibleComponents X, s ⊆ u
Tactic: obtain ⟨u, hu⟩ := exists_preirreducible s hs.isPreirreducible
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsIrreducible s
u : Set X
hu : IsPreirreducible u ∧ s ⊆ u ∧ ∀ (u_1 : Set X), IsPreirreducible u_1 → u ⊆ u_1 → u_1 = u
⊢ ∃ u ∈ irreducibleComponents X, s ⊆ u
have right : s ⊆ u
Tactic: use u, ⟨⟨hs.left.mono hu.right.left,hu.left⟩,fun _ h hl => (hu.right.right _ h.right hl).le⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : f x ∈ u
y : X
hy : y ∈ s
hyv : f y ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rw : ∀ (hxu : x ∈ f ⁻¹' u) (y : X) (hy : y ∈ s) (hyv : y ∈ f ⁻¹' v), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rw [← mem_preimage] at hxu hyv
Cleared hypotheses: hxu, y, hy, hyv
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (u' : Set X) (hu' : IsOpen[inst] u') (u'_eq : f ⁻¹' u ∩ s = u' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (v' : Set X) (hv' : IsOpen[inst] v') (v'_eq : f ⁻¹' v ∩ s = v' ∩ s), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have this : (s ∩ u').Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
Tactic: have := H u' v' hu' hv'
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (s ∩ u').Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have this₁ : (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
Tactic: rw [inter_comm s u', ← u'_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Irreducible (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (s ∩ v').Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have this₁ : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
Tactic: rw [inter_comm s v', ← v'_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x : X
hx : x ∈ s
hxu : x ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have rcases : ∀ (x : X) (hxs : x ∈ s) (hxu' : x ∈ u') (hxv' : x ∈ v'), (f '' s ∩ (u ∩ v)).Nonempty
Tactic: rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have refine_1 : f x ∈ u
Tactic: refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
refine_1 : f x ∈ u
⊢ (f '' s ∩ (u ∩ v)).Nonempty
have refine_2 : f x ∈ v
Tactic: refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ f x ∈ u
have refine_1 : x ∈ f ⁻¹' u
Tactic: rw [← mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.Irreducible (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst_1] u
hv : IsOpen[inst_1] v
x_1 : X
hx : x_1 ∈ s
hxu : x_1 ∈ f ⁻¹' u
y : X
hy : y ∈ s
hyv : y ∈ f ⁻¹' v
u' : Set X
hu' : IsOpen[inst] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set X
hv' : IsOpen[inst] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
this : (f ⁻¹' u ∩ s).Nonempty → (f ⁻¹' v ∩ s).Nonempty → (s ∩ (u' ∩ v')).Nonempty
x : X
hxs : x ∈ s
hxu' : x ∈ u'
hxv' : x ∈ v'
⊢ x ∈ f ⁻¹' u
have refine_1 : x ∈ f ⁻¹' u ∩ s
Tactic: apply mem_of_mem_inter_left