awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
f : A →A[R] A
n : ℕ
⊢ Eq (α := (a : A) → A) (⇑(f ^ n) : (a : A) → A) (⇑f : (a : A) → A)^[n]

Tactic:
hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Premises used: hom_coe_pow
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
f₁ : A →A[R] B
f₂ : A →A[R] C
⊢ (↑(f₁.prod f₂) : A →ₐ[R] B × C) = (↑f₁ : A →ₐ[R] B).prod (↑f₂ : A →ₐ[R] C)

Tactic:
rfl

Premises used: rfl, AlgHom.prod
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
f₁ : A →A[R] B
f₂ : A →A[R] C
x : A
⊢ Eq (α := B × C) ((f₁.prod f₂ : (a : A) → B × C) x : B × C) (((f₁ : (a : A) → B) x, (f₂ : (a : A) → C) x) : B × C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
F : Type u_5
D : Type u_6
inst_10 : UniformSpace D
inst_11 : CompleteSpace D
inst_12 : Semiring D
inst_13 : Algebra R D
inst_14 : T2Space B
inst_15 : FunLike F D B
inst_16 : AlgHomClass F R D B
inst_17 : ContinuousMapClass F D B
f g : F
⊢ CompleteSpace.{u_6} ↥(AlgHom.equalizer f g)

Tactic:
isClosed_eq (map_continuous f) (map_continuous g) |>.completeSpace_coe

Premises used: Set.Mem, setOf, IsClosed.completeSpace_coe
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Eq (α := A × B →ₐ[R] A) (↑(fst R A B) : A × B →ₐ[R] A) (AlgHom.fst R A B)

Tactic:
rfl

Premises used: rfl, AlgHom.fst
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Eq (α := (a : A × B) → A) (⇑(fst R A B) : (a : A × B) → A) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Eq (α := A × B →ₐ[R] B) (↑(snd R A B) : A × B →ₐ[R] B) (AlgHom.snd R A B)

Tactic:
rfl

Premises used: AlgHom.snd, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Eq (α := (a : A × B) → B) (⇑(snd R A B) : (a : A × B) → B) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
⊢ Eq (α := A × B →A[R] A × B) (ContinuousAlgHom.prod (fst R A B) (snd R A B)) (ContinuousAlgHom.id R (A × B))

Tactic:
ext fun ⟨_x, _y⟩ => rfl

Premises used: ContinuousAlgHom.snd, ContinuousAlgHom.prod, ContinuousAlgHom.ext, ContinuousAlgHom.id, ContinuousAlgHom.fst, _private.0.ContinuousAlgHom.fst_prod_snd.match_1, Prod, Eq, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
f : A →A[R] B
g : A →A[R] C
⊢ comp (fst R B C) (f.prod g) = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousAlgHom.ext, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
f : A →A[R] B
g : A →A[R] C
⊢ comp (snd R B C) (f.prod g) = g

Tactic:
ext fun _x => rfl

Premises used: ContinuousAlgHom.ext, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
D : Type u_6
inst_10 : Semiring D
inst_11 : TopologicalSpace D
inst_12 : Algebra R D
f₁ : A →A[R] B
f₂ : C →A[R] D
⊢ (↑(f₁.prodMap f₂) : A × C →ₐ[R] B × D) = (↑f₁ : A →ₐ[R] B).prodMap (↑f₂ : C →ₐ[R] D)

Tactic:
rfl

Premises used: AlgHom.prodMap, rfl, RingHom.prodMap, AlgHom.prod
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
C : Type u_4
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : TopologicalSpace C
D : Type u_6
inst_10 : Semiring D
inst_11 : TopologicalSpace D
inst_12 : Algebra R D
f₁ : A →A[R] B
f₂ : C →A[R] D
⊢ Eq (α := (a : A × C) → B × D) (⇑(f₁.prodMap f₂) : (a : A × C) → B × D)
    (Prod.map (⇑f₁ : (a : A) → B) (⇑f₂ : (a : C) → D))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
p : Subalgebra R B
h : ∀ (x : A), Membership.mem (α := B) p ((f : (a : A) → B) x : B)
⊢ (↑(f.codRestrict p h) : A →ₐ[R] ↥p) = (↑f : A →ₐ[R] B).codRestrict p h

Tactic:
rfl

Premises used: AlgHom.codRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
p : Subalgebra R B
h : ∀ (x : A), Membership.mem (α := B) p ((f : (a : A) → B) x : B)
x : A
⊢ Eq.{u_3 + 1} (α := B) ((↑((f.codRestrict p h : (a : A) → ↥p) x) : B) : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
B : Type u_3
inst_3 : Semiring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R A
inst_6 : Algebra R B
f : A →A[R] B
⊢ (↑f.rangeRestrict : A →ₐ[R] ↥(↑f : A →ₐ[R] B).range) = (↑f : A →ₐ[R] B).rangeRestrict

Tactic:
rfl

Premises used: AlgHom.codRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
p : Subalgebra R A
⊢ (↑p.valA : ↥p.toSubsemiring →+* A) = p.subtype

Tactic:
rfl

Premises used: Subsemiring.subtype, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
p : Subalgebra R A
⊢ Eq (α := (a : ↥p) → A) (⇑p.valA : (a : ↥p) → A) (⇑p.subtype : (a : ↥p.toSubsemiring) → A)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
p : Subalgebra R A
x : ↥p
⊢ (p.valA : (a : ↥p) → A) x = (↑x : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : TopologicalSpace A
inst_3 : Algebra R A
p : Subalgebra R A
⊢ (↑p.valA : ↥p →ₐ[R] A).range = p

Tactic:
Subalgebra.range_val p

Premises used: Subalgebra.val, Subalgebra.range_val
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : Ring S
inst_2 : TopologicalSpace S
inst_3 : Algebra R S
B : Type u_4
inst_4 : Ring B
inst_5 : TopologicalSpace B
inst_6 : Algebra R B
f : S →A[R] B
x : S
⊢ Eq.{u_4 + 1} (α := B) ((f : (a : S) → B) (-x) : B) (-(f : (a : S) → B) x : B)

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : Ring S
inst_2 : TopologicalSpace S
inst_3 : Algebra R S
B : Type u_4
inst_4 : Ring B
inst_5 : TopologicalSpace B
inst_6 : Algebra R B
f : S →A[R] B
x y : S
⊢ (f : (a : S) → B) (x - y) = HSub.hSub (α := B) (β := B) ((f : (a : S) → B) x : B) ((f : (a : S) → B) y : B)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
B : Type u_4
inst_3 : Ring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R B
inst_6 : Algebra S B
inst_7 : IsScalarTower R S B
C : Type u_5
inst_8 : Ring C
inst_9 : TopologicalSpace C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
f : B →A[S] C
⊢ Eq (α := B →ₐ[R] C) (↑(restrictScalars R f) : B →ₐ[R] C) (AlgHom.restrictScalars R (↑f : B →ₐ[S] C))

Tactic:
rfl

Premises used: AlgHom.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
B : Type u_4
inst_3 : Ring B
inst_4 : TopologicalSpace B
inst_5 : Algebra R B
inst_6 : Algebra S B
inst_7 : IsScalarTower R S B
C : Type u_5
inst_8 : Ring C
inst_9 : TopologicalSpace C
inst_10 : Algebra R C
inst_11 : Algebra S C
inst_12 : IsScalarTower R S C
f : B →A[S] C
⊢ Eq (α := (a : B) → C) (⇑(restrictScalars R f) : (a : B) → C) (⇑f : (a : B) → C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsTopologicalSemiring A
s : Subalgebra R A
⊢ IsTopologicalSemiring.{u} ↥s

Tactic:
s.toSubsemiring.topologicalSemiring

Premises used: Set.Mem, Subalgebra.toSubsemiring, Subsemiring.topologicalSemiring
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ IsSemitopologicalSemiring.{u} ↥s

Tactic:
s.toSubsemiring.semitopologicalSemiring

Premises used: Subsemiring.semitopologicalSemiring, Set.Mem, Subalgebra.toSubsemiring
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ s ≤ s.topologicalClosure

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed[inst_1] (closure[inst_1] (↑s : Set A))

Tactic:
@isClosed_closure A _ s

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed[inst_1] (↑s.topologicalClosure : Set A)

Tactic:
convert! @isClosed_closure A _ s

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s t : Subalgebra R A
h : s ≤ t
ht : IsClosed[inst_1] (↑t : Set A)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s t : Subalgebra R A
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
inst_5 : T2Space A
s : Set A
⊢ LE.le (α := Subalgebra R A) (topologicalClosure (adjoin R s)) (centralizer R (↑(centralizer R s) : Set A))

Tactic:
topologicalClosure_minimal (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

Premises used: Subalgebra.topologicalClosure_minimal, Algebra.adjoin_le_centralizer_centralizer, Set.isClosed_centralizer
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
h : (↑(comap f s.topologicalClosure) : Set B) = (↑(comap f s).topologicalClosure : Set B)
⊢ comap f s.topologicalClosure = (comap f s).topologicalClosure

Tactic:
apply SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
h :
  Eq.{u_2 + 1} (α := Set B) ((⇑f : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f : (a : B) → A) ⁻¹' (↑s : Set A)))
⊢ (↑(comap f s.topologicalClosure) : Set B) = closure[inst_5] (↑(comap f s) : Set B)

Tactic:
simp only [Subalgebra.coe_comap]

Premises used: Subalgebra.coe_comap
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
h :
  Eq.{u_2 + 1} (α := Set B) ((⇑f' : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f' : (a : B) → A) ⁻¹' (↑s : Set A)))
⊢ Eq.{u_2 + 1} (α := Set B) ((⇑f : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f : (a : B) → A) ⁻¹' (↑s : Set A)))

Tactic:
rw [w]
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
⊢ Eq.{u_2 + 1} (α := Set B) ((⇑f' : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f' : (a : B) → A) ⁻¹' (↑s : Set A)))

Tactic:
f'.preimage_closure _

Premises used: setOf, closure, Homeomorph.preimage_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
s : Subalgebra R A
B : Type u_2
inst_5 : TopologicalSpace B
inst_6 : Ring B
inst_7 : IsSemitopologicalRing B
inst_8 : Algebra R B
f : B →ₐ[R] A
f' : B ≃ₜ A
w : Eq (α := (a : B) → A) (⇑f : (a : B) → A) (⇑f' : (a : B) → A)
⊢ Eq.{u_2 + 1} (α := Set B) ((⇑f' : (a : B) → A) ⁻¹' (↑s.topologicalClosure : Set A))
    (closure[inst_5] ((⇑f' : (a : B) → A) ⁻¹' (↑s : Set A)))

Tactic:
exact f'.preimage_closure _

Premises used: Homeomorph.preimage_closure
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
x : A
⊢ Membership.mem (γ := Subalgebra R A) (elemental R x) x

Tactic:
le_topologicalClosure _ <| self_mem_adjoin_singleton R x

Premises used: Set.Mem, Subalgebra.le_topologicalClosure, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst_1] (↑s : Set A)
hx : x ∈ s
⊢ {x} ⊆ (↑s : Set A)

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
x : A
s : Subalgebra R A
hs : IsClosed[inst_1] (↑s : Set A)
⊢ elemental R x ≤ s ↔ x ∈ s

Tactic:
⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

Premises used: Algebra.elemental.self_mem, Iff.intro, Algebra.elemental.le_of_mem
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
x : A
⊢ IsClosed[inst_1] (↑(elemental R x) : Set A)

Tactic:
isClosed_topologicalClosure _

Premises used: Subalgebra.isClosed_topologicalClosure
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A_1 : Type u
inst_1 : TopologicalSpace A_1
inst_2 : Semiring A_1
inst_3 : Algebra R A_1
inst_4 : IsSemitopologicalSemiring A_1
A : Type u_2
inst_5 : UniformSpace A
inst_6 : CompleteSpace A
inst_7 : Semiring A
inst_8 : IsSemitopologicalSemiring A
inst_9 : Algebra R A
x : A
⊢ CompleteSpace.{u_2} ↥(elemental R x)

Tactic:
isClosed_closure.completeSpace_coe

Premises used: Set.Mem, setOf, closure, IsClosed.completeSpace_coe, Set.sInter
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
x : A
⊢ IsClosed[inst_1]
    (range (ι := ↥(elemental R x))
      (Subtype.val (p := fun (x_1 : A) ↦ Membership.mem (γ := Subalgebra R A) (elemental R x) x_1)))

Tactic:
simpa using isClosed R x

Premises used: Algebra.elemental.isClosed
-- Module: Mathlib.Topology.Algebra.Algebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u
inst_1 : TopologicalSpace A
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : IsSemitopologicalSemiring A
inst_5 : T2Space A
x : A
⊢ LE.le (α := Subalgebra R A) (elemental R x) (Subalgebra.centralizer R (↑(Subalgebra.centralizer R {x}) : Set A))

Tactic:
topologicalClosure_adjoin_le_centralizer_centralizer ..

Premises used: Set.Mem, Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizer
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
simp_rw :
  Eq.{u_3 + 1} (α := Filter P)
    (⨆ (i : V), map (fun (x : V) ↦ (x +ᵥ i) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (⨆ (p : P), map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
⊢ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v

Tactic:
simp_rw [asymptoticNhds, vadd_pure, map_iSup, map_map, Function.comp_def]

Premises used: Filter.map_iSup, Filter.map_map, Filter.vadd_pure, Function.comp_def, AffineSpace.asymptoticNhds
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
⊢ Eq.{u_3 + 1} (α := Filter P)
    (⨆ (i : V), map (fun (x : V) ↦ (x +ᵥ i) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (⨆ (p : P), map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))

Tactic:
(Equiv.vaddConst p).iSup_congr fun _ => ?_

Premises used: Equiv.vaddConst, Equiv.iSup_congr
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
refine :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := Filter P)
      (map (fun (x_1 : V) ↦ HVAdd.hVAdd (β := P) x_1 ((Equiv.vaddConst p : (a : V) → P) x : P))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
      (map (fun (x_1 : V) ↦ (x_1 +ᵥ x) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
⊢ Eq.{u_3 + 1} (α := Filter P)
    (⨆ (i : V), map (fun (x : V) ↦ (x +ᵥ i) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (⨆ (p : P), map (fun (x : V) ↦ x +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))

Tactic:
refine (Equiv.vaddConst p).iSup_congr fun _ => ?_

Premises used: Equiv.vaddConst, Equiv.iSup_congr
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
v : V
p : P
x : V
⊢ Eq.{u_3 + 1} (α := Filter P)
    (map (fun (x_1 : V) ↦ HVAdd.hVAdd (β := P) x_1 ((Equiv.vaddConst p : (a : V) → P) x : P))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))
    (map (fun (x_1 : V) ↦ (x_1 +ᵥ x) +ᵥ p) (HSMul.hSMul.{u_1, u_2, u_2} (α := Filter k) atTop (𝓝 v)))

Tactic:
simp [add_vadd]

Premises used: AddSemigroupAction.add_vadd
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
have : ∀ (p : P), u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v
⊢ u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
-- Module: Mathlib.Topology.Algebra.AsymptoticCone
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddTorsor V P
inst_5 : TopologicalSpace V
u v : V
p : P
nth_rw : u +ᵥ HVAdd.hVAdd (β := Filter P) (asymptoticNhds k V v) (pure p) = asymptoticNhds k P v
⊢ u +ᵥ asymptoticNhds k P v = asymptoticNhds k P v

Tactic:
nth_rw 1 [← asymptoticNhds_vadd_pure v p]

Premises used: AffineSpace.asymptoticNhds_vadd_pure