[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g✝ f g : M[Λ^ι]→L[R]N
h : toAlternatingMap f = toAlternatingMap g
⊢ ↑f = ↑g
[PROOFSTEP]
convert FunLike.ext'_iff.1 h
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : M ≃L[R] M'
f : M[Λ^ι]→L[R]N
⊢ (fun f => compContinuousLinearMap f ↑e) ((fun f => compContinuousLinearMap f ↑(ContinuousLinearEquiv.symm e)) f) = f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : M ≃L[R] M'
f : M[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑((fun f => compContinuousLinearMap f ↑e) ((fun f => compContinuousLinearMap f ↑(ContinuousLinearEquiv.symm e)) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : M ≃L[R] M'
f : M'[Λ^ι]→L[R]N
⊢ (fun f => compContinuousLinearMap f ↑(ContinuousLinearEquiv.symm e)) ((fun f => compContinuousLinearMap f ↑e) f) = f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : M ≃L[R] M'
f : M'[Λ^ι]→L[R]N
x✝ : ι → M'
⊢ ↑((fun f => compContinuousLinearMap f ↑(ContinuousLinearEquiv.symm e)) ((fun f => compContinuousLinearMap f ↑e) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : N ≃L[R] N'
f : M[Λ^ι]→L[R]N
⊢ ContinuousLinearMap.compContinuousAlternatingMap (↑(ContinuousLinearEquiv.symm e))
      (ContinuousLinearMap.compContinuousAlternatingMap (↑e) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : N ≃L[R] N'
f : M[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑(ContinuousLinearMap.compContinuousAlternatingMap (↑(ContinuousLinearEquiv.symm e))
          (ContinuousLinearMap.compContinuousAlternatingMap (↑e) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : N ≃L[R] N'
f : M[Λ^ι]→L[R]N'
⊢ ContinuousLinearMap.compContinuousAlternatingMap (↑e)
      (ContinuousLinearMap.compContinuousAlternatingMap (↑(ContinuousLinearEquiv.symm e)) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M'
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N
e : N ≃L[R] N'
f : M[Λ^ι]→L[R]N'
x✝ : ι → M
⊢ ↑(ContinuousLinearMap.compContinuousAlternatingMap (↑e)
          (ContinuousLinearMap.compContinuousAlternatingMap (↑(ContinuousLinearEquiv.symm e)) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp [(· ∘ ·)]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R M'
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : AddCommMonoid N✝
inst✝⁷ : Module R N✝
inst✝⁶ : TopologicalSpace N✝
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N✝
ι' : Type u_7
N : ι' → Type u_8
inst✝² : (i : ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι') → TopologicalSpace (N i)
inst✝ : (i : ι') → Module R (N i)
f : (i : ι') → M[Λ^ι]→L[R]N i
⊢ (fun f i => ContinuousLinearMap.compContinuousAlternatingMap (ContinuousLinearMap.proj i) f) (pi f) = f
[PROOFSTEP]
ext
[GOAL]
case h.H
R : Type u_1
M : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R M'
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : AddCommMonoid N✝
inst✝⁷ : Module R N✝
inst✝⁶ : TopologicalSpace N✝
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N✝
ι' : Type u_7
N : ι' → Type u_8
inst✝² : (i : ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι') → TopologicalSpace (N i)
inst✝ : (i : ι') → Module R (N i)
f : (i : ι') → M[Λ^ι]→L[R]N i
x✝¹ : ι'
x✝ : ι → M
⊢ ↑((fun f i => ContinuousLinearMap.compContinuousAlternatingMap (ContinuousLinearMap.proj i) f) (pi f) x✝¹) x✝ =
    ↑(f x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R M'
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : AddCommMonoid N✝
inst✝⁷ : Module R N✝
inst✝⁶ : TopologicalSpace N✝
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N✝
ι' : Type u_7
N : ι' → Type u_8
inst✝² : (i : ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι') → TopologicalSpace (N i)
inst✝ : (i : ι') → Module R (N i)
f : M[Λ^ι]→L[R]((i : ι') → N i)
⊢ pi ((fun f i => ContinuousLinearMap.compContinuousAlternatingMap (ContinuousLinearMap.proj i) f) f) = f
[PROOFSTEP]
ext
[GOAL]
case H.h
R : Type u_1
M : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : TopologicalSpace M
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R M'
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : AddCommMonoid N✝
inst✝⁷ : Module R N✝
inst✝⁶ : TopologicalSpace N✝
inst✝⁵ : AddCommMonoid N'
inst✝⁴ : Module R N'
inst✝³ : TopologicalSpace N'
n : ℕ
f✝ g : M[Λ^ι]→L[R]N✝
ι' : Type u_7
N : ι' → Type u_8
inst✝² : (i : ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι') → TopologicalSpace (N i)
inst✝ : (i : ι') → Module R (N i)
f : M[Λ^ι]→L[R]((i : ι') → N i)
x✝¹ : ι → M
x✝ : ι'
⊢ ↑(pi ((fun f i => ContinuousLinearMap.compContinuousAlternatingMap (ContinuousLinearMap.proj i) f) f)) x✝¹ x✝ =
    ↑f x✝¹ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M'[Λ^ι]→L[R]N
⊢ (fun g => compContinuousLinearMap g f) (g + g') =
    (fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g'
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
g g' : M'[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑((fun g => compContinuousLinearMap g f) (g + g')) x✝ =
    ↑((fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g') x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M'[Λ^ι]→L[R]N
⊢ AddHom.toFun
      { toFun := fun g => compContinuousLinearMap g f,
        map_add' :=
          (_ :
            ∀ (g g' : M'[Λ^ι]→L[R]N),
              (fun g => compContinuousLinearMap g f) (g + g') =
                (fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g') }
      (c • g) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun g => compContinuousLinearMap g f,
          map_add' :=
            (_ :
              ∀ (g g' : M'[Λ^ι]→L[R]N),
                (fun g => compContinuousLinearMap g f) (g + g') =
                  (fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g') }
        g
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : M →L[R] M'
c : R
g : M'[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑(AddHom.toFun
          { toFun := fun g => compContinuousLinearMap g f,
            map_add' :=
              (_ :
                ∀ (g g' : M'[Λ^ι]→L[R]N),
                  (fun g => compContinuousLinearMap g f) (g + g') =
                    (fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g') }
          (c • g))
      x✝ =
    ↑(↑(RingHom.id R) c •
          AddHom.toFun
            { toFun := fun g => compContinuousLinearMap g f,
              map_add' :=
                (_ :
                  ∀ (g g' : M'[Λ^ι]→L[R]N),
                    (fun g => compContinuousLinearMap g f) (g + g') =
                      (fun g => compContinuousLinearMap g f) g + (fun g => compContinuousLinearMap g f) g') }
            g)
      x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M[Λ^ι]→L[R]N
⊢ ContinuousLinearMap.compContinuousAlternatingMap f (g₁ + g₂) =
    ContinuousLinearMap.compContinuousAlternatingMap f g₁ + ContinuousLinearMap.compContinuousAlternatingMap f g₂
[PROOFSTEP]
ext1
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑(ContinuousLinearMap.compContinuousAlternatingMap f (g₁ + g₂)) x✝ =
    ↑(ContinuousLinearMap.compContinuousAlternatingMap f g₁ + ContinuousLinearMap.compContinuousAlternatingMap f g₂) x✝
[PROOFSTEP]
apply f.map_add
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M[Λ^ι]→L[R]N
⊢ ContinuousLinearMap.compContinuousAlternatingMap f (c • g) = c • ContinuousLinearMap.compContinuousAlternatingMap f g
[PROOFSTEP]
ext1
[GOAL]
case H
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
c : R
f : N →L[R] N'
g : M[Λ^ι]→L[R]N
x✝ : ι → M
⊢ ↑(ContinuousLinearMap.compContinuousAlternatingMap f (c • g)) x✝ =
    ↑(c • ContinuousLinearMap.compContinuousAlternatingMap f g) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f✝ g f : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
i j : ι
hv : v i = v j
hne : i ≠ j
⊢ MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v = 0
[PROOFSTEP]
simpa [MultilinearMap.alternatization_apply] using f.1.alternatization.map_eq_zero_of_eq' v i j hv hne
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g : ContinuousMultilinearMap R (fun x => M) N
⊢ (fun f =>
        { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
          map_eq_zero_of_eq' :=
            (_ :
              ∀ (v : ι → M) (i j : ι),
                v i = v j →
                  i ≠ j →
                    MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                      0) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g : ContinuousMultilinearMap R (fun x => M) N
x✝ : ι → M
⊢ ↑((fun f =>
            { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
              map_eq_zero_of_eq' :=
                (_ :
                  ∀ (v : ι → M) (i j : ι),
                    v i = v j →
                      i ≠ j →
                        MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap
                            v =
                          0) })
          0)
      x✝ =
    ↑0 x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g x✝¹ x✝ : ContinuousMultilinearMap R (fun x => M) N
⊢ ZeroHom.toFun
      {
        toFun := fun f =>
          { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
            map_eq_zero_of_eq' :=
              (_ :
                ∀ (v : ι → M) (i j : ι),
                  v i = v j →
                    i ≠ j →
                      MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap
                          v =
                        0) },
        map_zero' :=
          (_ :
            (fun f =>
                  { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                    map_eq_zero_of_eq' :=
                      (_ :
                        ∀ (v : ι → M) (i j : ι),
                          v i = v j →
                            i ≠ j →
                              MultilinearMap.toFun
                                  (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                0) })
                0 =
              0) }
      (x✝¹ + x✝) =
    ZeroHom.toFun
        {
          toFun := fun f =>
            { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
              map_eq_zero_of_eq' :=
                (_ :
                  ∀ (v : ι → M) (i j : ι),
                    v i = v j →
                      i ≠ j →
                        MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap
                            v =
                          0) },
          map_zero' :=
            (_ :
              (fun f =>
                    { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                      map_eq_zero_of_eq' :=
                        (_ :
                          ∀ (v : ι → M) (i j : ι),
                            v i = v j →
                              i ≠ j →
                                MultilinearMap.toFun
                                    (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                  0) })
                  0 =
                0) }
        x✝¹ +
      ZeroHom.toFun
        {
          toFun := fun f =>
            { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
              map_eq_zero_of_eq' :=
                (_ :
                  ∀ (v : ι → M) (i j : ι),
                    v i = v j →
                      i ≠ j →
                        MultilinearMap.toFun (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap
                            v =
                          0) },
          map_zero' :=
            (_ :
              (fun f =>
                    { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                      map_eq_zero_of_eq' :=
                        (_ :
                          ∀ (v : ι → M) (i j : ι),
                            v i = v j →
                              i ≠ j →
                                MultilinearMap.toFun
                                    (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                  0) })
                  0 =
                0) }
        x✝
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g x✝² x✝¹ : ContinuousMultilinearMap R (fun x => M) N
x✝ : ι → M
⊢ ↑(ZeroHom.toFun
          {
            toFun := fun f =>
              { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                map_eq_zero_of_eq' :=
                  (_ :
                    ∀ (v : ι → M) (i j : ι),
                      v i = v j →
                        i ≠ j →
                          MultilinearMap.toFun
                              (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                            0) },
            map_zero' :=
              (_ :
                (fun f =>
                      { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                        map_eq_zero_of_eq' :=
                          (_ :
                            ∀ (v : ι → M) (i j : ι),
                              v i = v j →
                                i ≠ j →
                                  MultilinearMap.toFun
                                      (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                    0) })
                    0 =
                  0) }
          (x✝² + x✝¹))
      x✝ =
    ↑(ZeroHom.toFun
            {
              toFun := fun f =>
                { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                  map_eq_zero_of_eq' :=
                    (_ :
                      ∀ (v : ι → M) (i j : ι),
                        v i = v j →
                          i ≠ j →
                            MultilinearMap.toFun
                                (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                              0) },
              map_zero' :=
                (_ :
                  (fun f =>
                        { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                          map_eq_zero_of_eq' :=
                            (_ :
                              ∀ (v : ι → M) (i j : ι),
                                v i = v j →
                                  i ≠ j →
                                    MultilinearMap.toFun
                                        (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                      0) })
                      0 =
                    0) }
            x✝² +
          ZeroHom.toFun
            {
              toFun := fun f =>
                { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                  map_eq_zero_of_eq' :=
                    (_ :
                      ∀ (v : ι → M) (i j : ι),
                        v i = v j →
                          i ≠ j →
                            MultilinearMap.toFun
                                (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                              0) },
              map_zero' :=
                (_ :
                  (fun f =>
                        { toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f,
                          map_eq_zero_of_eq' :=
                            (_ :
                              ∀ (v : ι → M) (i j : ι),
                                v i = v j →
                                  i ≠ j →
                                    MultilinearMap.toFun
                                        (∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • domDomCongr σ f).toMultilinearMap v =
                                      0) })
                      0 =
                    0) }
            x✝¹)
      x✝
[PROOFSTEP]
simp [Finset.sum_add_distrib]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
⊢ ↑(↑alternatization f) v = ∑ σ : Equiv.Perm ι, ↑Equiv.Perm.sign σ • ↑f (v ∘ ↑σ)
[PROOFSTEP]
simp [alternatization, (· ∘ ·)]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g : ContinuousMultilinearMap R (fun x => M) N
⊢ ContinuousAlternatingMap.toAlternatingMap (↑alternatization f) = ↑MultilinearMap.alternatization f.toMultilinearMap
[PROOFSTEP]
ext v
[GOAL]
case H
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : TopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f g : ContinuousMultilinearMap R (fun x => M) N
v : ι → M
⊢ ↑(ContinuousAlternatingMap.toAlternatingMap (↑alternatization f)) v =
    ↑(↑MultilinearMap.alternatization f.toMultilinearMap) v
[PROOFSTEP]
simp [alternatization_apply_apply, MultilinearMap.alternatization_apply, (· ∘ ·)]


[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
⊢ ↑1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
a✝ : X
⊢ ↑↑1 a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
x y : LocallyConstant X Y
⊢ OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : LocallyConstant X Y
inst✝¹ : Monoid Y
inst✝ : ContinuousMul Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y)) a✝ =
    ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x y : LocallyConstant X Y
⊢ ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑↑(x + y) a✝ = ↑(↑x + ↑y) a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
⊢ AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
      (x • y) =
    ↑(RingHom.id R) x •
      AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid Y
inst✝² : Module R Y
inst✝¹ : ContinuousAdd Y
inst✝ : ContinuousConstSMul R Y
x : R
y : LocallyConstant X Y
a✝ : X
⊢ ↑(AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
          (x • y))
      a✝ =
    ↑(↑(RingHom.id R) x •
          AddHom.toFun { toFun := toContinuousMap, map_add' := (_ : ∀ (x y : LocallyConstant X Y), ↑(x + y) = ↑x + ↑y) }
            y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
⊢ ↑1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
a✝ : X
⊢ ↑↑1 a✝ = ↑1 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
⊢ OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y)) a✝ =
    ↑(OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : LocallyConstant X Y),
                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
      0 =
    0
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
a✝ : X
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : LocallyConstant X Y),
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
          0)
      a✝ =
    ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : LocallyConstant X Y),
                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
      (x + y) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
        x +
      OneHom.toFun
        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
        y
[PROOFSTEP]
ext
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
x y : LocallyConstant X Y
a✝ : X
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : LocallyConstant X Y),
                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
          (x + y))
      a✝ =
    ↑(OneHom.toFun
            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
            x +
          OneHom.toFun
            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
            y)
      a✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (x y : LocallyConstant X Y),
                              OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : LocallyConstant X Y),
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : LocallyConstant X Y),
                                OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        x +
                      OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        y) })
      (↑(algebraMap R (LocallyConstant X Y)) r) =
    ↑(algebraMap R C(X, Y)) r
[PROOFSTEP]
ext x
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
f : LocallyConstant X Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
r : R
x : X
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  { toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x y : LocallyConstant X Y),
                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                            OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                              OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : LocallyConstant X Y),
                                  OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : LocallyConstant X Y),
                      OneHom.toFun
                          (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : LocallyConstant X Y),
                                    OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                          (x + y) =
                        OneHom.toFun
                            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : LocallyConstant X Y),
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                            x +
                          OneHom.toFun
                            (↑{ toOneHom := { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) },
                                map_mul' :=
                                  (_ :
                                    ∀ (x y : LocallyConstant X Y),
                                      OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } (x * y) =
                                        OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } x *
                                          OneHom.toFun { toFun := toContinuousMap, map_one' := (_ : ↑1 = 1) } y) })
                            y) })
          (↑(algebraMap R (LocallyConstant X Y)) r))
      x =
    ↑(↑(algebraMap R C(X, Y)) r) x
[PROOFSTEP]
simp [Algebra.smul_def]


[GOAL]
X : Type u_1
t : TopologicalSpace X
⊢ t = ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace
[PROOFSTEP]
rw [le_iInf_iff]
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x => x ∈ i) sierpinskiSpace
[PROOFSTEP]
exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
⊢ ⨅ (u : Opens X), induced (fun x => x ∈ u) sierpinskiSpace ≤ t
[PROOFSTEP]
intro u h
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
[PROOFSTEP]
rw [← generateFrom_iUnion_isOpen]
[GOAL]
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ IsOpen u
[PROOFSTEP]
apply isOpen_generateFrom_of_mem
[GOAL]
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ u ∈ ⋃ (i : Opens X), {s | IsOpen s}
[PROOFSTEP]
simp only [Set.mem_iUnion, Set.mem_setOf_eq, isOpen_induced_iff]
[GOAL]
case a.hs
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ ∃ i t_1, IsOpen t_1 ∧ (fun x => x ∈ i) ⁻¹' t_1 = u
[PROOFSTEP]
exact ⟨⟨u, h⟩, { True }, isOpen_singleton_true, by simp [Set.preimage]⟩
[GOAL]
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen u
⊢ (fun x => x ∈ { carrier := u, is_open' := h }) ⁻¹' {True} = u
[PROOFSTEP]
simp [Set.preimage]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ Inducing ↑(productOfMemOpens X)
[PROOFSTEP]
convert inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
[GOAL]
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ (i : Opens X), induced (fun x => x ∈ i) inferInstance
[PROOFSTEP]
apply eq_induced_by_maps_to_sierpinski
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
⊢ Function.Injective ↑(productOfMemOpens X)
[PROOFSTEP]
intro x1 x2 h
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ x1 = x2
[PROOFSTEP]
apply Inseparable.eq
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : ↑(productOfMemOpens X) x1 = ↑(productOfMemOpens X) x2
⊢ Inseparable x1 x2
[PROOFSTEP]
rw [← Inducing.inseparable_iff (productOfMemOpens_inducing X), h]