awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : AddCommGroup M
inst_3 : Module R M
B : ModuleFilterBasis R M
inst_4 : IsTopologicalRing R
B' : AddGroupFilterBasis M := B.toAddGroupFilterBasis
x : TopologicalSpace M := B'.topology
h : IsTopologicalAddGroup M
⊢ ContinuousSMul R M

Tactic:
exact ContinuousSMul.of_basis_zero B'.nhds_zero_hasBasis
      (fun {_} => by simpa using B.smul)
      (by simpa using B.smul_left) B.smul_right

Premises used: ModuleFilterBasis.smul_right, AddGroupFilterBasis.nhds_zero_hasBasis, ContinuousSMul.of_basis_zero
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
rcases :
  ∀ (V : Set R) (V_in : V ∈ BR) (W : Set M) (W_in : W ∈ BM) (H : V • W ⊆ U),
    ∃ (V : Set R),
      Membership.mem (γ := Filter R) (𝓝 0) V ∧
        ∃ (W : Set M),
          Membership.mem (γ := Set (Set M))
              (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
            V • W ⊆ U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
V : Set R
V_in : V ∈ BR
W : Set M
W_in : W ∈ BM
H : V • W ⊆ U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩

Premises used: And.intro, Exists.intro, AddGroupFilterBasis.mem_nhds_zero, RingFilterBasis.toAddGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
V : Set R
V_in : V ∈ BR
W : Set M
W_in : W ∈ BM
H : V • W ⊆ U
⊢ ∃ (V : Set R),
    Membership.mem (γ := Filter R) (𝓝 0) V ∧
      ∃ (W : Set M),
        Membership.mem (γ := Set (Set M))
            (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) W ∧
          V • W ⊆ U

Tactic:
exact ⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
rcases : ∀ (V : Set R) (V_in : V ∈ BR) (H : V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U), ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
rcases smul_right m₀ U_in with ⟨V, V_in, H⟩
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
V : Set R
V_in : V ∈ BR
H : V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H

Premises used: Filter.Eventually, AddGroupFilterBasis.mem_nhds_zero, RingFilterBasis.toAddGroupFilterBasis, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.FilterBasis
Goal:
R_1 : Type u_1
M_1 : Type u_2
inst : CommRing R_1
inst_1 : TopologicalSpace R_1
inst_2 : AddCommGroup M_1
inst_3 : Module R_1 M_1
B : ModuleFilterBasis R_1 M_1
R : Type u_3
M : Type u_4
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : Module R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun (x : M) ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
x : TopologicalSpace R := BR.topology
m₀ : M
U : Set M
U_in :
  Membership.mem (γ := Set (Set M)) (FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    U
V : Set R
V_in : V ∈ BR
H : V ⊆ (fun (x : R) ↦ x • m₀) ⁻¹' U
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U

Tactic:
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) H

Premises used: AddGroupFilterBasis.mem_nhds_zero, RingFilterBasis.toAddGroupFilterBasis, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
α : Type u_3
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
l : Filter α
f g : α → P
x y : P
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y))

Tactic:
(continuous_vsub.tendsto (x, y)).comp (hf.prodMk_nhds hg)

Premises used: Prod.mk, Continuous.tendsto, IsTopologicalAddTorsor.continuous_vsub, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
α : Type u_3
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : TopologicalSpace α
f g : α → P
hf : Continuous[inst_5, inst_3] f
hg : Continuous[inst_5, inst_3] g
⊢ Continuous[inst_5, inst_1] fun (x : α) ↦ f x -ᵥ g x

Tactic:
continuous_vsub.comp₂ hf hg

Premises used: Continuous.comp₂, IsTopologicalAddTorsor.continuous_vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
α : Type u_3
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : TopologicalSpace α
f g : α → P
x : α
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_3, u_1} (Y := V) (fun (x : α) ↦ f x -ᵥ g x) x

Tactic:
hf.vsub hg

Premises used: ContinuousAt, Filter.Tendsto.vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
α : Type u_3
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : TopologicalSpace α
f g : α → P
x : α
s : Set α
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_3, u_1} (Y := V) (fun (x : α) ↦ f x -ᵥ g x) s x

Tactic:
hf.vsub hg

Premises used: ContinuousWithinAt, Filter.Tendsto.vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
α : Type u_3
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : TopologicalSpace α
f g : α → P
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_3, u_1} (Y := V) (fun (x : α) ↦ f x -ᵥ g x) s

Tactic:
fun x hx ↦
  (hf x hx).vsub (hg x hx)

