awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
h : mkCLM K E ∘SL outCLM K E ∘SL f = f
⊢ ∃ (a : F →SL[σ] E), mkCLM K E ∘SL a = f

Tactic:
use (outCLM K E).comp f

Premises used: ContinuousLinearMap.comp, SeparationQuotient.outCLM
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
L : Type u_3
inst_6 : Semiring L
σ : L →+* K
F : Type u_4
inst_7 : AddCommMonoid F
inst_8 : Module L F
inst_9 : TopologicalSpace F
f : ContinuousLinearMap.{u_3, u_1, u_4, u_2} σ F (SeparationQuotient E)
h : (mkCLM K E ∘SL outCLM K E) ∘SL f = f
h₁ : ContinuousLinearMap.id K (SeparationQuotient E) ∘SL f = f
h₂ h₃ : f = f
⊢ mkCLM K E ∘SL outCLM K E ∘SL f = f

Tactic:
rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp]

Premises used: SeparationQuotient.mkCLM_comp_outCLM, ContinuousLinearMap.comp_assoc, ContinuousLinearMap.id_comp
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ IsEmbedding (X := SeparationQuotient E) (Y := E)
    (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)

Tactic:
Function.LeftInverse.isEmbedding (mk_outCLM K) continuous_mk (map_continuous _)

Premises used: SeparationQuotient.continuous_mk, SeparationQuotient.mk_outCLM, ContinuousMapClass.map_continuous, Function.LeftInverse.isEmbedding
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ Function.Injective (α := SeparationQuotient E) (β := E)
    (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)

Tactic:
(isEmbedding_outCLM K E).injective

Premises used: Topology.IsEmbedding.injective, SeparationQuotient.isEmbedding_outCLM
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul K E
rw : IsUniformInducing.{u_2, u_2} (α := SeparationQuotient E) id
⊢ IsUniformInducing (α := SeparationQuotient E) (β := E)
    (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)

Tactic:
rw [← isUniformInducing_mk.of_comp_iff, mk_comp_outCLM]

Premises used: SeparationQuotient.isUniformInducing_mk, IsUniformInducing.of_comp_iff, SeparationQuotient.mk_comp_outCLM
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ IsUniformInducing.{u_2, u_2} (α := SeparationQuotient E) id

Tactic:
.id

Premises used: IsUniformInducing.id
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ IsUniformInducing.{u_2, u_2} (α := SeparationQuotient E) id

Tactic:
exact .id
-- Module: Mathlib.Topology.Algebra.SeparationQuotient.Section
Goal:
K : Type u_1
E : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul K E
⊢ UniformContinuous (α := SeparationQuotient E) (β := E)
    (⇑(outCLM K E : SeparationQuotient E →L[K] E) : (a : SeparationQuotient E) → E)

Tactic:
(outCLM_isUniformInducing K E).uniformContinuous

