awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y : A
hy_2 : y ∈ (↑(adjoin R {x}) : Set A)
hy : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) y
mem : ∀ (u : A) (hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u) (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
algebraMap₁ :
  ∀ (r : R) (hy : Membership.mem (α := A) (↑(adjoin R {x}) : Set A) ((Algebra.algebraMap R A : (a : R) → A) r : A)),
    P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
⊢ P y ⋯
have add₁ : ∀ (u v : A) (hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u)
  (hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v)
  (hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u sorry) (hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v sorry)
  (hy : u + v ∈ (↑(adjoin R {x}) : Set A)), P (u + v) sorry
Tactic: induction hy using Algebra.adjoin_induction with
  | mem u hu =>
    obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
    · exact self
    · simp_rw [← hu, star_star] at star_self
      exact star_self
  | algebraMap r => exact algebraMap r
  | add u v hu_mem hv_mem hu hv =>
    exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
  | mul u v hu_mem hv_mem hu hv =>
    exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
Cleared hypotheses: hy_2, hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
x y_1 : A
hy_1 : Membership.mem (γ := StarSubalgebra R A) (elemental R x) y_1
P : (u : A) → Membership.mem (γ := StarSubalgebra R A) (elemental R x) u → Prop
self : P x ⋯
star_self : P (star x) ⋯
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u + v) ⋯
mul :
  ∀ (u : A) (hu : Membership.mem (γ := StarSubalgebra R A) (elemental R x) u) (v : A)
    (hv : Membership.mem (γ := StarSubalgebra R A) (elemental R x) v), P u hu → P v hv → P (u * v) ⋯
closure :
  ∀ (s : Set A) (hs : s ⊆ (↑(elemental R x) : Set A)),
    (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure[inst_2] s), P v ⋯
y : A
hy_2 : y ∈ (↑(adjoin R {x}) : Set A)
hy : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) y
mem : ∀ (u : A) (hu : Membership.mem (γ := Set A) ({x} ∪ star {x}) u) (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯
algebraMap₁ :
  ∀ (r : R) (hy : Membership.mem (α := A) (↑(adjoin R {x}) : Set A) ((Algebra.algebraMap R A : (a : R) → A) r : A)),
    P ((Algebra.algebraMap R A : (a : R) → A) r) ⋯
add₁ :
  ∀ (u v : A) (hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u)
    (hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v)
    (hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u ⋯) (hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v ⋯)
    (hy : u + v ∈ (↑(adjoin R {x}) : Set A)), P (u + v) ⋯
⊢ P y ⋯
have mul₁ : ∀ (u v : A) (hu_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) u)
  (hv_mem : Membership.mem (γ := Subalgebra R A) (Algebra.adjoin R ({x} ∪ star {x})) v)
  (hu : ∀ (hy : u ∈ (↑(adjoin R {x}) : Set A)), P u sorry) (hv : ∀ (hy : v ∈ (↑(adjoin R {x}) : Set A)), P v sorry)
  (hy : u * v ∈ (↑(adjoin R {x}) : Set A)), P (u * v) sorry
Tactic: induction hy using Algebra.adjoin_induction with
  | mem u hu =>
    obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
    · exact self
    · simp_rw [← hu, star_star] at star_self
      exact star_self
  | algebraMap r => exact algebraMap r
  | add u v hu_mem hv_mem hu hv =>
    exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
  | mul u v hu_mem hv_mem hu hv =>
    exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
Cleared hypotheses: hy_2, hy
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
⊢ φ = ψ
have refine : ∀ (x : ↥(adjoin R {a})),
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
Tactic: refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
have refine_1 : ∀ (x : A) (h : Membership.mem (γ := Set A) {a} x),
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x sorry) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x sorry) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
Tactic: refine adjoin_induction_subtype x ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.StarSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : Semiring A
inst_4 : StarRing A
inst_5 : IsSemitopologicalSemiring A
inst_6 : ContinuousStar A
inst_7 : Algebra R A
inst_8 : StarModule R A
inst_9 : TopologicalSpace B
inst_10 : Semiring B
inst_11 : StarRing B
inst_12 : Algebra R B
inst_13 : T2Space B
F : Type u_4
a : A
inst_14 : FunLike.{u_4 + 1, u_2 + 1, u_3 + 1} F (↥(elemental R a)) B
inst_15 : AlgHomClass.{u_4, u_1, u_2, u_3} F R (↥(elemental R a)) B
inst_16 : StarHomClass.{u_4, u_2, u_3} F (↥(elemental R a)) B
φ ψ : F
hφ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑φ : (a : ↥(elemental R a)) → B)
hψ : Continuous[instTopologicalSpaceSubtype, inst_9] (⇑ψ : (a : ↥(elemental R a)) → B)
h :
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
    ((ψ : (a : ↥(elemental R a)) → B)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (elemental R a) x) a ⋯) :
      B)
x : ↥(adjoin R {a})
refine_1 :
  ∀ (x : A) (h : Membership.mem (γ := Set A) {a} x),
    Eq.{u_3 + 1} (α := B)
      ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x ⋯) :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
      ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
          ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := StarSubalgebra R A) (adjoin R {a}) x) x ⋯) :
            ↥(topologicalClosure (adjoin R {a}))) :
        B)
