awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)
have rw : TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
  sSup (TopologicalSpace.coinduced f '' s)
Tactic: rw [sSup_eq_iSup', sSup_image', coinduced_iSup]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sSup (TopologicalSpace.coinduced f '' s)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)
have rw₁ : TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
  ⨆ (a : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑a : TopologicalSpace α)
Tactic: rw [sSup_eq_iSup', sSup_image', coinduced_iSup]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set (TopologicalSpace α)
rw :
  TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    sSup (TopologicalSpace.coinduced f '' s)
rw₁ :
  TopologicalSpace.coinduced f (⨆ (a : (↑s : Type u_1)), (↑a : TopologicalSpace α)) =
    ⨆ (a : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑a : TopologicalSpace α)
⊢ TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)
have rw₂ : Eq.{u_2 + 1} (α := TopologicalSpace β) (⨆ (i : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑i : TopologicalSpace α))
  (⨆ (a : (↑s : Type u_1)), TopologicalSpace.coinduced f (↑a : TopologicalSpace α))
Tactic: rw [sSup_eq_iSup', sSup_image', coinduced_iSup]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
⊢ Eq (α := (t : TopologicalSpace α) → TopologicalSpace β) (TopologicalSpace.induced (⇑e.symm : (a : β) → α))
    (TopologicalSpace.coinduced (⇑e : (a : α) → β))
have h : ∀ (t : TopologicalSpace α) (U : Set β),
  IsOpen[TopologicalSpace.induced (⇑e.symm : (a : β) → α) t] U ↔
    IsOpen[TopologicalSpace.coinduced (⇑e : (a : α) → β) t] U
Tactic: ext t U
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_4
β : Type u_5
e : α ≃ β
t : TopologicalSpace α
U : Set β
⊢ IsOpen[TopologicalSpace.induced (⇑e.symm : (a : β) → α) t] U ↔
    IsOpen[TopologicalSpace.coinduced (⇑e : (a : α) → β) t] U