Premises used: ContinuousOn, ContinuousWithinAt.vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
have : ∀ (p : P), Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
h : ∀ (x : V × V), x.1 + x.2
| Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2

Tactic:
enter [1, x]
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
x : V × V
h : x.1 + x.2 = ((x.1 + x.2) +ᵥ p) -ᵥ p
h₁ h₂ : x.1 + x.2 = x.1 + x.2
⊢ x.1 + x.2 = (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p

Tactic:
rw [vadd_vadd, vadd_vsub]

Premises used: vadd_vadd, vadd_vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
enter : fun (p : V × V) ↦ p.1 + p.2
h : ∀ (x : V × V), x.1 + x.2
| Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2

Tactic:
enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]

Premises used: vadd_vadd, vadd_vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
conv : Continuous[instTopologicalSpaceProd, inst_1] fun (x : V × V) ↦ (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : V × V) ↦ p.1 + p.2

Tactic:
conv =>
      enter [1, x]
      equals (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p => rw [vadd_vadd, vadd_vsub]

Premises used: vadd_vadd, vadd_vsub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : V × V) ↦ (x.1 +ᵥ x.2 +ᵥ p) -ᵥ p

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
have : ∀ (p : P), Continuous[inst_1, inst_1] fun (a : V) ↦ -a
⊢ Continuous[inst_1, inst_1] fun (a : V) ↦ -a

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
h : ∀ (v : V), -v
| Continuous[inst_1, inst_1] fun (a : V) ↦ -a

Tactic:
enter [1, v]
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
v : V
h : -v = p -ᵥ p - v
h₁ : -v = 0 - v
h₂ h₃ : -v = -v
⊢ -v = p -ᵥ (v +ᵥ p)

Tactic:
rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]

Premises used: vsub_vadd_eq_vsub_sub, vsub_self, zero_sub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
enter : fun (a : V) ↦ -a
h : ∀ (v : V), -v
| Continuous[inst_1, inst_1] fun (a : V) ↦ -a

Tactic:
enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]

Premises used: vsub_vadd_eq_vsub_sub, vsub_self, zero_sub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
conv : Continuous[inst_1, inst_1] fun (v : V) ↦ p -ᵥ (v +ᵥ p)
⊢ Continuous[inst_1, inst_1] fun (a : V) ↦ -a

Tactic:
conv =>
      enter [1, v]
      equals p -ᵥ (v +ᵥ p) => rw [vsub_vadd_eq_vsub_sub, vsub_self, zero_sub]

Premises used: vsub_vadd_eq_vsub_sub, vsub_self, zero_sub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
P : Type u_2
inst : AddGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
p : P
⊢ Continuous[inst_1, inst_1] fun (v : V) ↦ p -ᵥ (v +ᵥ p)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalAddGroup G
simp : Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦ x.1 - x.2
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦ x.1 -ᵥ x.2

Tactic:
simp only [vsub_eq_sub]

Premises used: vsub_eq_sub
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalAddGroup G
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦ x.1 - x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst_3] fun (p : (V × W) × P × Q) ↦ p.1.1 +ᵥ p.2.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst_8] fun (p : (V × W) × P × Q) ↦ p.1.2 +ᵥ p.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : (P × Q) × P × Q) ↦ x.1.1 -ᵥ x.2.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
V : Type u_1
W : Type u_2
P : Type u_3
Q : Type u_4
inst : AddCommGroup V
inst_1 : TopologicalSpace V
inst_2 : AddTorsor V P
inst_3 : TopologicalSpace P
inst_4 : IsTopologicalAddTorsor P
inst_5 : AddCommGroup W
inst_6 : TopologicalSpace W
inst_7 : AddTorsor W Q
inst_8 : TopologicalSpace Q
inst_9 : IsTopologicalAddTorsor Q
⊢ Continuous[instTopologicalSpaceProd, inst_6] fun (x : (P × Q) × P × Q) ↦ x.1.2 -ᵥ x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
simp :
  ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_3 i] fun (a : ((i : ι) → V i) × ((i : ι) → P i)) ↦ a.1 i +ᵥ a.2 i
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_3 i] fun (a : ((i : ι) → V i) × ((i : ι) → P i)) ↦ (a.1 +ᵥ a.2) i

Tactic:
simp only [Pi.vadd_apply']

Premises used: Pi.vadd_apply'
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_3 i] fun (a : ((i : ι) → V i) × ((i : ι) → P i)) ↦ a.1 i +ᵥ a.2 i

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
simp :
  ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_1 i] fun (a : ((i : ι) → P i) × ((i : ι) → P i)) ↦ a.1 i -ᵥ a.2 i
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_1 i] fun (a : ((i : ι) → P i) × ((i : ι) → P i)) ↦ (a.1 -ᵥ a.2) i

