mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₃ : y = val
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ x :: xs

Tactic:
;

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₃ : y = val
h₀ : (x :: xs).Nodup
h₁ : (x :: xs).length = (y :: ys).length
⊢ val ∈ y :: ys ↔ x ∈ x :: xs
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?

Tactic:
;

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = ys[i]?

Tactic:
;

Goal state after:
case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = ys[i]?
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))

Tactic:
;

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Tactic:
;

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case mk
G : GrpCat
H : FiniteIndexNormalSubgroup ↑G
x✝ : ↑(FiniteGrp.of (↑G ⧸ H.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x) =
    (ConcreteCategory.hom (𝟙 (FiniteGrp.of (↑G ⧸ H.toSubgroup)))) (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x)

Tactic:
;

Goal state after:
case mk
G : GrpCat
H : FiniteIndexNormalSubgroup ↑G
x✝ : ↑(FiniteGrp.of (↑G ⧸ H.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x) =
    (ConcreteCategory.hom (𝟙 (FiniteGrp.of (↑G ⧸ H.toSubgroup)))) (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x)
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case mk
G : GrpCat
X✝ Y✝ Z✝ : FiniteIndexNormalSubgroup ↑G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(FiniteGrp.of (↑G ⧸ X✝.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x) =
    (ConcreteCategory.hom
        (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Y✝.toSubgroup (MonoidHom.id ↑G) ⋯) ≫
          FiniteGrp.ofHom (QuotientGroup.map Y✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x)

Tactic:
;

Goal state after:
case mk
G : GrpCat
X✝ Y✝ Z✝ : FiniteIndexNormalSubgroup ↑G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(FiniteGrp.of (↑G ⧸ X✝.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x) =
    (ConcreteCategory.hom
        (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Y✝.toSubgroup (MonoidHom.id ↑G) ⋯) ≫
          FiniteGrp.ofHom (QuotientGroup.map Y✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (⨅ i ∈ 𝔖,
        comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
          (𝓝 ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f)))) ↔
    Tendsto F ℱ (⨅ i ∈ 𝔖, comap i.domRestrict (𝓝 (i.domRestrict f)))

Tactic:
tendsto_iInf,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
⊢ (∀ i ∈ 𝔖,
      Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
        (comap (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
          (𝓝 ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))))) ↔
    ∀ i ∈ 𝔖, Tendsto F ℱ (comap i.domRestrict (𝓝 (i.domRestrict f)))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : completion G ⟶ P
⊢ eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        ((fun f ↦ lift f) ((fun f ↦ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f) f)) =
    eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f

Tactic:
;

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : completion G ⟶ P
⊢ eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        ((fun f ↦ lift f) ((fun f ↦ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f) f)) =
    eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
x✝ : M
⊢ (0 ⋆[L] f) x✝ = 0 x✝

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E'
x✝ : M
⊢ (0 ⋆[L] f) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E
x✝ : M
⊢ (f ⋆[L] 0) x✝ = 0 x✝

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝⁸ : Monoid M
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid E'
inst✝⁴ : AddCommMonoid F
inst✝³ : Module S E
inst✝² : Module S E'
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] E' →ₗ[S] F
f : M → E
x✝ : M
⊢ (f ⋆[L] 0) x✝ = 0 x✝
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (({1}.indicator fun x ↦ e) ⋆[L] f) x = f x

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : E →ₗ[S] F →ₗ[S] F
e : E
f : M → F
hL : ∀ (y : F), (L e) y = y
x : M
⊢ (({1}.indicator fun x ↦ e) ⋆[L] f) x = f x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (f ⋆[L] {1}.indicator fun x ↦ e) x = f x

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst✝⁶ : Monoid M
inst✝⁵ : CommSemiring S
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid F
inst✝² : Module S E
inst✝¹ : Module S F
inst✝ : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (L y) e = y
x : M
⊢ (f ⋆[L] {1}.indicator fun x ↦ e) x = f x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
x : M
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
x : M
⊢ ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
⊢ (fun x ↦ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)) = fun x ↦
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
;

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
⊢ (fun x ↦ ∑' (ab : ↑(mulFiber x)), (L (f (↑ab).1)) (g (↑ab).2)) = fun x ↦
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: case e_f
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ (fun c ↦ (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2)) = fun ab ↦
    (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
;

Goal state after:
case e_f
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ (fun c ↦ (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2)) = fun ab ↦
    (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: case e_f
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x a b : M
property✝ : (a, b) ∈ mulFiber x
⊢ (L (f (↑((mulFiber_swapEquiv x) ⟨(a, b), property✝⟩)).1)) (g (↑((mulFiber_swapEquiv x) ⟨(a, b), property✝⟩)).2) =
    (L (g (↑⟨(a, b), property✝⟩).1)) (f (↑⟨(a, b), property✝⟩).2)

Tactic:
;

Goal state after:
case e_f
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x a b : M
property✝ : (a, b) ∈ mulFiber x
⊢ (L (f (↑((mulFiber_swapEquiv x) ⟨(a, b), property✝⟩)).1)) (g (↑((mulFiber_swapEquiv x) ⟨(a, b), property✝⟩)).2) =
    (L (g (↑⟨(a, b), property✝⟩).1)) (f (↑⟨(a, b), property✝⟩).2)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² + x✝¹), cont := ⋯ } x✝ =
    ({ toLinearMap := B.flip x✝², cont := ⋯ } + { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
;

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² + x✝¹), cont := ⋯ } x✝ =
    ({ toLinearMap := B.flip x✝², cont := ⋯ } + { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² : 𝕜
x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² • x✝¹), cont := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
;

Goal state after:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² : 𝕜
x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² • x✝¹), cont := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
u : R
⊢ u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ ↑(unitary R)

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
u : R
⊢ u ∈ f ⁻¹' {(1, 1)} ↔ u ∈ ↑(unitary R)
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
⊢ IsClosed ↑(unitary R)

Tactic:
by
  let f (u : R) : R × R := (star u * u, u * star u)
  have hf : f ⁻¹' {(1, 1)} = unitary R := by ext u; simp [f, Unitary.mem_iff]
  rw [← hf]
  exact isClosed_singleton.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
x✝ : G
⊢ (star (toConv (f.ofConv ∘SL g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
x✝ : G
⊢ (star (toConv (f.ofConv ∘SL g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
x✝ : G
⊢ (star (toConv (f ∘SL g))).ofConv x✝ = (toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv x✝

Tactic:
;

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
x✝ : G
⊢ (star (toConv (f ∘SL g))).ofConv x✝ = (toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv x✝