[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y
[PROOFSTEP]
rw [← AlgHom.map_add]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
    ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R x + FreeAlgebra.ι R y)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel R Rel.add
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : M
⊢ AddHom.toFun
      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
        map_add' :=
          (_ :
            ∀ (x y : M),
              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
          map_add' :=
            (_ :
              ∀ (x y : M),
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
        x
[PROOFSTEP]
rw [← AlgHom.map_smul]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : M
⊢ AddHom.toFun
      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
        map_add' :=
          (_ :
            ∀ (x y : M),
              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
      (r • x) =
    ↑(RingQuot.mkAlgHom R (Rel R M)) (↑(RingHom.id R) r • FreeAlgebra.ι R x)
[PROOFSTEP]
exact RingQuot.mkAlgHom_rel R Rel.smul
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = ↑(ι R) m
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) =
    ↑{
          toAddHom :=
            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M),
                AddHom.toFun
                    { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                      map_add' :=
                        (_ :
                          ∀ (x y : M),
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                    (r • x) =
                  ↑(RingHom.id R) r •
                    AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      x) }
      m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
h : Rel R M x y
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y
[PROOFSTEP]
induction h
[GOAL]
case add
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
a✝ b✝ : M
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R (a✝ + b✝)) =
    ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R a✝ + FreeAlgebra.ι R b✝)
[PROOFSTEP]
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, map_mul, AlgHom.commutes,
  map_add]
[GOAL]
case smul
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x y : FreeAlgebra R M
r✝ : R
a✝ : M
⊢ ↑(↑(FreeAlgebra.lift R) ↑f) (FreeAlgebra.ι R (r✝ • a✝)) =
    ↑(↑(FreeAlgebra.lift R) ↑f) (↑(algebraMap R (FreeAlgebra R M)) r✝ * FreeAlgebra.ι R a✝)