Tactic:
simp only [Pi.vsub_apply]

Premises used: Pi.vsub_apply
-- Module: Mathlib.Topology.Algebra.Group.AddTorsor
Goal:
ι : Type u_1
V : ι → Type u_2
P : ι → Type u_3
inst : (i : ι) → AddCommGroup (V i)
inst_1 : (i : ι) → TopologicalSpace (V i)
inst_2 : (i : ι) → AddTorsor.{u_2, u_3} (V i) (P i)
inst_3 : (i : ι) → TopologicalSpace (P i)
inst_4 : ∀ (i : ι), IsTopologicalAddTorsor.{u_2, u_3} (P i)
⊢ ∀ (i : ι), Continuous[instTopologicalSpaceProd, inst_1 i] fun (a : ((i : ι) → P i) × ((i : ι) → P i)) ↦ a.1 i -ᵥ a.2 i

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
rw : IsClosed[inst_1] (⋂ (i : M), {x : M | i ∈ s → i * x = x * i})
⊢ IsClosed[inst_1] s.centralizer

Tactic:
rw [centralizer, setOf_forall]

Premises used: Set.centralizer, Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
⊢ IsClosed[inst_1] (⋂ (i : M), {x : M | i ∈ s → i * x = x * i})

Tactic:
isClosed_sInter ?_

Premises used: iInf, Set.iInter, isClosed_sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
refine :
  ∀ (t : Set M),
    Membership.mem (γ := Set (Set M)) (range fun (i : M) ↦ {x : M | i ∈ s → i * x = x * i}) t → IsClosed[inst_1] t
⊢ IsClosed[inst_1] (⋂ (i : M), {x : M | i ∈ s → i * x = x * i})

Tactic:
refine isClosed_sInter ?_

Premises used: isClosed_sInter
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
⊢ IsOpen[inst_1] {x : M | m ∈ s}

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
refine_1 : Continuous[inst_1, inst_1] (HMul.hMul m)
refine_2 : Continuous[inst_1, inst_1] fun (x : M) ↦ x * m
⊢ IsClosed[inst_1] ((fun (i : M) ↦ ({x : M | i ∈ s → i * x = x * i} : Set M)) m)

Tactic:
refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_

Premises used: isClosed_imp, isClosed_eq
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
⊢ Continuous[inst_1, inst_1] (HMul.hMul m)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
M : Type u_1
s : Set M
inst : Mul M
inst_1 : TopologicalSpace M
inst_2 : SeparatelyContinuousMul M
inst_3 : T2Space M
m : M
⊢ Continuous[inst_1, inst_1] fun (x : M) ↦ x * m

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ Eq (α := (a : G) → G) (⇑(Homeomorph.mulLeft a) : (a : G) → G) fun (x : G) ↦ a * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
H :
  ∀ (x : G),
    Eq (α := G) ((Homeomorph.symm (Homeomorph.mulLeft a) : (a : G) → G) x : G)
      ((Homeomorph.mulLeft a⁻¹ : (a : G) → G) x : G)
⊢ Eq (α := G ≃ₜ G) (Homeomorph.symm (Homeomorph.mulLeft a)) (Homeomorph.mulLeft a⁻¹)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a x : G
⊢ Eq (α := G) ((Homeomorph.symm (Homeomorph.mulLeft a) : (a : G) → G) x : G)
    ((Homeomorph.mulLeft a⁻¹ : (a : G) → G) x : G)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ IsOpenMap (Y := G) fun (x : G) ↦ a * x

Tactic:
(Homeomorph.mulLeft a).isOpenMap

Premises used: Homeomorph.mulLeft, Homeomorph.isOpenMap
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
U : Set G
h : IsOpen[inst] U
x : G
⊢ IsOpen[inst] (x • U)

Tactic:
isOpenMap_mul_left x _ h

Premises used: isOpenMap_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
a : G
⊢ IsClosedMap (Y := G) fun (x : G) ↦ a * x

Tactic:
(Homeomorph.mulLeft a).isClosedMap

Premises used: Homeomorph.isClosedMap, Homeomorph.mulLeft
-- Module: Mathlib.Topology.Algebra.Group.Basic
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
U : Set G
h : IsClosed[inst] U
x : G
⊢ IsClosed[inst] (x • U)

Tactic:
isClosedMap_mul_left x _ h

Premises used: isClosedMap_mul_left