awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (hx : x ∈ V),
    Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
      ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have neg : ∀ (hx : x ∉ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ + D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h + D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
a : X
⊢ Membership.mem (γ := Set X)
      (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
        restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯)
      a →
    a ∈ (↑(h.toFinset (s := F.support (U := U))) : Set X)
have contrapose : a ∉ (↑(h.toFinset (s := F.support (U := U))) : Set X) →
  a ∉
    Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) sorry
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
⊢ ∑ᶠ (x : X), restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯ = F
have this : (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
    restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) sorry) ⊆
  (↑(h.toFinset (s := F.support (U := U))) : Set X)
Tactic: have : (fun x ↦ (single x (F x)).restrict (subset_univ U)).support ⊆ h.toFinset := by
    intro
    contrapose
    aesop
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
⊢ ∑ᶠ (x : X), restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯ = F
have rw : ∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) sorry = F
Tactic: rw [finsum_eq_sum_of_support_subset _ this]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
⊢ ∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ = F
have h₁ : ∀ (z : X),
  Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) sorry :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
z : X
⊢ Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
have pos : ∀ (hz : z ∉ U),
  Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) sorry :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
Tactic: by_cases hz : z ∉ U
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
z : X
pos :
  ∀ (hz : z ∉ U),
    Eq.{u_2 + 1} (α := Y)
      ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ :
            (a : X) → Y)
          z :
        Y)
      ((F : (a : X) → Y) z : Y)
⊢ Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
have neg : ∀ (hz : ¬z ∉ U),
  Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) sorry :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
Tactic: by_cases hz : z ∉ U
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
z : X
hz : ¬z ∉ U
⊢ Eq.{u_2 + 1} (α := Y)
    ((∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ :
          (a : X) → Y)
        z :
      Y)
    ((F : (a : X) → Y) z : Y)
