awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyFinsupp
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
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:
simp [restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U : Set X
Y : Type u_2
inst_1 : AddCommGroup Y
V : Set X
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ (restrictMonoidHom (U := U) (V := V) h : (a : locallyFinsuppWithin U Y) → locallyFinsuppWithin V Y) D =
    D.restrict (U := U) (V := V) h

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyFinsupp
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
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)) ⋯
⊢ 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)

Tactic:
contrapose
-- Module: Mathlib.Topology.LocallyFinsupp
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
⊢ 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)) ⋯

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
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
⊢ (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)

Tactic:
have : (fun x ↦ (single x (F x)).restrict (subset_univ U)).support ⊆ h.toFinset := by
    intro
    contrapose
    aesop
-- Module: Mathlib.Topology.LocallyFinsupp
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)
rw : ∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ = F
⊢ ∑ᶠ (x : X), restrict (U := univ) (V := U) (single x ((F : (a : X) → Y) x)) ⋯ = F

Tactic:
rw [finsum_eq_sum_of_support_subset _ this]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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)) ⋯ :
            (a : X) → Y)
          z :
        Y)
      ((F : (a : X) → Y) z : Y)
⊢ ∑ i ∈ h.toFinset (s := F.support (U := U)), restrict (U := univ) (V := U) (single i ((F : (a : X) → Y) i)) ⋯ = F

Tactic:
ext z
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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)) ⋯ :
            (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)

Tactic:
by_cases hz : z ∉ U
-- Module: Mathlib.Topology.LocallyFinsupp
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)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
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
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)
⊢ 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)

Tactic:
simp [restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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)
⊢ 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

