awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Piecewise
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})
⊢ ContinuousOn f (s ∩ {a : α | p a})

Tactic:
hf.mono (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, subset_closure, ContinuousOn.mono
-- Module: Mathlib.Topology.Piecewise
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})
⊢ ContinuousOn f (s ∩ {a : α | p a})

Tactic:
exact hf.mono (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, subset_closure, ContinuousOn.mono
-- Module: Mathlib.Topology.Piecewise
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})
⊢ ContinuousOn g (s ∩ {a : α | ¬p a})

Tactic:
hg.mono (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, subset_closure, ContinuousOn.mono
-- Module: Mathlib.Topology.Piecewise
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})
⊢ ContinuousOn g (s ∩ {a : α | ¬p a})

Tactic:
exact hg.mono (inter_subset_inter_right s subset_closure)

Premises used: Set.inter_subset_inter_right, subset_closure, ContinuousOn.mono
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s t : Set α
inst_2 : (a : α) → Decidable (a ∈ t)
ht : ∀ a ∈ s ∩ frontier t, f a = g a
hf : ContinuousOn f (s ∩ closure[inst] t)
hg : ContinuousOn g (s ∩ closure[inst] tᶜ)
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) s

Tactic:
hf.if ht hg

Premises used: Set.piecewise, ContinuousOn.if
-- Module: Mathlib.Topology.Piecewise
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}
rw : ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p a then f a else g a

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.Piecewise
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})
hg₁ : ContinuousOn g (univ ∩ {a : α | ¬p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ

Tactic:
apply ContinuousOn.if'

Premises used: ContinuousOn.if'
-- Module: Mathlib.Topology.Piecewise
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}
⊢ ∀ (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:
simpa
-- Module: Mathlib.Topology.Piecewise
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}
⊢ ∀ (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:
simpa
-- Module: Mathlib.Topology.Piecewise
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 f (univ ∩ {a : α | p a})

Tactic:
simpa
-- Module: Mathlib.Topology.Piecewise
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 g (univ ∩ {a : α | ¬p a})

Tactic:
simpa
-- Module: Mathlib.Topology.Piecewise
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})
rw : ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p a then f a else g a

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Topology.Piecewise
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})
hg₁ : ContinuousOn g (univ ∩ closure[inst] {a : α | ¬p a})
⊢ ContinuousOn.{u_1, u_2} (Y := β) (fun (a : α) ↦ if p a then f a else g a) univ

Tactic:
apply ContinuousOn.if

Premises used: ContinuousOn.if
-- Module: Mathlib.Topology.Piecewise
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})
⊢ ∀ (a : α), Membership.mem (γ := Set α) (univ ∩ frontier {a : α | p a}) a → f a = g a

Tactic:
simpa
-- Module: Mathlib.Topology.Piecewise
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 f (univ ∩ closure[inst] {a : α | p a})

Tactic:
simpa
-- Module: Mathlib.Topology.Piecewise
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 g (univ ∩ closure[inst] {a : α | ¬p a})

Tactic:
simpa
-- Module: Mathlib.Topology.Piecewise
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 : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p a then f a else g a

Tactic:
continuous_if hp hf.continuousOn hg.continuousOn

Premises used: Continuous.continuousOn, continuous_if
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : Prop
inst_2 : Decidable p
hf : p → Continuous[inst, inst_1] f
hg : ¬p → Continuous[inst, inst_1] g
pos : ∀ (h : p), Continuous[inst, inst_1] fun (a : α) ↦ f a
neg : ∀ (h : ¬p), Continuous[inst, inst_1] fun (a : α) ↦ g a
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p then f a else g a

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : Prop
inst_2 : Decidable p
hf : p → Continuous[inst, inst_1] f
hg : ¬p → Continuous[inst, inst_1] g
h : p
⊢ Continuous[inst, inst_1] fun (a : α) ↦ f a

Tactic:
hf h
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : Prop
inst_2 : Decidable p
hf : p → Continuous[inst, inst_1] f
hg : ¬p → Continuous[inst, inst_1] g
h : ¬p
⊢ Continuous[inst, inst_1] fun (a : α) ↦ g a

Tactic:
hg h
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : Prop
inst_2 : Decidable p
hf : p → Continuous[inst, inst_1] f
hg : ¬p → Continuous[inst, inst_1] g
h : p
⊢ Continuous[inst, inst_1] fun (a : α) ↦ f a