have neg : Eq.{u_2 + 1} (α := Y)
  (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
  ((F : (a : X) → Y) z : Y)
Tactic: simp [restrict_apply]
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
z : X
hz : ¬z ∉ U
⊢ Eq.{u_2 + 1} (α := Y)
    (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
    ((F : (a : X) → Y) z : Y)
have pos : ∀ (hz : z ∈ F.support (U := U)),
  Eq.{u_2 + 1} (α := Y)
    (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
    ((F : (a : X) → Y) z : Y)
Tactic: by_cases hz : z ∈ F.support
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : DecidableEq X
inst_2 : AddCommMonoid Y
U : Set X
F : locallyFinsuppWithin U Y
h : F.support (U := U).Finite
this :
  (Function.support (M := locallyFinsuppWithin U Y) fun (x : X) ↦
      restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯) ⊆
    (↑(h.toFinset (s := F.support (U := U))) : Set X)
z : X
hz : ¬z ∉ U
pos :
  ∀ (hz : z ∈ F.support (U := U)),
    Eq.{u_2 + 1} (α := Y)
      (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
      ((F : (a : X) → Y) z : Y)
⊢ Eq.{u_2 + 1} (α := Y)
    (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
    ((F : (a : X) → Y) z : Y)
have neg : ∀ (hz : z ∉ F.support (U := U)),
  Eq.{u_2 + 1} (α := Y)
    (if z ∈ U then if z ∈ h.toFinset (s := F.support (U := U)) then (F : (a : X) → Y) z else 0 else 0 : Y)
    ((F : (a : X) → Y) z : Y)
Tactic: by_cases hz : z ∈ F.support
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊔ D₂).restrict (U := U) (V := V) h = D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h
have h₁ : ∀ (x : X),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have pos : ∀ (hx : x ∈ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (hx : x ∈ V),
    Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
      ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have neg : ∀ (hx : x ∉ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊔ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
⊢ (D₁ ⊓ D₂).restrict (U := U) (V := V) h = D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h
have h₁ : ∀ (x : X),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have pos : ∀ (hx : x ∈ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
inst_2 : Lattice Y
V : Set X
h : V ⊆ U
D₁ D₂ : locallyFinsuppWithin U Y
x : X
pos :
  ∀ (hx : x ∈ V),
    Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
      ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
⊢ Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
have neg : ∀ (hx : x ∉ V),
  Eq.{u_2 + 1} (α := Y) (((D₁ ⊓ D₂).restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
    ((D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h : (a : X) → Y) x : Y)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
⊢ D⁺.restrict (U := U) (V := V) h = (D.restrict (U := U) (V := V) h)⁺
have h₁ : ∀ (x : X),
  Eq (α := ℤ) ((D⁺.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
    (((D.restrict (U := U) (V := V) h)⁺ : (a : X) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
⊢ D⁻.restrict (U := U) (V := V) h = (D.restrict (U := U) (V := V) h)⁻
have h₁ : ∀ (x : X),
  Eq (α := ℤ) ((D⁻.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
    (((D.restrict (U := U) (V := V) h)⁻ : (a : X) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.LocallyFinsupp (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ Eq (α := ℤ) ((D⁻.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
    (((D.restrict (U := U) (V := V) h)⁻ : (a : X) → ℤ) x : ℤ)
have h₁ : Eq (α := ℤ) (if x ∈ V then ((D : (a : X) → ℤ) x)⁻ else 0 : ℤ) ((if x ∈ V then (D : (a : X) → ℤ) x else 0)⁻ : ℤ)
Tactic: simp only [locallyFinsuppWithin.restrict_apply, locallyFinsuppWithin.negPart_apply]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ inst_1 = induced (g ∘ f) inst_2
have rw : induced f inst = induced (g ∘ f) inst_2
Tactic: rw [hf.eq_induced, hg.eq_induced, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
rw : induced f inst = induced (g ∘ f) inst_2
⊢ inst_1 = induced (g ∘ f) inst_2
have rw₁ : induced f (induced g inst_2) = induced (g ∘ f) inst_2
Tactic: rw [hf.eq_induced, hg.eq_induced, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
rw : induced f inst = induced (g ∘ f) inst_2
rw₁ : induced f (induced g inst_2) = induced (g ∘ f) inst_2
⊢ inst_1 = induced (g ∘ f) inst_2
have rw₂ : induced (g ∘ f) inst_2 = induced (g ∘ f) inst_2
Tactic: rw [hf.eq_induced, hg.eq_induced, induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
⊢ IsInducing (g ∘ f) ↔ IsInducing f
have refine : ∀ (h : IsInducing (g ∘ f)), IsInducing f
Tactic: refine ⟨fun h ↦ ?_, hg.comp⟩
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ IsInducing f
have rw : inst_1 = induced f inst
Tactic: rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
rw : inst_1 = induced f inst
⊢ IsInducing f
have rw₁ : inst_1 = induced f (induced g inst_2)
Tactic: rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
rw : inst_1 = induced f inst
rw₁ : inst_1 = induced f (induced g inst_2)
⊢ IsInducing f
have rw₂ : inst_1 = induced (g ∘ f) inst_2
Tactic: rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
rw : inst_1 = induced f inst
rw₁ : inst_1 = induced f (induced g inst_2)
rw₂ : inst_1 = induced (g ∘ f) inst_2
⊢ IsInducing f
have rw₃ : induced (g ∘ f) inst_2 = induced (g ∘ f) inst_2
Tactic: rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : Continuous[inst_1, inst] f
hg : Continuous[inst, inst_2] g
hgf : IsInducing (g ∘ f)
⊢ induced f inst ≤ inst_1
have grw : induced f inst ≤ induced (g ∘ f) inst_2
Tactic: grw [hgf.eq_induced, ← induced_compose, ← hg.le_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : Continuous[inst_1, inst] f
hg : Continuous[inst, inst_2] g
hgf : IsInducing (g ∘ f)
grw : induced f inst ≤ induced (g ∘ f) inst_2
⊢ induced f inst ≤ inst_1
have grw₁ : induced f inst ≤ induced f (induced g inst_2)
Tactic: grw [hgf.eq_induced, ← induced_compose, ← hg.le_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : Continuous[inst_1, inst] f
hg : Continuous[inst, inst_2] g
hgf : IsInducing (g ∘ f)
grw : induced f inst ≤ induced (g ∘ f) inst_2
grw₁ : induced f inst ≤ induced f (induced g inst_2)
⊢ induced f inst ≤ inst_1
have grw₂ : induced f inst ≤ induced f inst
Tactic: grw [hgf.eq_induced, ← induced_compose, ← hg.le_induced]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot
have rw : (map f (comap f (𝓝 (f x)) ⊓ l)).NeBot ↔ (𝓝 x ⊓ l).NeBot
Tactic: rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
rw : (map f (comap f (𝓝 (f x)) ⊓ l)).NeBot ↔ (𝓝 x ⊓ l).NeBot
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot
have rw₁ : (map f (𝓝 x ⊓ l)).NeBot ↔ (𝓝 x ⊓ l).NeBot
Tactic: rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
rw : (map f (comap f (𝓝 (f x)) ⊓ l)).NeBot ↔ (𝓝 x ⊓ l).NeBot
rw₁ : (map f (𝓝 x ⊓ l)).NeBot ↔ (𝓝 x ⊓ l).NeBot
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot
have rw₂ : (𝓝 x ⊓ l).NeBot ↔ (𝓝 x ⊓ l).NeBot
Tactic: rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
have rw : Tendsto f l (comap g (𝓝 (g y))) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
Tactic: rw [hg.nhds_eq_comap, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
rw : Tendsto f l (comap g (𝓝 (g y))) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
have rw₁ : Tendsto (g ∘ f) l (𝓝 (g y)) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
Tactic: rw [hg.nhds_eq_comap, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hg : IsInducing g
⊢ Continuous[inst_1, inst] f ↔ Continuous[inst_1, inst_2] (g ∘ f)
have simp_rw : (∀ (x : X), ContinuousAt f x) ↔ ∀ (x : X), ContinuousAt (g ∘ f) x
Tactic: simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
have simp_rw : Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))
Tactic: simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
simp_rw : Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
have simp_rw₁ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (𝓝 (f x)) ≤ 𝓝 (g (f x))
Tactic: simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
simp_rw : Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))
simp_rw₁ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (𝓝 (f x)) ≤ 𝓝 (g (f x))
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
have simp_rw₂ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (map f (𝓝 x)) ≤ 𝓝 (g (f x))
Tactic: simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
simp_rw : Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))
simp_rw₁ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (𝓝 (f x)) ≤ 𝓝 (g (f x))
simp_rw₂ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (map f (𝓝 x)) ≤ 𝓝 (g (f x))
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
have simp_rw₃ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map (g ∘ f) (𝓝 x) ≤ 𝓝 (g (f x))
Tactic: simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]
-- Lean 4 proof step from Mathlib.Topology.Maps.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ closure[inst_1] s = f ⁻¹' closure[inst] (f '' s)
have h : ∀ (x : X), x ∈ closure[inst_1] s ↔ x ∈ f ⁻¹' closure[inst] (f '' s)
Tactic: ext x