Premises used: Function.locallyFinsuppWithin.support
-- Module: Mathlib.Topology.LocallyFinsupp
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_1 : ¬z ∉ U
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:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
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_1 : ¬z ∉ U
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:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
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
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)
⊢ (D₁ ⊔ D₂).restrict (U := U) (V := V) h = D₁.restrict (U := U) (V := V) h ⊔ D₂.restrict (U := U) (V := V) h

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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)
⊢ 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
-- Module: Mathlib.Topology.LocallyFinsupp
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
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:
simp [locallyFinsuppWithin.restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
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
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:
simp [locallyFinsuppWithin.restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
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
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)
⊢ (D₁ ⊓ D₂).restrict (U := U) (V := V) h = D₁.restrict (U := U) (V := V) h ⊓ D₂.restrict (U := U) (V := V) h

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
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)
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)
⊢ 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
-- Module: Mathlib.Topology.LocallyFinsupp
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
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:
simp [locallyFinsuppWithin.restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
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
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:
simp [locallyFinsuppWithin.restrict_apply, hx]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Topology.LocallyFinsupp
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
D : locallyFinsuppWithin U Y
h : V ⊆ U
⊢ (restrictLatticeHom (U := U) (V := V) h : (a : locallyFinsuppWithin U Y) → locallyFinsuppWithin V Y) D =
    D.restrict (U := U) (V := V) h

Tactic:
rfl
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
h₁ :
  ∀ (x : X),
    Eq (α := ℤ) ((D⁺.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
      (((D.restrict (U := U) (V := V) h)⁺ : (a : X) → ℤ) x : ℤ)
⊢ D⁺.restrict (U := U) (V := V) h = (D.restrict (U := U) (V := V) h)⁺

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ Eq (α := ℤ) (if x ∈ V then ((D : (a : X) → ℤ) x)⁺ else 0 : ℤ) ((if x ∈ V then (D : (a : X) → ℤ) x else 0)⁺ : ℤ)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
h₁ :
  ∀ (x : X),
    Eq (α := ℤ) ((D⁻.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
      (((D.restrict (U := U) (V := V) h)⁻ : (a : X) → ℤ) x : ℤ)
⊢ D⁻.restrict (U := U) (V := V) h = (D.restrict (U := U) (V := V) h)⁻

Tactic:
ext x
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
h₁ : Eq (α := ℤ) (if x ∈ V then ((D : (a : X) → ℤ) x)⁻ else 0 : ℤ) ((if x ∈ V then (D : (a : X) → ℤ) x else 0)⁻ : ℤ)
⊢ Eq (α := ℤ) ((D⁻.restrict (U := U) (V := V) h : (a : X) → ℤ) x : ℤ)
    (((D.restrict (U := U) (V := V) h)⁻ : (a : X) → ℤ) x : ℤ)

Tactic:
simp only [locallyFinsuppWithin.restrict_apply, locallyFinsuppWithin.negPart_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply, Function.locallyFinsuppWithin.negPart_apply
-- Module: Mathlib.Topology.LocallyFinsupp
Goal:
X : Type u_1
inst : TopologicalSpace X
U V : Set X
D : locallyFinsuppWithin U ℤ
h : V ⊆ U
x : X
⊢ Eq (α := ℤ) (if x ∈ V then ((D : (a : X) → ℤ) x)⁻ else 0 : ℤ) ((if x ∈ V then (D : (a : X) → ℤ) x else 0)⁻ : ℤ)

Tactic:
aesop
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace Y
f : X → Y
⊢ IsInducing f

Tactic:
@IsInducing.mk _ _ (TopologicalSpace.induced f ‹_›) _ _ rfl

Premises used: Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsInducing.{u_1, u_1} (X := X) id

Tactic:
⟨induced_id.symm⟩

Premises used: induced_id, Topology.IsInducing.mk, Eq.symm
-- Module: Mathlib.Topology.Maps.Basic
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
rw₂ rw₃ : induced (g ∘ f) inst_2 = induced (g ∘ f) inst_2
⊢ inst_1 = induced (g ∘ f) inst_2

Tactic:
rw [hf.eq_induced, hg.eq_induced, induced_compose]

Premises used: induced_compose, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
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

Tactic:
⟨fun h ↦ ?_, hg.comp⟩

Premises used: Topology.IsInducing.comp, Iff.intro
-- Module: Mathlib.Topology.Maps.Basic
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
refine : ∀ (h : IsInducing (g ∘ f)), IsInducing f
⊢ IsInducing (g ∘ f) ↔ IsInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩
-- Module: Mathlib.Topology.Maps.Basic
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
rw₃ rw₄ : induced (g ∘ f) inst_2 = induced (g ∘ f) inst_2
⊢ IsInducing f

Tactic:
rw [isInducing_iff, hg.eq_induced, induced_compose, h.eq_induced]

Premises used: induced_compose, Topology.isInducing_iff, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
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)
grw₂ grw₃ : induced f inst ≤ induced f inst
⊢ induced f inst ≤ inst_1

Tactic:
grw [hgf.eq_induced, ← induced_compose, ← hg.le_induced]

Premises used: induced_compose, Continuous.le_induced, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
⊢ IsInducing f ↔ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
(isInducing_iff _).trans (induced_iff_nhds_eq f)

Premises used: induced_iff_nhds_eq, Topology.isInducing_iff, Iff.trans
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
isInducing_iff_nhds.1 hf

Premises used: Topology.isInducing_iff_nhds, Iff.mp
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
ι : Type u_4
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
p : ι → Prop
s : ι → Set Y
hf : IsInducing f
x : X
h_basis : (𝓝 (f x)).HasBasis p s
⊢ (𝓝 x).HasBasis p (preimage f ∘ s)

Tactic:
hf.nhds_eq_comap x ▸ h_basis.comap f

Premises used: Topology.IsInducing.nhds_eq_comap, Eq.rec, Filter.HasBasis.comap, Eq.symm
-- Module: Mathlib.Topology.Maps.Basic
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
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))

Tactic:
simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]

Premises used: Topology.IsInducing.nhds_eq_comap, iSup_image, Filter.comap_iSup, sSup_image, nhdsSet
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
⊢ map f (𝓝 x) = 𝓝[range f] f x

Tactic:
hf.eq_induced ▸ map_nhds_induced_eq x

Premises used: Eq.rec, map_nhds_induced_eq, Eq.symm, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
hf.eq_induced ▸ map_nhds_induced_of_mem h

Premises used: Eq.rec, Eq.symm, Topology.IsInducing.eq_induced, map_nhds_induced_of_mem
-- Module: Mathlib.Topology.Maps.Basic
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
rw₂ rw₃ : (𝓝 x ⊓ l).NeBot ↔ (𝓝 x ⊓ l).NeBot
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot

Tactic:
rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.push_pull', Filter.map_neBot_iff
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝[range f] f x

Tactic:
hf.map_nhds_eq x ▸ image_mem_map hs

Premises used: Eq.rec, Filter.image_mem_map, Topology.IsInducing.map_nhds_eq
-- Module: Mathlib.Topology.Maps.Basic
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))
rw₁ rw₂ : Tendsto (g ∘ f) l (𝓝 (g y)) ↔ Tendsto (g ∘ f) l (𝓝 (g y))
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
rw [hg.nhds_eq_comap, tendsto_comap_iff]

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.tendsto_comap_iff
-- Module: Mathlib.Topology.Maps.Basic
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
x : X
⊢ ContinuousAt f x ↔ ContinuousAt (g ∘ f) x

Tactic:
hg.tendsto_nhds_iff

Premises used: ContinuousAt, Topology.IsInducing.tendsto_nhds_iff
-- Module: Mathlib.Topology.Maps.Basic
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
simp_rw : (∀ (x : X), ContinuousAt f x) ↔ ∀ (x : X), ContinuousAt (g ∘ f) x
⊢ Continuous[inst_1, inst] f ↔ Continuous[inst_1, inst_2] (g ∘ f)

Tactic:
simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]

Premises used: Topology.IsInducing.continuousAt_iff, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Maps.Basic
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))
simp_rw₃ : map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map (g ∘ f) (𝓝 x) ≤ 𝓝 (g (f x))
⊢ ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)

Tactic:
simp_rw [ContinuousAt, Filter.Tendsto, ← hf.map_nhds_of_mem _ h, Filter.map_map, comp]

Premises used: Topology.IsInducing.map_nhds_of_mem, ContinuousAt, Function.comp, Filter.map_map, Filter.Tendsto
-- Module: Mathlib.Topology.Maps.Basic
Goal:
X : Type u_1
Y : Type u_2
f : X → Y
inst : TopologicalSpace Y
inst_1 : TopologicalSpace X
hf : IsInducing f
⊢ Continuous[inst_1, inst] f

Tactic:
hf.continuous_iff.mp continuous_id

Premises used: Topology.IsInducing.continuous_iff, continuous_id, Iff.mp