Tactic:
exacts [hf h, hg h]
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
p : Prop
inst_2 : Decidable p
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ Continuous[inst, inst_1] fun (a : α) ↦ if p then f a else g a

Tactic:
continuous_if_const p (fun _ => hf) fun _ => hg

Premises used: continuous_if_const
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
inst_2 : (a : α) → Decidable (a ∈ s)
hs : ∀ a ∈ frontier s, f a = g a
hf : ContinuousOn f (closure[inst] s)
hg : ContinuousOn g (closure[inst] sᶜ)
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
continuous_if hs hf hg

Premises used: continuous_if, Set.piecewise
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : α → β
s : Set α
inst_2 : (a : α) → Decidable (a ∈ s)
hs : ∀ a ∈ frontier s, f a = g a
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
hf.if hs hg

Premises used: Continuous.if, Set.piecewise
-- Module: Mathlib.Topology.Piecewise
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')

Tactic:
simp only [isOpen_iff_continuous_mem, Set.ite] at *

Premises used: isOpen_iff_continuous_mem, Set.ite
-- Module: Mathlib.Topology.Piecewise
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, _] (t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s'))

Tactic:
continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn

Premises used: Continuous.continuousOn, propext, continuous_piecewise
-- Module: Mathlib.Topology.Piecewise
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'
h : ∀ (x : α), x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x
⊢ Continuous[inst, _] fun (x : α) ↦ x ∈ s ∩ t ∪ s' \ t

Tactic:
convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2

Premises used: Continuous.continuousOn, propext, continuous_piecewise
-- Module: Mathlib.Topology.Piecewise
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
neg :
  ∀ (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

Tactic:
by_cases hx : x ∈ t
-- Module: Mathlib.Topology.Piecewise
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 : α
hx : x ∈ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Piecewise
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 : α
hx : x ∉ t
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (β := fun (a : α) ↦ Prop) (Membership.mem s) (Membership.mem s') x

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Piecewise
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
h 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
⊢ IsOpen[inst] (t.ite s s')

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]

Premises used: isOpen_iff_continuous_mem, Set.ite
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst] s
hs' : IsOpen[inst] s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'

Tactic:
simpa [hx] using Set.ext_iff.1 ht x

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Topology.Piecewise
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
rw₄ rw₅ : s ∩ t ∪ s ∩ frontier t = s ∩ t ∪ s ∩ frontier t
⊢ t.ite s s' ∩ closure[inst] t = s ∩ closure[inst] 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]

Premises used: closure_eq_self_union_frontier, Set.ite_inter_of_inter_eq, Set.inter_union_distrib_left, Set.ite_inter_self
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rw : s' ∩ frontier tᶜ = s ∩ frontier tᶜ
⊢ t.ite s s' ∩ closure[inst] tᶜ = s' ∩ closure[inst] tᶜ

Tactic:
rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq]

Premises used: Set.ite_compl, ite_inter_closure_eq_of_inter_frontier_eq
-- Module: Mathlib.Topology.Piecewise
Goal:
α : Type u_1
inst : TopologicalSpace α
s s' t : Set α
ht : s ∩ frontier t = s' ∩ frontier t
rwa : s' ∩ frontier t = s ∩ frontier t
rwa₁ rwa₂ rwa₃ rwa₄ : s ∩ frontier t = s' ∩ frontier t
⊢ s' ∩ frontier tᶜ = s ∩ frontier tᶜ

Tactic:
rwa [frontier_compl, eq_comm]

Premises used: frontier_compl, eq_comm
-- Module: Mathlib.Topology.Piecewise
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)
hg : ContinuousOn g (t.ite s s' ∩ closure[inst] tᶜ)
⊢ ContinuousOn (t.piecewise (β := fun (a : α) ↦ β) f g) (t.ite s s')

Tactic:
apply ContinuousOn.piecewise

Premises used: ContinuousOn.piecewise
-- Module: Mathlib.Topology.Piecewise
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 ht₁ ht₂ ht₃ : ∀ a ∈ s ∩ frontier t, f a = g a
⊢ ∀ a ∈ t.ite s s' ∩ frontier t, f a = g a

Tactic:
rwa [ite_inter_of_inter_eq _ H]

Premises used: Set.ite_inter_of_inter_eq
-- Module: Mathlib.Topology.Piecewise
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)
hf hf₁ hf₂ hf₃ : ContinuousOn f (s ∩ closure[inst] t)
⊢ ContinuousOn f (t.ite s s' ∩ closure[inst] t)

Tactic:
rwa [ite_inter_closure_eq_of_inter_frontier_eq H]

Premises used: ite_inter_closure_eq_of_inter_frontier_eq
-- Module: Mathlib.Topology.Piecewise
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)
hg hg₁ hg₂ hg₃ : ContinuousOn g (s' ∩ closure[inst] tᶜ)
⊢ ContinuousOn g (t.ite s s' ∩ closure[inst] tᶜ)

Tactic:
rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]

Premises used: ite_inter_closure_compl_eq_of_inter_frontier_eq
-- Module: Mathlib.Topology.Piecewise
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
h' : ContinuousOn g s'
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')

Tactic:
continuousOn_piecewise_ite' (h.mono inter_subset_left) (h'.mono inter_subset_left) H Heq

Premises used: continuousOn_piecewise_ite', Set.inter_subset_left, ContinuousOn.mono
-- Module: Mathlib.Topology.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (i : α) → TopologicalSpace (X i)
a : α
⊢ Continuous (X := (a : α) → X a) (Y := (a_1 : (↑(Set.Iic a) : Type u_1)) → X (↑a_1 : α)) (restrictLe (π := X) a)

Tactic:
Pi.continuous_restrict _

Premises used: Pi.continuous_restrict, Preorder.restrictLe
-- Module: Mathlib.Topology.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (i : α) → TopologicalSpace (X i)
a b : α
hab : a ≤ b
⊢ Continuous (X := (a : (↑(Set.Iic b) : Type u_1)) → X (↑a : α)) (restrictLe₂ (π := X) hab)

Tactic:
Pi.continuous_restrict₂ _

Premises used: Preorder.restrictLe₂, Pi.continuous_restrict₂
-- Module: Mathlib.Topology.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (i : α) → TopologicalSpace (X i)
inst_2 : LocallyFiniteOrderBot α
a : α
⊢ Continuous (X := (i : α) → X i) (Y := (i : ↥(Finset.Iic a)) → X (↑i : α)) (frestrictLe (π := X) a)

Tactic:
Finset.continuous_restrict _

Premises used: Finset.continuous_restrict, Preorder.frestrictLe
-- Module: Mathlib.Topology.PreorderRestrict
Goal:
α : Type u_1
inst : Preorder α
X : α → Type u_2
inst_1 : (i : α) → TopologicalSpace (X i)
inst_2 : LocallyFiniteOrderBot α
a b : α
hab : a ≤ b
⊢ Continuous (X := (i : ↥(Finset.Iic b)) → X (↑i : α)) (frestrictLe₂ (π := X) hab)

Tactic:
Finset.continuous_restrict₂ _

Premises used: Finset.continuous_restrict₂, Preorder.frestrictLe₂
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_3
inst : TopologicalSpace α
rw :
  IsQuasiSeparated.{u_3} (α := α) univ ↔
    ∀ (U V : Set α), IsOpen[inst] U → IsCompact U → IsOpen[inst] V → IsCompact V → IsCompact (U ∩ V)
⊢ IsQuasiSeparated.{u_3} (α := α) univ ↔ QuasiSeparatedSpace α

Tactic:
rw [quasiSeparatedSpace_iff]

Premises used: quasiSeparatedSpace_iff
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ IsQuasiSeparated.{u_3} (α := α) univ ↔
    ∀ (U V : Set α), IsOpen[inst] U → IsCompact U → IsOpen[inst] V → IsCompact V → IsCompact (U ∩ V)

Tactic:
simp [IsQuasiSeparated]

Premises used: IsQuasiSeparated
-- Module: Mathlib.Topology.QuasiSeparated
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : QuasiSeparatedSpace α
⊢ IsQuasiSeparated.{u_3} (α := α) univ

Tactic:
isQuasiSeparated_univ_iff.mpr inferInstance

Premises used: Iff.mpr, isQuasiSeparated_univ_iff, inferInstance
-- Module: Mathlib.Topology.QuasiSeparated
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 (f '' (f ⁻¹' U ∩ f ⁻¹' V))

Tactic:
(H (f ⁻¹' U) (f ⁻¹' V) ?_ (h.continuous.1 _ hU') ?_ ?_ (h.continuous.1 _ hV') ?_).image
      h.continuous

Premises used: Set.preimage, IsCompact.image, Continuous.isOpen_preimage, Topology.IsEmbedding.continuous