awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Mul Y
f g : LocallyConstant X Y
x : X
⊢ (f * g : (a : X) → Y) x = HMul.hMul (α := Y) (β := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MulZeroOneClass Y
U : Set X
hU : IsClopen U
⊢ Eq (α := (a : X) → Y) (⇑(charFn Y (U := U) hU) : (a : X) → Y) (U.indicator 1)

Tactic:
rfl

Premises used: Set.indicator, rfl, ite
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MulZeroOneClass Y
U : Set X
inst_2 : Nontrivial Y
x : X
hU : IsClopen U
⊢ Eq.{u_2 + 1} (α := Y) ((charFn Y (U := U) hU : (a : X) → Y) x : Y) (1 : Y) ↔ x ∈ U

Tactic:
Set.indicator_eq_one_iff_mem _

Premises used: Set.indicator, Set.indicator_eq_one_iff_mem, ite
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MulZeroOneClass Y
U : Set X
inst_2 : Nontrivial Y
x : X
hU : IsClopen U
⊢ Eq.{u_2 + 1} (α := Y) ((charFn Y (U := U) hU : (a : X) → Y) x : Y) (0 : Y) ↔ x ∉ U

Tactic:
Set.indicator_eq_zero_iff_notMem _

Premises used: Set.indicator, Set.indicator_eq_zero_iff_notMem, ite
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : MulZeroOneClass Y
U V : Set X
inst_2 : Nontrivial Y
hU : IsClopen U
hV : IsClopen V
h : charFn Y (U := U) hU = charFn Y (U := V) hV
⊢ U = V

Tactic:
Set.indicator_one_inj Y <| coe_inj.mpr h

Premises used: Iff.mpr, LocallyConstant.coe_inj, Set.indicator_one_inj
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Div Y
f g : LocallyConstant X Y
⊢ (⇑(f / g) : (a : X) → Y) = HDiv.hDiv (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Div Y
f g : LocallyConstant X Y
x : X
⊢ (f / g : (a : X) → Y) x = HDiv.hDiv (α := Y) (β := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
R : Type u_4
inst_1 : SMul R Y
r : R
f : LocallyConstant X Y
⊢ (⇑(r • f) : (a : X) → Y) = HSMul.hSMul (β := (a : X) → Y) r (⇑f : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
R : Type u_4
inst_1 : SMul R Y
r : R
f : LocallyConstant X Y
x : X
⊢ (r • f : (a : X) → Y) x = HSMul.hSMul (β := Y) r ((f : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
h :
  ∀ (x_1 : X),
    Eq.{u_2 + 1} (α := Y)
      ((HMul.hMul (α := LocallyConstant X Y)
              ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
            (a : X) → Y)
          x_1 :
        Y)
      ((HMul.hMul (β := LocallyConstant X Y) x
              ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) :
            (a : X) → Y)
          x_1 :
        Y)
⊢ HMul.hMul (α := LocallyConstant X Y)
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x =
    HMul.hMul (β := LocallyConstant X Y) x
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y)

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)
    ((HMul.hMul (β := LocallyConstant X Y) x
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) :
          (a : X) → Y)
        x_1 :
      Y)

Tactic:
Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)
    ((HMul.hMul (β := LocallyConstant X Y) x
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) :
          (a : X) → Y)
        x_1 :
      Y)

Tactic:
exact Algebra.commutes' _ _

Premises used: Algebra.commutes'
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
h :
  ∀ (x_1 : X),
    Eq.{u_2 + 1} (α := Y) ((r • x : (a : X) → Y) x_1 : Y)
      ((HMul.hMul (α := LocallyConstant X Y)
              ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
            (a : X) → Y)
          x_1 :
        Y)
⊢ r • x =
    HMul.hMul (α := LocallyConstant X Y)
      ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x

Tactic:
ext
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y) ((r • x : (a : X) → Y) x_1 : Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)