[PROOFSTEP]
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, map_mul, AlgHom.commutes,
  map_add]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F => LinearMap.comp (AlgHom.toLinearMap F) (ι R))
      ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
          { val := ↑(FreeAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ (x y : FreeAlgebra R M),
                  Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ (fun F =>
        LinearMap.comp (AlgHom.toLinearMap F)
          {
            toAddHom :=
              { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                map_add' :=
                  (_ :
                    ∀ (x y : M),
                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M),
                  AddHom.toFun
                      { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                        map_add' :=
                          (_ :
                            ∀ (x y : M),
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                      (r • x) =
                    ↑(RingHom.id R) r •
                      AddHom.toFun
                        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                          map_add' :=
                            (_ :
                              ∀ (x y : M),
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                        x) })
      ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
          { val := ↑(FreeAlgebra.lift R) ↑f,
            property :=
              (_ :
                ∀ (x y : FreeAlgebra R M),
                  Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
        f) =
    f
[PROOFSTEP]
ext1 x
[GOAL]
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ↑((fun F =>
            LinearMap.comp (AlgHom.toLinearMap F)
              {
                toAddHom :=
                  { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                    map_add' :=
                      (_ :
                        ∀ (x y : M),
                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : M),
                      AddHom.toFun
                          { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                            map_add' :=
                              (_ :
                                ∀ (x y : M),
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                          (r • x) =
                        ↑(RingHom.id R) r •
                          AddHom.toFun
                            { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                              map_add' :=
                                (_ :
                                  ∀ (x y : M),
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                      (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                            x) })
          ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
              { val := ↑(FreeAlgebra.lift R) ↑f,
                property :=
                  (_ :
                    ∀ (x y : FreeAlgebra R M),
                      Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
            f))
      x =
    ↑f x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (↑(AlgHom.comp
            ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
                { val := ↑(FreeAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ (x y : FreeAlgebra R M),
                        Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
              ((fun F => LinearMap.comp (AlgHom.toLinearMap F) (ι R)) F))
            (RingQuot.mkAlgHom R (Rel R M))) ∘
        FreeAlgebra.ι R)
      x =
    (↑(AlgHom.comp F (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
[PROOFSTEP]
rw [ι]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : TensorAlgebra R M →ₐ[R] A
x : M
⊢ (↑(AlgHom.comp
            ((↑(RingQuot.liftAlgHom R) ∘ fun f =>
                { val := ↑(FreeAlgebra.lift R) ↑f,
                  property :=
                    (_ :
                      ∀ (x y : FreeAlgebra R M),
                        Rel R M x y → ↑(↑(FreeAlgebra.lift R) ↑f) x = ↑(↑(FreeAlgebra.lift R) ↑f) y) })
              ((fun F =>
                  LinearMap.comp (AlgHom.toLinearMap F)
                    {
                      toAddHom :=
                        { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                          map_add' :=
                            (_ :
                              ∀ (x y : M),
                                (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                  (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                    (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) },
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : M),
                            AddHom.toFun
                                { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : M),
                                        (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                                (r • x) =
                              ↑(RingHom.id R) r •
                                AddHom.toFun
                                  { toFun := fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m),
                                    map_add' :=
                                      (_ :
                                        ∀ (x y : M),
                                          (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) (x + y) =
                                            (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) x +
                                              (fun m => ↑(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m)) y) }
                                  x) })
                F))
            (RingQuot.mkAlgHom R (Rel R M))) ∘
        FreeAlgebra.ι R)
      x =
    (↑(AlgHom.comp F (RingQuot.mkAlgHom R (Rel R M))) ∘ FreeAlgebra.ι R) x
[PROOFSTEP]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply _ _)
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap (↑(lift R) f)) (ι R) = f
[PROOFSTEP]
convert (lift R).symm_apply_apply f
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ↑(↑(lift R) f) (↑(ι R) x) = ↑f x
[PROOFSTEP]
conv_rhs => rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
| ↑f x
[PROOFSTEP]
rw [← ι_comp_lift f]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ g = ↑(lift R) f
[PROOFSTEP]
rw [← (lift R).symm_apply_eq]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ LinearMap.comp (AlgHom.toLinearMap g) (ι R) = f ↔ ↑(lift R).symm g = f
[PROOFSTEP]
simp only [lift, Equiv.coe_fn_symm_mk]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (LinearMap.comp (AlgHom.toLinearMap g) (ι R)) = g
[PROOFSTEP]
rw [← lift_symm_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : TensorAlgebra R M →ₐ[R] A
⊢ ↑(lift R) (↑(lift R).symm g) = g
[PROOFSTEP]
exact (lift R).apply_symm_apply g
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : LinearMap.comp (AlgHom.toLinearMap f) (ι R) = LinearMap.comp (AlgHom.toLinearMap g) (ι R)
⊢ f = g
[PROOFSTEP]
rw [← lift_symm_apply, ← lift_symm_apply] at w
[GOAL]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : TensorAlgebra R M →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
[PROOFSTEP]
exact (lift R).symm.injective w
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
⊢ C a
[PROOFSTEP]
let s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := C
    mul_mem' := @h_mul
    add_mem' := @h_add
    algebraMap_mem' := h_grade0 }
    -- porting note: Added `h`. `h` is needed for `of`.
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
[PROOFSTEP]
let h : AddCommMonoid s := inferInstanceAs (AddCommMonoid (Subalgebra.toSubmodule s))
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
⊢ C a
[PROOFSTEP]
let of : M →ₗ[R] s := (ι R).codRestrict (Subalgebra.toSubmodule s) h_grade1
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
⊢ C a
[PROOFSTEP]
have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) :=
  by
  ext
  simp
  erw [LinearMap.codRestrict_apply]
    -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
⊢ AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M))) (ι R)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp (Subalgebra.val s) (↑(lift R) of))) (ι R)) x✝
[PROOFSTEP]
simp
[GOAL]
case w.h
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
x✝ : M
⊢ ↑(ι R) x✝ = ↑(↑(LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1) x✝)
[PROOFSTEP]
erw [LinearMap.codRestrict_apply]
  -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
of_id : AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C a
[PROOFSTEP]
rw [← AlgHom.id_apply (R := R) a, of_id]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (TensorAlgebra R M)) r)
h_grade1 : ∀ (x : M), C (↑(ι R) x)
h_mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
h_add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  {
    toSubsemiring :=
      { toSubmonoid := { toSubsemigroup := { carrier := C, mul_mem' := h_mul }, one_mem' := (_ : 1 ∈ C) },
        add_mem' := h_add, zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
h : AddCommMonoid { x // x ∈ s } := inferInstanceAs (AddCommMonoid { x // x ∈ ↑Subalgebra.toSubmodule s })
of : M →ₗ[R] { x // x ∈ s } := LinearMap.codRestrict (↑Subalgebra.toSubmodule s) (ι R) h_grade1
of_id : AlgHom.id R (TensorAlgebra R M) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C (↑(AlgHom.comp (Subalgebra.val s) (↑(lift R) of)) a)
[PROOFSTEP]
exact Subtype.prop (lift R of a)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (TensorAlgebra R M)) x) = x
[PROOFSTEP]
simp [algebraMapInv]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ TensorAlgebra R M →ₗ[R] M
[PROOFSTEP]
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ↑ιInv (↑(ι R) x) = x
[PROOFSTEP]
simp [ιInv, (AlgHom.toLinearMap_apply), toTrivSqZeroExt_ι _]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
⊢ ↑(ι R) x = 0 ↔ x = 0
[PROOFSTEP]
rw [← ι_inj R x 0, LinearMap.map_zero]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := lift_ι_apply _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
rw [h, AlgHom.commutes] at hf0
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
[GOAL]
case refine'_1
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
exact this.symm.imp_left Eq.symm
[GOAL]
case refine'_2
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (TensorAlgebra R M)) r
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ↑(ι R) 0 = ↑(algebraMap R (TensorAlgebra R M)) 0
[PROOFSTEP]
rw [LinearMap.map_zero, RingHom.map_zero]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ↑(ι R) x ≠ 1
[PROOFSTEP]
rw [← (algebraMap R (TensorAlgebra R M)).map_one, Ne.def, ι_eq_algebraMap_iff]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)
[PROOFSTEP]
exact one_ne_zero ∘ And.right
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Disjoint (LinearMap.range (ι R)) 1
[PROOFSTEP]
rw [Submodule.disjoint_def]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x : TensorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
[PROOFSTEP]
rintro _ ⟨x, hx⟩ ⟨r, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : ↑(ι R) x = ↑(Algebra.linearMap R (TensorAlgebra R M)) r
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
[PROOFSTEP]
rw [Algebra.linearMap_apply, ι_eq_algebraMap_iff] at hx
[GOAL]
case intro.intro
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(Algebra.linearMap R (TensorAlgebra R M)) r = 0
[PROOFSTEP]
rw [hx.2, map_zero]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ ↑toTensor (ι R m) = ↑(TensorAlgebra.ι R) m
[PROOFSTEP]
simp [toTensor]


[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
[PROOFSTEP]
let ⟨t, htx, htf⟩ := hf x
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
[PROOFSTEP]
refine ⟨t, htx, htf.preimage <| ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ InjOn (fun i => g i) ((fun i => g i) ⁻¹' {i | Set.Nonempty (f i ∩ t)})
[PROOFSTEP]
exact hg.mono fun i (hi : Set.Nonempty _) => hi.left
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
rcases hf a with ⟨U, haU, hfin⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a ≤ ⨆ (i : ι), 𝓝[f i] a
[PROOFSTEP]
calc
  𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
  _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by simp only [mem_setOf_eq, iUnion_nonempty_self]
  _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := (nhdsWithin_biUnion hfin _ _)
  _ ≤ ⨆ i, 𝓝[f i ∩ U] a := (iSup₂_le_iSup _ _)
  _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ <| inter_subset_left _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i] a = 𝓝[⋃ (i : ι), f i ∩ U] a
[PROOFSTEP]
rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : Set.Finite {i | Set.Nonempty (f i ∩ U)}
⊢ 𝓝[⋃ (i : ι), f i ∩ U] a = 𝓝[⋃ (i : ι) (_ : i ∈ {j | Set.Nonempty (f j ∩ U)}), f i ∩ U] a
[PROOFSTEP]
simp only [mem_setOf_eq, iUnion_nonempty_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ (i : ι), f i)
[PROOFSTEP]
rintro x -
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x
[PROOFSTEP]
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
by_cases hx : x ∈ closure (f i)
[GOAL]
case pos
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
exact hc i _ hx
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
[PROOFSTEP]
rw [hx]
[GOAL]
case neg
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))
[PROOFSTEP]
exact tendsto_bot
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
⊢ LocallyFinite fun i => closure (f i)
[PROOFSTEP]
intro x
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
[PROOFSTEP]
rcases hf x with ⟨s, hsx, hsf⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun i => closure (f i)) i ∩ t)}
[PROOFSTEP]
refine' ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => _⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : Set.Finite {i | Set.Nonempty (f i ∩ s)}
i : ι
hi : i ∈ {i | Set.Nonempty ((fun i => closure (f i)) i ∩ interior s)}
⊢ i ∈ {i | Set.Nonempty (f i ∩ s)}
[PROOFSTEP]
exact (hi.mono isOpen_interior.closure_inter).of_closure.mono (inter_subset_inter_right _ interior_subset)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
⊢ closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure (⋃ (i : ι), f i) ↔ x ∈ ⋃ (i : ι), closure (f i)
[PROOFSTEP]
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
⊢ IsClosed (⋃ (i : ι), f i)
[PROOFSTEP]
simp only [← closure_eq_iff_isClosed, hf.closure_iUnion, (hc _).closure_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ ⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ ∈ 𝓝 x
[PROOFSTEP]
refine' IsOpen.mem_nhds _ (mem_iInter₂.2 fun i => id)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ)
[PROOFSTEP]
suffices IsClosed (⋃ i : { i // x ∉ f i }, f i) by rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
this : IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
⊢ IsOpen (⋂ (i : ι) (_ : ¬x ∈ f i), (f i)ᶜ)
[PROOFSTEP]
rwa [← isOpen_compl_iff, compl_iUnion, iInter_subtype] at this
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
hf : LocallyFinite f
hc : ∀ (i : ι), IsClosed (f i)
x : X
⊢ IsClosed (⋃ (i : { i // ¬x ∈ f i }), f ↑i)
[PROOFSTEP]
exact (hf.comp_injective Subtype.val_injective).isClosed_iUnion fun i => hc _
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
choose U hUx hU using hf
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
choose N hN using fun x => (hU x).bddAbove
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X), N x ∈ upperBounds {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
replace hN : ∀ (x), ∀ n > N x, ∀ y ∈ U x, f (n + 1) y = f n y
[GOAL]
case hN
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X), N x ∈ upperBounds {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
⊢ ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
exact fun x n hn y hy => by_contra fun hne => hn.lt.not_le <| hN x ⟨y, hne, hy⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
replace hN : ∀ (x), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
[GOAL]
case hN
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n > N x → ∀ (y : X), y ∈ U x → f (n + 1) y = f n y
⊢ ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
exact fun x n hn y hy => Nat.le_induction rfl (fun k hle => (hN x _ hle _ hy).trans) n hn
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
⊢ ∃ F, ∀ (x : X), ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = F p.snd
[PROOFSTEP]
refine ⟨fun x => f (N x + 1) x, fun x => ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
⊢ ∀ᶠ (p : ℕ × X) in atTop ×ˢ 𝓝 x, f p.fst p.snd = (fun x => f (N x + 1) x) p.snd
[PROOFSTEP]
filter_upwards [Filter.prod_mem_prod (eventually_gt_atTop (N x)) (hUx x)]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
⊢ ∀ (a : ℕ × X), a ∈ {x_1 | N x < x_1} ×ˢ U x → f a.fst a.snd = f (N a.snd + 1) a.snd
[PROOFSTEP]
rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩
[GOAL]
case h.mk.intro
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty ((fun n => {x | f (n + 1) x ≠ f n x}) i ∩ U x)}
N : X → ℕ
hN : ∀ (x : X) (n : ℕ), n ≥ N x + 1 → ∀ (y : X), y ∈ U x → f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (n, y).fst (n, y).snd = f (N (n, y).snd + 1) (n, y).snd
[PROOFSTEP]
calc
  f n y = f (N x + 1) y := hN _ _ hn _ hy
  _ = f (max (N x + 1) (N y + 1)) y := (hN _ _ (le_max_left _ _) _ hy).symm
  _ = f (N y + 1) y := hN _ _ (le_max_right _ _) _ (mem_of_mem_nhds <| hUx y)
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ↑e)
⊢ LocallyFinite f
[PROOFSTEP]
simpa only [(· ∘ ·), e.apply_symm_apply] using h.comp_injective e.symm.injective
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : ι ⊕ ι' → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)
[PROOFSTEP]
simp only [locallyFinite_iff_smallSets, ← forall_and, ← finite_preimage_inl_and_inr, preimage_setOf_eq, (· ∘ ·),
  eventually_and]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)
[PROOFSTEP]
rw [← (Equiv.optionEquivSumPUnit.{_, 0} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)
[PROOFSTEP]
simp only [locallyFinite_of_finite, and_true]
[GOAL]
ι : Type u_1
ι' : Type u_2
α : Type u_3
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
[PROOFSTEP]
rfl


[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
⊢ IsLocallyHomeomorphOn f s
[PROOFSTEP]
intro x hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
[PROOFSTEP]
obtain ⟨e, hx, he⟩ := h x hx
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
⊢ ∃ e, x ∈ e.source ∧ f = ↑e
[PROOFSTEP]
exact
  ⟨{ e with
      toFun := f
      map_source' := fun x hx => by rw [he x hx]; exact e.map_source' hx
      left_inv' := fun x hx => by rw [he x hx]; exact e.left_inv' hx
      right_inv' := fun y hy => by rw [he _ (e.map_target' hy)]; exact e.right_inv' hy
      continuous_toFun := (continuousOn_congr he).mpr e.continuous_toFun },
    hx, rfl⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ f x ∈ e.target
[PROOFSTEP]
rw [he x hx]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ ↑e x ∈ e.target
[PROOFSTEP]
exact e.map_source' hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ LocalEquiv.invFun e.toLocalEquiv (f x) = x
[PROOFSTEP]
rw [he x hx]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x✝ : X
hx✝¹ : x✝ ∈ s
e : LocalHomeomorph X Y
hx✝ : x✝ ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx : x ∈ e.source
⊢ LocalEquiv.invFun e.toLocalEquiv (↑e x) = x
[PROOFSTEP]
exact e.left_inv' hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
y : Y
hy : y ∈ e.target
⊢ f (LocalEquiv.invFun e.toLocalEquiv y) = y
[PROOFSTEP]
rw [he _ (e.map_target' hy)]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
h : ∀ (x : X), x ∈ s → ∃ e, x ∈ e.source ∧ ∀ (y : X), y ∈ e.source → f y = ↑e y
x : X
hx✝ : x ∈ s
e : LocalHomeomorph X Y
hx : x ∈ e.source
he : ∀ (y : X), y ∈ e.source → f y = ↑e y
y : Y
hy : y ∈ e.target
⊢ ↑e (LocalEquiv.invFun e.toLocalEquiv y) = y
[PROOFSTEP]
exact e.right_inv' hy
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocallyHomeomorphOn g t
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
⊢ IsLocallyHomeomorphOn (g ∘ f) s
[PROOFSTEP]
intro x hx
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
hg : IsLocallyHomeomorphOn g t
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
⊢ ∃ e, x ∈ e.source ∧ g ∘ f = ↑e
[PROOFSTEP]
obtain ⟨eg, hxg, rfl⟩ := hg (f x) (h hx)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
t : Set Y
hf : IsLocallyHomeomorphOn f s
h : Set.MapsTo f s t
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hxg : f x ∈ eg.source
hg : IsLocallyHomeomorphOn (↑eg) t
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ f = ↑e
[PROOFSTEP]
obtain ⟨ef, hxf, rfl⟩ := hf x hx
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
s : Set X
t : Set Y
x : X
hx : x ∈ s
eg : LocalHomeomorph Y Z
hg : IsLocallyHomeomorphOn (↑eg) t
ef : LocalHomeomorph X Y
hxf : x ∈ ef.source
hf : IsLocallyHomeomorphOn (↑ef) s
h : Set.MapsTo (↑ef) s t
hxg : ↑ef x ∈ eg.source
⊢ ∃ e, x ∈ e.source ∧ ↑eg ∘ ↑ef = ↑e
[PROOFSTEP]
exact ⟨ef.trans eg, ⟨hxf, hxg⟩, rfl⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
t : Set Y
⊢ IsLocallyHomeomorph f ↔ IsLocallyHomeomorphOn f Set.univ
[PROOFSTEP]
simp only [IsLocallyHomeomorph, IsLocallyHomeomorphOn, Set.mem_univ, forall_true_left]


[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → Set.Finite (f ⁻¹' K)
[PROOFSTEP]
rw [hasBasis_cocompact.tendsto_right_iff]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → Set.Finite (f ⁻¹' K)
[PROOFSTEP]
refine' forall₂_congr (fun K _ ↦ _)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ Set.Finite (f ⁻¹' K)
[PROOFSTEP]
simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
⊢ DiscreteTopology X
[PROOFSTEP]
refine' singletons_open_iff_discrete.mp (fun x ↦ _)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen {x}
[PROOFSTEP]
obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen {x}
[PROOFSTEP]
obtain ⟨U : Set Y, hU₁ : U ⊆ K, hU₂ : IsOpen U, hU₃ : f x ∈ U⟩ := mem_nhds_iff.mp hK'
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
⊢ IsOpen {x}
[PROOFSTEP]
have hU₄ : Set.Finite (f ⁻¹' U) := Finite.subset (tendsto_cofinite_cocompact_iff.mp hf K hK) (preimage_mono hU₁)
[GOAL]
case intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : LocallyCompactSpace Y
hf' : Continuous f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
U : Set Y
hU₁ : U ⊆ K
hU₂ : IsOpen U
hU₃ : f x ∈ U
hU₄ : Set.Finite (f ⁻¹' U)
⊢ IsOpen {x}
[PROOFSTEP]
exact isOpen_singleton_of_finite_mem_nhds _ ((hU₂.preimage hf').mem_nhds hU₃) hU₄
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ Tendsto f cofinite (cocompact Y)
[PROOFSTEP]
convert hf
[GOAL]
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : Tendsto f (cocompact X) (cocompact Y)
⊢ cofinite = cocompact X
[PROOFSTEP]
rw [cocompact_eq_cofinite X]