Premises used: IsUniformInducing.uniformContinuous, SeparationQuotient.outCLM_isUniformInducing
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
f : WithConv (E →L[R] F)
x : E
⊢ Eq.{u_3 + 1} (α := F) (((star f).ofConv : (a : E) → F) x : F) (star ((f.ofConv : (a : E) → F) (star x)) : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
f : WithConv (E →L[R] F)
⊢ (↑(star f).ofConv : E →ₗ[R] F) = (star (toConv (↑f.ofConv : E →ₗ[R] F))).ofConv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
f : WithConv (E →L[R] F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)

Tactic:
simp [IsSelfAdjoint, WithConv.ext_iff, ContinuousLinearMap.ext_iff, star_eq_iff_star_eq,
    eq_comm (a := f _)]

Premises used: IsSelfAdjoint, eq_comm, star_eq_iff_star_eq, ContinuousLinearMap.ext_iff, WithConv.ext_iff
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
f : WithConv (E →L[R] F)
⊢ IsSelfAdjoint (toConv (↑f.ofConv : E →ₗ[R] F)) ↔ IsSelfAdjoint f

Tactic:
simp [isSelfAdjoint_iff_map_star, LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star]

Premises used: ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
x : WithConv (E →L[R] F)
h :
  ∀ (x_1 : E), Eq.{u_3 + 1} (α := F) (((star (star x)).ofConv : (a : E) → F) x_1 : F) ((x.ofConv : (a : E) → F) x_1 : F)
⊢ star (star x) = x

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
x : WithConv (E →L[R] F)
x_1 : E
⊢ Eq.{u_3 + 1} (α := F) (((star (star x)).ofConv : (a : E) → F) x_1 : F) ((x.ofConv : (a : E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : ContinuousAdd F
x y : WithConv (E →L[R] F)
h :
  ∀ (x_1 : E),
    Eq.{u_3 + 1} (α := F) (((star (x + y)).ofConv : (a : E) → F) x_1 : F)
      (((star x + star y).ofConv : (a : E) → F) x_1 : F)
⊢ star (x + y) = star x + star y

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : ContinuousAdd F
x y : WithConv (E →L[R] F)
x_1 : E
⊢ Eq.{u_3 + 1} (α := F) (((star (x + y)).ofConv : (a : E) → F) x_1 : F)
    (((star x + star y).ofConv : (a : E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
h :
  ∀ (x : G),
    Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘SL g.ofConv))).ofConv : (a : G) → F) x : F)
      (((toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv : (a : G) → F) x : F)
⊢ star (toConv (f.ofConv ∘SL g.ofConv)) = toConv ((star f).ofConv ∘SL (star g).ofConv)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
x : G
⊢ Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘SL g.ofConv))).ofConv : (a : G) → F) x : F)
    (((toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv : (a : G) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
h :
  ∀ (x : G),
    Eq.{u_3 + 1} (α := F) (((star (toConv (f ∘SL g))).ofConv : (a : G) → F) x : F)
      (((toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv : (a : G) → F) x : F)
⊢ star (toConv (f ∘SL g)) = toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
G : Type u_4
inst_14 : AddCommMonoid G
inst_15 : Module R G
inst_16 : StarAddMonoid G
inst_17 : StarModule R G
inst_18 : TopologicalSpace G
inst_19 : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
x : G
⊢ Eq.{u_3 + 1} (α := F) (((star (toConv (f ∘SL g))).ofConv : (a : G) → F) x : F)
    (((toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv : (a : G) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : TopologicalSpace E
inst_7 : ContinuousStar E
h :
  ∀ (x : E),
    Eq (α := E) ((ofConv (star (toConv (ContinuousLinearMap.id R E))) : (a : E) → E) x : E)
      ((ofConv (toConv (ContinuousLinearMap.id R E)) : (a : E) → E) x : E)
⊢ Eq (α := WithConv (E →L[R] E)) (star (toConv (ContinuousLinearMap.id R E))) (toConv (ContinuousLinearMap.id R E))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : TopologicalSpace E
inst_7 : ContinuousStar E
x : E
⊢ Eq (α := E) ((ofConv (star (toConv (ContinuousLinearMap.id R E))) : (a : E) → E) x : E)
    ((ofConv (toConv (ContinuousLinearMap.id R E)) : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
h :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv 0)) : (a : E) → F) x : F) ((ofConv (toConv 0) : (a : E) → F) x : F)
⊢ Eq (α := WithConv (E →L[R] F)) (star (toConv 0)) (toConv 0)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
x : E
⊢ Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv 0)) : (a : E) → F) x : F) ((ofConv (toConv 0) : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : TopologicalSpace E
inst_3 : ContinuousStar E
S : Type u_4
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : TopologicalSpace S
inst_10 : ContinuousStar S
inst_11 : ContinuousSMul S E
a : E
h :
  Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S a))) : (a : S) → E) 1 : E)
    ((ofConv (toConv (toSpanSingleton S (star a))) : (a : S) → E) 1 : E)
⊢ Eq (α := WithConv (S →L[S] E)) (star (toConv (toSpanSingleton S a))) (toConv (toSpanSingleton S (star a)))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
E : Type u_2
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : TopologicalSpace E
inst_3 : ContinuousStar E
S : Type u_4
inst_4 : Semiring S
inst_5 : StarAddMonoid S
inst_6 : StarModule S S
inst_7 : Module S E
inst_8 : StarModule S E
inst_9 : TopologicalSpace S
inst_10 : ContinuousStar S
inst_11 : ContinuousSMul S E
a : E
⊢ Eq.{u_2 + 1} (α := E) ((ofConv (star (toConv (toSpanSingleton S a))) : (a : S) → E) 1 : E)
    ((ofConv (toConv (toSpanSingleton S (star a))) : (a : S) → E) 1 : E)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
inst_6 : ContinuousStar E
inst_7 : ContinuousStar F
S : Type u_4
inst_8 : Semiring S
inst_9 : StarAddMonoid S
inst_10 : StarModule S S
inst_11 : Module S E
inst_12 : StarModule S E
inst_13 : TopologicalSpace S
inst_14 : ContinuousStar S
inst_15 : Module S F
inst_16 : StarModule S F
inst_17 : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
h :
  ∀ (x_1 : E),
    Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
      ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)