Tactic:
Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
x : LocallyConstant X Y
x_1 : X
⊢ Eq.{u_2 + 1} (α := Y) ((r • x : (a : X) → Y) x_1 : Y)
    ((HMul.hMul (α := LocallyConstant X Y)
            ((RingHom.comp constRingHom (algebraMap R Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) x :
          (a : X) → Y)
        x_1 :
      Y)

Tactic:
exact Algebra.smul_def' _ _

Premises used: Algebra.smul_def'
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
r : R
⊢ Eq (α := (a : X) → Y)
    (⇑((algebraMap R (LocallyConstant X Y) : (a : R) → LocallyConstant X Y) r : LocallyConstant X Y) : (a : X) → Y)
    ((algebraMap R (X → Y) : (a : R) → X → Y) r)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
R : Type u_5
inst_1 : TopologicalSpace Y
Z : Type u_6
inst_2 : Semiring R
inst_3 : AddCommMonoid Z
inst_4 : Module R Z
f : C(X, Y)
hfs : Function.Surjective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑f : (a : X) → Y)
⊢ Eq (α := Submodule R (LocallyConstant Y Z)) (LinearMap.ker (comapₗ R f)) ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective <| comap_injective _ hfs

Premises used: LocallyConstant.comap_injective, LinearMap.ker_eq_bot_of_injective
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
Z : Type u_6
inst_1 : MulOneClass Y
inst_2 : MulOneClass Z
f : Y →* Z
⊢ Eq (α := LocallyConstant X Z) (map.{u_1, u_2, u_6} (Y := Y) (⇑f : (a : Y) → Z) 1) 1

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R : Type u_5
Z : Type u_6
inst_1 : MulOneClass Y
inst_2 : MulOneClass Z
f : Y →* Z
⊢ ∀ (x y : LocallyConstant X Y),
    map (⇑f : (a : Y) → Z) (x * y) =
      HMul.hMul (α := LocallyConstant X Z) (map (⇑f : (a : Y) → Z) x) (map (⇑f : (a : Y) → Z) y)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R_2 : Type u_5
Z : Type u_6
R : Type u_7
inst_1 : Semiring R
inst_2 : AddCommMonoid Y
inst_3 : Module R Y
inst_4 : AddCommMonoid Z
inst_5 : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (x y : LocallyConstant X Y),
    map (⇑f : (a : Y) → Z) (x + y) =
      HAdd.hAdd (α := LocallyConstant X Z) (map (⇑f : (a : Y) → Z) x) (map (⇑f : (a : Y) → Z) y)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R_2 : Type u_5
Z : Type u_6
R : Type u_7
inst_1 : Semiring R
inst_2 : AddCommMonoid Y
inst_3 : Module R Y
inst_4 : AddCommMonoid Z
inst_5 : Module R Z
f : Y →ₗ[R] Z
⊢ ∀ (m : R) (x : LocallyConstant X Y),
    map (⇑f : (a : Y) → Z) (m • x) =
      HSMul.hSMul (α := R) (β := LocallyConstant X Z) ((RingHom.id R : (a : R) → R) m : R) (map (⇑f : (a : Y) → Z) x)

Tactic:
aesop
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
α : Type u_3
R_1 : Type u_4
R_2 : Type u_5
Z : Type u_6
R : Type u_7
inst_1 : CommSemiring R
inst_2 : Semiring Y
inst_3 : Algebra R Y
inst_4 : Semiring Z
inst_5 : Algebra R Z
f : Y →ₐ[R] Z
x : R
⊢ Eq (α := LocallyConstant X Z)
    (OneHom.toFun
      (↑(↑(mapRingHom (↑f : Y →+* Z)) : LocallyConstant X Y →* LocallyConstant X Z) :
        OneHom (LocallyConstant X Y) (LocallyConstant X Z))
      ((algebraMap R (LocallyConstant X Y) : (a : R) → LocallyConstant X Y) x))
    ((algebraMap R (LocallyConstant X Z) : (a : R) → LocallyConstant X Z) x)

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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
⊢ ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})

Tactic:
tfae_have 1 → 4 := fun h y => h {y}
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
⊢ ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
⊢ ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
⊢ ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
⊢ ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}

Tactic:
tfae_have 4 → 3 := fun h x => h (f x)
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
⊢ ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
⊢ ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
⊢ ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
⊢ ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x

Tactic:
tfae_have 3 → 2 := fun h x => IsOpen.mem_nhds (h x) rfl

Premises used: IsOpen.mem_nhds, rfl
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
2 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
rcases :
  ∀ (U : Set X) (eq : U ⊆ {x_1 : X | (fun (x' : X) ↦ f x' = f x) x_1}) (hU : IsOpen[inst] U) (hx : x ∈ U),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
U : Set X
eq : U ⊆ {x_1 : X | (fun (x' : X) ↦ f x' = f x) x_1}
hU : IsOpen[inst] U
hx : x ∈ U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
⟨U, hU, hx, eq⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
U : Set X
eq : U ⊆ {x_1 : X | (fun (x' : X) ↦ f x' = f x) x_1}
hU : IsOpen[inst] U
hx : x ∈ U
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
exact ⟨U, hU, hx, eq⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
tfae_have 2 → 5
  | h, x => by
    rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩
    exact ⟨U, hU, hx, eq⟩
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ IsLocallyConstant f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
⊢ ∀ (a : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x), IsLocallyConstant f

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
refine : ∀ (x : X) (hx : x ∈ f ⁻¹' s), ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.LocallyConstant.Basic
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
tfae_1_to_4 : ∀ (a : IsLocallyConstant f) (y : Y), IsOpen[inst] (f ⁻¹' {y})
tfae_4_to_3 : ∀ (a : ∀ (y : Y), IsOpen[inst] (f ⁻¹' {y})) (x : X), IsOpen[inst] {x' : X | f x' = f x}
tfae_3_to_2 : ∀ (a : ∀ (x : X), IsOpen[inst] {x' : X | f x' = f x}) (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  ∀ (a : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) (x : X),
    ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
rcases :
  ∀ (U : Set X) (hU : IsOpen[inst] U) (hxU : x ∈ U) (eq : ∀ x' ∈ U, f x' = f x), ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen[inst] t ∧ x ∈ t

Tactic:
rcases h x with ⟨U, hU, hxU, eq⟩