have h : (∃ (t_1 : Set α), IsOpen[t] t_1 ∧ (⇑e.symm : (a : β) → α) ⁻¹' t_1 = U) ↔ IsOpen[t] ((⇑e : (a : α) → β) ⁻¹' U)
Tactic: rw [isOpen_induced_iff, isOpen_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
inst : TopologicalSpace α
h : NontrivialTopology α
⊢ Nontrivial α
have contrapose! : ∀ (h : Subsingleton α), IndiscreteTopology α
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
⊢ Eq (α := TopologicalSpace (WithTopology α ⊤)) (WithTopology.instTopologicalSpace α ⊤) ⊤
have rw : Eq.{u + 1} (α := TopologicalSpace (WithTopology α ⊤)) (induced WithTopology.ofTopology ⊤) ⊤
Tactic: rw [WithTopology.topology_eq_induced, induced_top]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
rw : Eq.{u + 1} (α := TopologicalSpace (WithTopology α ⊤)) (induced WithTopology.ofTopology ⊤) ⊤
⊢ Eq (α := TopologicalSpace (WithTopology α ⊤)) (WithTopology.instTopologicalSpace α ⊤) ⊤
have rw₁ : Eq.{u + 1} (α := TopologicalSpace (WithTopology α ⊤)) ⊤ ⊤
Tactic: rw [WithTopology.topology_eq_induced, induced_top]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
⊢ NontrivialTopology.{u} (WithTopology α t) ↔ t ≠ ⊤
have simp_rw : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ ↔ t = ⊤
Tactic: simp_rw [nontrivialTopology_iff, topology_eq_induced, ne_eq, not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
⊢ Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ ↔ t = ⊤
have mp : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ → t = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
mp : Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ → t = ⊤
⊢ Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤ ↔ t = ⊤
have mpr : t = ⊤ → Eq (α := TopologicalSpace (WithTopology α t)) (induced ofTopology t) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)
have rw : t ≤ generateFrom (preimage f '' b)
Tactic: rw [induced_generateFrom_eq]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)
have h₁ : ∀ s ∈ preimage f '' b, IsOpen[t] s
Tactic: apply le_generateFrom
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom s
have refine : ∀ s_1 ∈ insert t s, IsOpen[generateFrom s] s_1
Tactic: refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
s : Set (Set α)
⊢ generateFrom (insert ∅ s) = generateFrom s
have rw : generateFrom (insert (⋃₀ ∅) s) = generateFrom s
Tactic: rw [← sUnion_empty]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun (t : TopologicalSpace α) ↦ 𝓝 a) t
have rw : nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f
Tactic: rw [le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f
have a₁ : 𝓝 a ≤ pure a ⊔ f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
x : TopologicalSpace α := nhdsAdjoint a f
a₁ : 𝓝 a ≤ pure a ⊔ f
⊢ 𝓝 a = pure a ⊔ f
have a₂ : pure a ⊔ f ≤ 𝓝 a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw₁ : (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
  𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₁ :
  (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
    𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw₂ : (𝓝 a ≤ pure a ⊔ f ∧ ∀ (x : α), x ≠ a → 𝓝 x ≤ pure x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw₁ : (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
  𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
simp_rw : (∀ (x : α), 𝓝 x ≤ 𝓝 x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
simp_rw₁ :
  (∀ (x : α), 𝓝 x ≤ update (β := fun (a : α) ↦ Filter α) pure a (pure a ⊔ f) x) ↔
    𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
have simp_rw₂ : (𝓝 a ≤ pure a ⊔ f ∧ ∀ (x : α), x ≠ a → 𝓝 x ≤ pure x) ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
Tactic: classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).ge_iff_eq']
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
a : α
⊢ 𝓝 a = ⊤
have refl : ∀ [IndiscreteTopology α], 𝓝 a = ⊤
Tactic: cases IndiscreteTopology.eq_top α
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
⊢ t = ⊤ ↔ ∀ (x y : α), Inseparable x y
have rw : t = ⊤ ↔ IndiscreteTopology α
Tactic: rw [← TopologicalSpace.indiscrete_iff_forall_inseparable, indiscreteTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
rw : t = ⊤ ↔ IndiscreteTopology α
⊢ t = ⊤ ↔ ∀ (x y : α), Inseparable x y
have rw₁ : t = ⊤ ↔ t = ⊤
Tactic: rw [← TopologicalSpace.indiscrete_iff_forall_inseparable, indiscreteTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
⊢ t ≠ ⊤ ↔ ∃ (x : α) (y : α), ¬Inseparable x y
have rw : t ≠ ⊤ ↔ NontrivialTopology α
Tactic: rw [← TopologicalSpace.nontrivial_iff_exists_not_inseparable, nontrivialTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
t : TopologicalSpace α
rw : t ≠ ⊤ ↔ NontrivialTopology α
⊢ t ≠ ⊤ ↔ ∃ (x : α) (y : α), ¬Inseparable x y
have rw₁ : t ≠ ⊤ ↔ t ≠ ⊤
Tactic: rw [← TopologicalSpace.nontrivial_iff_exists_not_inseparable, nontrivialTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)
have rw : b ⊆ {s : Set β | IsOpen[coinduced f t] s} ↔ ∀ s ∈ b, IsOpen[t] (f ⁻¹' s)
Tactic: rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
t₁ t₂ : TopologicalSpace α
t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₁
h₂ : Continuous[t₁, t₃] f
⊢ Continuous[t₂, t₃] f
have rw : ∀ (h₂ : t₁ ≤ induced f t₃), t₂ ≤ induced f t₃
Tactic: rw [continuous_iff_le_induced] at h₂ ⊢
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
t₂ t₃ : TopologicalSpace β
h₁ : t₂ ≤ t₃
h₂ : Continuous[t₁, t₂] f
⊢ Continuous[t₁, t₃] f
have rw : ∀ (h₂ : coinduced f t₁ ≤ t₂), coinduced f t₁ ≤ t₃
Tactic: rw [continuous_iff_coinduced_le] at h₂ ⊢
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s
have simp_rw : (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔
  ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
Tactic: simp_rw [mem_nhds_iff, isOpen_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
⊢ (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
have mp : (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) →
  ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
this : TopologicalSpace β := induced f T
mp :
  (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) →
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
⊢ (∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t) ↔
    ∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s
have mpr : (∃ (u : Set α), (∃ t ⊆ u, IsOpen[T] t ∧ f a ∈ t) ∧ f ⁻¹' u ⊆ s) →
  ∃ t ⊆ s, (∃ (t_1 : Set α), IsOpen[T] t_1 ∧ f ⁻¹' t_1 = t) ∧ a ∈ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
⊢ 𝓝 a = comap f (𝓝 (f a))
have h : ∀ (s : Set β), s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
have h : (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ s ∈ comap f (𝓝 (f a))
Tactic: rw [mem_nhds_induced, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
h : (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ s ∈ comap f (𝓝 (f a))
⊢ s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
have h₁ : (∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s) ↔ ∃ t ∈ 𝓝 (f a), f ⁻¹' t ⊆ s
Tactic: rw [mem_nhds_induced, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
⊢ map f (𝓝 a) = 𝓝 (f a)
have rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
Tactic: rw [nhds_induced, map_comap_of_surjective hf]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
hf : Surjective f
a : β
rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)
have rw₁ : 𝓝 (f a) = 𝓝 (f a)
Tactic: rw [nhds_induced, map_comap_of_surjective hf]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
f : α → β
a : α
l : Filter α
⊢ Continuous[nhdsAdjoint a l, inst] f ↔ Tendsto f l (𝓝 (f a))
have simp_rw : nhdsAdjoint a l ≤ induced f inst ↔ Tendsto f l (𝓝 (f a))
Tactic: simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
f : α → β
a : α
l : Filter α
simp_rw : nhdsAdjoint a l ≤ induced f inst ↔ Tendsto f l (𝓝 (f a))
⊢ Continuous[nhdsAdjoint a l, inst] f ↔ Tendsto f l (𝓝 (f a))
have simp_rw₁ : l ≤ 𝓝 a ↔ Tendsto f l (𝓝 (f a))
Tactic: simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
f : α → β
a : α
l : Filter α
simp_rw : nhdsAdjoint a l ≤ induced f inst ↔ Tendsto f l (𝓝 (f a))
simp_rw₁ : l ≤ 𝓝 a ↔ Tendsto f l (𝓝 (f a))
⊢ Continuous[nhdsAdjoint a l, inst] f ↔ Tendsto f l (𝓝 (f a))
have simp_rw₂ : l ≤ comap f (𝓝 (f a)) ↔ Tendsto f l (𝓝 (f a))
Tactic: simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x : TopologicalSpace β
⊢ coinduced f (nhdsAdjoint a l) ≤ x ↔ nhdsAdjoint (f a) (map f l) ≤ x
have rw : coinduced f (nhdsAdjoint a l) ≤ x ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
Tactic: rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x : TopologicalSpace β
rw : coinduced f (nhdsAdjoint a l) ≤ x ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
⊢ coinduced f (nhdsAdjoint a l) ≤ x ↔ nhdsAdjoint (f a) (map f l) ≤ x
have rw₁ : Continuous[nhdsAdjoint a l, x] f ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
Tactic: rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x : TopologicalSpace β
rw : coinduced f (nhdsAdjoint a l) ≤ x ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₁ : Continuous[nhdsAdjoint a l, x] f ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
⊢ coinduced f (nhdsAdjoint a l) ≤ x ↔ nhdsAdjoint (f a) (map f l) ≤ x
have rw₂ : Tendsto f l (𝓝 (f a)) ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
Tactic: rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : Filter α
x : TopologicalSpace β
rw : coinduced f (nhdsAdjoint a l) ≤ x ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₁ : Continuous[nhdsAdjoint a l, x] f ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
rw₂ : Tendsto f l (𝓝 (f a)) ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
⊢ coinduced f (nhdsAdjoint a l) ≤ x ↔ nhdsAdjoint (f a) (map f l) ≤ x
have rw₃ : map f l ≤ 𝓝 (f a) ↔ map f l ≤ (fun (t : TopologicalSpace β) ↦ 𝓝 (f a)) x
Tactic: rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set β
h : IsClosed[t] s
⊢ IsClosed[induced f t] (f ⁻¹' s)
have simp_rw : IsOpen[induced f t] (f ⁻¹' s)ᶜ
Tactic: simp_rw [← isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a
have rw : map f (comap f (𝓝 (f a))) = 𝓝[range f] f a
Tactic: rw [nhds_induced, Filter.map_comap, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
rw : map f (comap f (𝓝 (f a))) = 𝓝[range f] f a
⊢ map f (𝓝 a) = 𝓝[range f] f a
have rw₁ : 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝[range f] f a
Tactic: rw [nhds_induced, Filter.map_comap, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
rw : map f (comap f (𝓝 (f a))) = 𝓝[range f] f a
rw₁ : 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝[range f] f a
⊢ map f (𝓝 a) = 𝓝[range f] f a
have rw₂ : 𝓝 (f a) ⊓ 𝓟 (range f) = 𝓝 (f a) ⊓ 𝓟 (range f)
Tactic: rw [nhds_induced, Filter.map_comap, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)
have rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
Tactic: rw [nhds_induced, Filter.map_comap_of_mem h]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
h : range f ∈ 𝓝 (f a)
rw : map f (comap f (𝓝 (f a))) = 𝓝 (f a)
⊢ map f (𝓝 a) = 𝓝 (f a)
have rw₁ : 𝓝 (f a) = 𝓝 (f a)
Tactic: rw [nhds_induced, Filter.map_comap_of_mem h]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
have pos : q → (Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x)
Tactic: by_cases q
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
l : Filter α
p : α → Prop
q : Prop
pos : q → (Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x)
⊢ Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
have neg : ¬q → (Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x)
Tactic: by_cases q
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
p : α → Prop
⊢ Continuous[inst, _] p ↔ IsOpen[inst] {x : α | p x}
have simp : (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ (x : α), Membership.mem (γ := Set α) {x : α | p x} x → {x : α | p x} ∈ 𝓝 x
Tactic: simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l
have rw : (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l
Tactic: rw [rtendsto'_def]
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
r : SetRel Y X
l : Filter Y
x : X
⊢ (∀ s ∈ 𝓝 x, r.preimage s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → r.preimage s ∈ l
have hf : ∀ (s t : Set X), s ⊆ t → r.preimage s ⊆ r.preimage t
Tactic: apply all_mem_nhds_filter
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
⊢ IsOpen[inst] f.Dom
have rw : IsOpen[inst] (f.preimage Set.univ)
Tactic: rw [← PFun.preimage_univ]
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
⊢ PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
have mp : PContinuous f → ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
mp : PContinuous f → ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
⊢ PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
have mpr : (∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
⊢ PTendsto' f (𝓝 x) (𝓝 y)
have mp : ∀ (s : Set Y), (∃ t ⊆ s, IsOpen[inst_1] t ∧ y ∈ t) → ∃ t ⊆ f.preimage s, IsOpen[inst] t ∧ x ∈ t
Tactic: simp only [ptendsto'_def, mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
⊢ IsOpen[inst] (f.preimage s)
have mpr : ∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)
Tactic: rw [isOpen_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Partial (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst_1] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s ⊆ t
⊢ t ∈ 𝓝 x
have mpr : f.preimage s ∈ 𝓝 x
Tactic: grw [← h]
-- Lean 4 proof step from Mathlib.Topology.Partial (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s_1 : Set Y
os : IsOpen[inst_1] s_1
x : X
y : Y
ys : y ∈ s_1
fxy : (x, y) ∈ f.graph'
t : Set X
h : f.preimage s_1 ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
⊢ f.preimage s ∈ 𝓝 x
have this : PTendsto' f (𝓝 x) (𝓝 y)
Tactic: have : PTendsto' f (𝓝 x) (𝓝 y) := hf fxy