⊢ Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion ⋯ : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure) x :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
have refine_2 : ∀ (r : R),
  Eq.{u_3 + 1} (α := B)
    ((φ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            ((algebraMap R ↥(adjoin R {a}) : (a_1 : R) → ↥(adjoin R {a})) r) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
    ((ψ : (a : ↥(adjoin R {a}).topologicalClosure) → B)
        ((inclusion sorry : (a_1 : ↥(adjoin R {a})) → ↥(adjoin R {a}).topologicalClosure)
            ((algebraMap R ↥(adjoin R {a}) : (a_1 : R) → ↥(adjoin R {a})) r) :
          ↥(topologicalClosure (adjoin R {a}))) :
      B)
Tactic: refine adjoin_induction_subtype x ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1
have rw : closure[inst_1] (mulSupport f) = ∅ ↔ f = 1
Tactic: rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
rw : closure[inst_1] (mulSupport f) = ∅ ↔ f = 1
⊢ mulTSupport f = ∅ ↔ f = 1
have rw₁ : mulSupport f = ∅ ↔ f = 1
Tactic: rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
rw : closure[inst_1] (mulSupport f) = ∅ ↔ f = 1
rw₁ : mulSupport f = ∅ ↔ f = 1
⊢ mulTSupport f = ∅ ↔ f = 1
have rw₂ : f = 1 ↔ f = 1
Tactic: rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ 1) ∅
have rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) fun (x : X) ↦ 1)) ∅
Tactic: rw [mulTSupport, mulSupport_fun_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) fun (x : X) ↦ 1)) ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ 1) ∅
have rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
Tactic: rw [mulTSupport, mulSupport_fun_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) fun (x : X) ↦ 1)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) fun (x : X) ↦ 1) ∅
have rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [mulTSupport, mulSupport_fun_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) 1) ∅
have rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) 1)) ∅
Tactic: rw [mulTSupport, mulSupport_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) 1)) ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) 1) ∅
have rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
Tactic: rw [mulTSupport, mulSupport_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport.{u_1, u_2} (M := α) 1)) ∅
rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ∅) ∅
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport.{u_1, u_2} (α := α) 1) ∅
have rw₂ : Eq.{u_1 + 1} (α := Set X) ∅ ∅
Tactic: rw [mulTSupport, mulSupport_one, closure_empty]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq g hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq g hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
hg : ∀ {x : α}, g x = 1 ↔ x = 1
f : X → α
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw₂ : closure[inst_1] (mulSupport f) = closure[inst_1] (mulSupport f)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq g hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_of_range_subset hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_of_range_subset hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
β : Type u_4
inst : One α
inst_1 : TopologicalSpace X
inst_2 : One β
g : α → β
f : X → α
hg : ∀ {x : α}, x ∈ range f → (g x = 1 ↔ x = 1)
rw : closure[inst_1] (mulSupport (g ∘ f)) = mulTSupport f
rw₁ : closure[inst_1] (mulSupport (g ∘ f)) = closure[inst_1] (mulSupport f)
⊢ mulTSupport (g ∘ f) = mulTSupport f
have rw₂ : closure[inst_1] (mulSupport f) = closure[inst_1] (mulSupport f)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_of_range_subset hg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst_1, inst_2] f
⊢ mulTSupport (g ∘ f) ⊆ f ⁻¹' mulTSupport g
have rw : closure[inst_1] (f ⁻¹' mulSupport g) ⊆ f ⁻¹' closure[inst_2] (mulSupport g)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport (g ∘ (⇑f : (a : X) → Y))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
have rw : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y)))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage, Homeomorph.preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
rw :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport (g ∘ (⇑f : (a : X) → Y))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
have rw₁ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
  ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage, Homeomorph.preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
rw :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
rw₁ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport (g ∘ (⇑f : (a : X) → Y))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
have rw₂ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
  ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage, Homeomorph.preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
Y : Type u_9
inst_2 : TopologicalSpace Y
g : Y → α
f : X ≃ₜ Y
rw :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
rw₁ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] (mulSupport (g ∘ (⇑f : (a : X) → Y))))
    ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
rw₂ :
  Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
    ((⇑f : (a : X) → Y) ⁻¹' closure[inst_2] (mulSupport g))
⊢ Eq.{u_1 + 1} (α := Set X) (mulTSupport (g ∘ (⇑f : (a : X) → Y))) ((⇑f : (a : X) → Y) ⁻¹' mulTSupport g)
have rw₃ : Eq.{u_1 + 1} (α := Set X) (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
  (closure[inst_1] ((⇑f : (a : X) → Y) ⁻¹' mulSupport g))
Tactic: rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage, Homeomorph.preimage_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
X : Type u_1
α : Type u_2
inst : One α
inst_1 : TopologicalSpace X
f : X → α
⊢ range f ⊆ insert 1 (f '' mulTSupport f)
have grw : range f ⊆ insert 1 (f '' mulSupport f)
Tactic: grw [← subset_mulTSupport f]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Support (goal)
Goal:
α : Type u_2
β : Type u_4
inst : TopologicalSpace α
inst_1 : One β
f : α → β
x : α
simp_rw : x ∉ closure[inst] (mulSupport f) ↔ f =ᶠ[𝓝 x] 1
simp_rw₁ : (¬∀ t ∈ 𝓝 x, (t ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
⊢ x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
have simp_rw₂ : (∃ (x_1 : Set α) (_ : x_1 ∈ 𝓝 x), ¬(x_1 ∩ mulSupport f).Nonempty) ↔ f =ᶠ[𝓝 x] 1
Tactic: simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
    ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]