⊢ Eq (α := WithConv (E →L[S] F)) (star (toConv (f.ofConv.smulRight x))) (toConv ((star f).ofConv.smulRight (star x)))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
inst_6 : ContinuousStar E
inst_7 : ContinuousStar F
S : Type u_4
inst_8 : Semiring S
inst_9 : StarAddMonoid S
inst_10 : StarModule S S
inst_11 : Module S E
inst_12 : StarModule S E
inst_13 : TopologicalSpace S
inst_14 : ContinuousStar S
inst_15 : Module S F
inst_16 : StarModule S F
inst_17 : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((ofConv (star (toConv (f.ofConv.smulRight x))) : (a : E) → F) x_1 : F)
    ((ofConv (toConv ((star f).ofConv.smulRight (star x))) : (a : E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : SMulCommClass R R F
inst_15 : ContinuousConstSMul R F
x : R
x_1 : WithConv (E →L[R] F)
h :
  ∀ (x_2 : E),
    Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
      (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)
⊢ star (x • x_1) = star x • star x_1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
inst_10 : TopologicalSpace E
inst_11 : TopologicalSpace F
inst_12 : ContinuousStar E
inst_13 : ContinuousStar F
inst_14 : SMulCommClass R R F
inst_15 : ContinuousConstSMul R F
x : R
x_1 : WithConv (E →L[R] F)
x_2 : E
⊢ Eq.{u_3 + 1} (α := F) (((star (x • x_1)).ofConv : (a : E) → F) x_2 : F)
    (((star x • star x_1).ofConv : (a : E) → F) x_2 : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Star.LinearMap
Goal:
E : Type u_2
F : Type u_3
inst : AddCommMonoid E
inst_1 : StarAddMonoid E
inst_2 : AddCommMonoid F
inst_3 : StarAddMonoid F
inst_4 : TopologicalSpace E
inst_5 : TopologicalSpace F
inst_6 : ContinuousStar E
inst_7 : ContinuousStar F
R : Type u_4
inst_8 : CommSemiring R
inst_9 : StarRing R
inst_10 : Module R E
inst_11 : StarModule R E
inst_12 : Module R F
inst_13 : StarModule R F
f : WithConv (E →L[R] F)
⊢ star f = toConv ((↑(starL R) : F →L⋆[R] F) ∘SL f.ofConv ∘SL (↑(starL R) : E →L⋆[R] E))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Star.Real
Goal:
⊢ ContinuousStar ℝ

Tactic:
⟨continuous_id⟩

Premises used: ContinuousStar.mk, continuous_id
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
h : ∀ (u : R), u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ (↑(unitary R) : Set R)
⊢ f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)

Tactic:
ext u
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
u : R
⊢ u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ (↑(unitary R) : Set R)

Tactic:
simp [f, Unitary.mem_iff]

Premises used: Unitary.mem_iff
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
⊢ f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)

Tactic:
have hf : f ⁻¹' {(1, 1)} = unitary R := by ext u; simp [f, Unitary.mem_iff]
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
rw : IsClosed (f ⁻¹' {(1, 1)})
⊢ IsClosed (↑(unitary R) : Set R)

Tactic:
rw [← hf]
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
⊢ Continuous f

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
inst_2 : TopologicalSpace R
inst_3 : T1Space R
inst_4 : ContinuousStar R
inst_5 : ContinuousMul R
f : (u : R) → R × R := fun (u : R) ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = (↑(unitary R) : Set R)
⊢ IsClosed (f ⁻¹' {(1, 1)})

Tactic:
exact isClosed_singleton.preimage (by fun_prop)

Premises used: IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
s : Set R
⊢ ContinuousOn star s

Tactic:
continuous_star.continuousOn

Premises used: Continuous.continuousOn, ContinuousStar.continuous_star
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
s : Set R
x : R
⊢ ContinuousWithinAt star s x

Tactic:
continuous_star.continuousWithinAt

Premises used: ContinuousStar.continuous_star, Continuous.continuousWithinAt
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
x : R
⊢ ContinuousAt star x

Tactic:
continuous_star.continuousAt

Premises used: ContinuousStar.continuous_star, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Star
Goal:
R : Type u_2
inst : TopologicalSpace R
inst_1 : Star R
inst_2 : ContinuousStar R
a : R
⊢ Tendsto star (𝓝 a) (𝓝 (star a))

Tactic:
continuousAt_star

Premises used: ContinuousAt, continuousAt_star