awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s
have hf₁ : ContinuousOn f (s ∩ {a : α | p a})
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
hpf : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a : α | p a}, Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf₁ : ContinuousOn f (s ∩ {a : α | p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) s
have hg₁ : ContinuousOn g (s ∩ {a : α | ¬p a})
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
have hpf : Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (f a))
Tactic: simp only [← hp a ha, ite_self]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (f a))
have hpf : Tendsto f (𝓝[s ∩ closure[inst] {a : α | p a}] a) (𝓝 (f a))
Tactic: apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
have hpg : Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (g a))
Tactic: simp only [hp a ha, ite_self]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (g a))
have hpg : Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
Tactic: apply tendsto_nhdsWithin_mono_left (inter_subset_inter_right s subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
⊢ Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
have has : a ∈ s
Tactic: rcases ha with ⟨has, ⟨_, ha⟩⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
has : a ∈ s
⊢ Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
have left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
Tactic: rcases ha with ⟨has, ⟨_, ha⟩⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
ha : a ∈ s ∩ frontier {a : α | p a}
has : a ∈ s
left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
⊢ Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
have ha₁ : a ∉ interior {a : α | p a}
Tactic: rcases ha with ⟨has, ⟨_, ha⟩⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Piecewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ a ∈ s ∩ frontier {a : α | p a}, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] {a : α | p a})
hg : ContinuousOn g (s ∩ closure[inst] {a : α | ¬p a})
a : α
has : a ∈ s
left : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}) a
ha : a ∉ interior {a : α | p a}
⊢ Tendsto g (𝓝[s ∩ closure[inst] {a : α | ¬p a}] a) (𝓝 (g a))
have ha₁ : Membership.mem (γ := Set α) (closure[inst] {a : α | p a}ᶜ) a
Tactic: rw [← mem_compl_iff, ← closure_compl] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hpf :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto f (𝓝[{x : α | p x}] a) (𝓝 (if p a then f a else g a))
hpg :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x : α | p x}
hg : ContinuousOn g {x : α | ¬p x}
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p a then f a else g a
have rw : ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hpf :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto f (𝓝[{x : α | p x}] a) (𝓝 (if p a then f a else g a))
hpg :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x : α | p x}
hg : ContinuousOn g {x : α | ¬p x}
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hpf₁ : ∀ (a : α),
  Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
    Tendsto f (𝓝[univ ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hpf :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto f (𝓝[{x : α | p x}] a) (𝓝 (if p a then f a else g a))
hpg :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x : α | p x}
hg : ContinuousOn g {x : α | ¬p x}
hpf₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
      Tendsto f (𝓝[univ ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hpg₁ : ∀ (a : α),
  Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
    Tendsto g (𝓝[univ ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hpf :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto f (𝓝[{x : α | p x}] a) (𝓝 (if p a then f a else g a))
hpg :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x : α | p x}
hg : ContinuousOn g {x : α | ¬p x}
hpf₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
      Tendsto f (𝓝[univ ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
      Tendsto g (𝓝[univ ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hf₁ : ContinuousOn f (univ ∩ {a : α | p a})
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hpf :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto f (𝓝[{x : α | p x}] a) (𝓝 (if p a then f a else g a))
hpg :
  ∀ (a : α),
    Membership.mem (γ := Set α) (frontier {x : α | p x}) a →
      Tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f {x : α | p x}
hg : ContinuousOn g {x : α | ¬p x}
hpf₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
      Tendsto f (𝓝[univ ∩ {a : α | p a}] a) (𝓝 (if p a then f a else g a))
hpg₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a →
      Tendsto g (𝓝[univ ∩ {a : α | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf₁ : ContinuousOn f (univ ∩ {a : α | p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hg₁ : ContinuousOn g (univ ∩ {a : α | ¬p a})
Tactic: apply ContinuousOn.if'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ (a : α), Membership.mem (γ := Set α) (frontier {x : α | p x}) a → f a = g a
hf : ContinuousOn f (closure[inst] {x : α | p x})
hg : ContinuousOn g (closure[inst] {x : α | ¬p x})
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p a then f a else g a
have rw : ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ (a : α), Membership.mem (γ := Set α) (frontier {x : α | p x}) a → f a = g a
hf : ContinuousOn f (closure[inst] {x : α | p x})
hg : ContinuousOn g (closure[inst] {x : α | ¬p x})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hp₁ : ∀ (a : α), Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a → f a = g a
Tactic: apply ContinuousOn.if
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ (a : α), Membership.mem (γ := Set α) (frontier {x : α | p x}) a → f a = g a
hf : ContinuousOn f (closure[inst] {x : α | p x})
hg : ContinuousOn g (closure[inst] {x : α | ¬p x})
hp₁ : ∀ (a : α), Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a → f a = g a
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hf₁ : ContinuousOn f (univ ∩ closure[inst] {a : α | p a})
Tactic: apply ContinuousOn.if
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : α → Prop
inst_2 : (a : α) → Decidable (p a)
hp : ∀ (a : α), Membership.mem (γ := Set α) (frontier {x : α | p x}) a → f a = g a
hf : ContinuousOn f (closure[inst] {x : α | p x})
hg : ContinuousOn g (closure[inst] {x : α | ¬p x})
hp₁ : ∀ (a : α), Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a → f a = g a
hf₁ : ContinuousOn f (univ ∩ closure[inst] {a : α | p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
have hg₁ : ContinuousOn g (univ ∩ closure[inst] {a : α | ¬p a})
Tactic: apply ContinuousOn.if
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst] s
hs' : IsOpen[inst] s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
⊢ IsOpen[inst] (t.ite s s')
have simp : ∀ (hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s) (hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'),
  Continuous[inst, _] fun (x : α) ↦ x ∈ s ∩ t ∪ s' \ t
Tactic: simp only [isOpen_iff_continuous_mem, Set.ite] at *
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s
hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'
⊢ Continuous[inst, _] fun (x : α) ↦ x ∈ s ∩ t ∪ s' \ t
have h : ∀ (x : α), x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
Tactic: convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s
hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
have pos : ∀ (hx : x ∈ t), x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s
hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'
x : α
pos :
  ∀ (hx : x ∈ t), x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
have neg : ∀ (hx : x ∉ t), x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst] s
hs' : IsOpen[inst] s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
⊢ IsOpen[inst] (t.ite s s')
have simp : ∀ (hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s) (hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'),
  Continuous[inst, _] fun (x : α) ↦ x ∈ s ∩ t ∪ s' \ t
Tactic: classical
    simp only [isOpen_iff_continuous_mem, Set.ite] at *
    convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
    rename_i x
    by_cases hx : x ∈ t <;> simp [hx]
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst] s
hs' : IsOpen[inst] s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
simp :
  ∀ (hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s) (hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s'),
    Continuous[inst, _] fun (x : α) ↦ x ∈ s ∩ t ∪ s' \ t
⊢ IsOpen[inst] (t.ite s s')
have h : ∀ (hs : Continuous[inst, _] fun (x : α) ↦ x ∈ s) (hs' : Continuous[inst, _] fun (x : α) ↦ x ∈ s') (x : α),
  x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
Tactic: classical
    simp only [isOpen_iff_continuous_mem, Set.ite] at *
    convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
    rename_i x
    by_cases hx : x ∈ t <;> simp [hx]
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] t
have rw : t.ite s s' ∩ (t ∪ frontier t) = s ∩ (t ∪ frontier t)
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rw : t.ite s s' ∩ (t ∪ frontier t) = s ∩ (t ∪ frontier t)
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] t
have rw₁ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ (t ∪ frontier t)
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rw : t.ite s s' ∩ (t ∪ frontier t) = s ∩ (t ∪ frontier t)
rw₁ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ (t ∪ frontier t)
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] t
have rw₂ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rw : t.ite s s' ∩ (t ∪ frontier t) = s ∩ (t ∪ frontier t)
rw₁ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ (t ∪ frontier t)
rw₂ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] t
have rw₃ : s ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rw : t.ite s s' ∩ (t ∪ frontier t) = s ∩ (t ∪ frontier t)
rw₁ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ (t ∪ frontier t)
rw₂ : t.ite s s' ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
rw₃ : s ∩ t ∪ t.ite s s' ∩ frontier t = s ∩ t ∪ s ∩ frontier t
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] t
have rw₄ : s ∩ t ∪ s ∩ frontier t = s ∩ t ∪ s ∩ frontier t
Tactic: rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
    ite_inter_self, ite_inter_of_inter_eq _ ht]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ t.ite s s' ∩ closure[inst] tᶜ = s' ∩ closure[inst] tᶜ
have rw : s' ∩ frontier tᶜ = s ∩ frontier tᶜ
Tactic: rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ
have rwa : s' ∩ frontier t = s ∩ frontier t
Tactic: rwa [frontier_compl, eq_comm]
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s' t : Set α
inst_2 : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst] t)
h' : ContinuousOn g (s' ∩ closure[inst] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) (t.ite s s')
have ht : ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a
Tactic: apply ContinuousOn.piecewise
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s' t : Set α
inst_2 : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst] t)
h' : ContinuousOn g (s' ∩ closure[inst] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
ht : ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) (t.ite s s')
have hf : ContinuousOn f (t.ite s s' ∩ closure[inst] t)
Tactic: apply ContinuousOn.piecewise
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s' t : Set α
inst_2 : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst] t)
h' : ContinuousOn g (s' ∩ closure[inst] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
ht : ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a
hf : ContinuousOn f (t.ite s s' ∩ closure[inst] t)
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) (t.ite s s')
have hg : ContinuousOn g (t.ite s s' ∩ closure[inst] tᶜ)
Tactic: apply ContinuousOn.piecewise
-- Lean 4 proof step from Mathlib.Topology.Piecewise (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s s' t : Set α
inst_2 : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure[inst] t)
h' : ContinuousOn g (s' ∩ closure[inst] tᶜ)
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f g (s ∩ frontier t)
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a
have ht : ∀ a ∈ s ∩ frontier t, f a = g a
Tactic: rwa [ite_inter_of_inter_eq _ H]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ IsQuasiSeparated.{u_3} (α := α) univ ↔ QuasiSeparatedSpace α
have rw : IsQuasiSeparated.{u_3} (α := α) univ ↔
  ∀ (U V : Set α), IsOpen[inst] U → IsCompact U → IsOpen[inst] V → IsCompact V → IsCompact (U ∩ V)
Tactic: rw [quasiSeparatedSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.QuasiSeparated (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst_1] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst_1] V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
have h₁ : U ∩ V = f '' (f ⁻¹' U ∩ f ⁻¹' V)
Tactic: convert!
    (H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous