[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
⊢ ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
    (fun {U} f => ChartedSpace.LiftProp P f) f →
      (fun {U} f => ChartedSpace.LiftProp P f) fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
[PROOFSTEP]
intro U V i f h x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
⊢ ChartedSpace.LiftPropAt P (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) x
[PROOFSTEP]
have hUV : U ≤ V := CategoryTheory.leOfHom i
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)) x
[PROOFSTEP]
show ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x
[PROOFSTEP]
rw [← hG.liftPropAt_iff_comp_inclusion hUV]
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
U V : Opens ↑(TopCat.of M)
i : U ⟶ V
f : { x // x ∈ V } → M'
h : ChartedSpace.LiftProp P f
x : { x // x ∈ U }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (inclusion hUV x)
[PROOFSTEP]
apply h
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
⊢ ∀ {U : Opens ↑(TopCat.of M)} (f : { x // x ∈ U } → M'),
    (∀ (x : { x // x ∈ U }),
        ∃ V x i,
          TopCat.PrelocalPredicate.pred
            { pred := fun {U} f => ChartedSpace.LiftProp P f,
              res :=
                (_ :
                  ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                    ChartedSpace.LiftProp P f →
                      ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
            fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)) →
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        f
[PROOFSTEP]
intro V f h x
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
obtain ⟨U, hxU, i, hU : ChartedSpace.LiftProp P (f ∘ i)⟩ := h x
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
let x' : U := ⟨x, hxU⟩
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
have hUV : U ≤ V := CategoryTheory.leOfHom i
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
have : ChartedSpace.LiftPropAt P f (inclusion hUV x') :=
  by
  rw [hG.liftPropAt_iff_comp_inclusion hUV]
  exact hU x'
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P f (inclusion hUV x')
[PROOFSTEP]
rw [hG.liftPropAt_iff_comp_inclusion hUV]
[GOAL]
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
⊢ ChartedSpace.LiftPropAt P (f ∘ inclusion hUV) x'
[PROOFSTEP]
exact hU x'
[GOAL]
case intro.intro.intro
H : Type u_1
inst✝⁵ : TopologicalSpace H
H' : Type u_2
inst✝⁴ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
M : Type u
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
hG : LocalInvariantProp G G' P
V : Opens ↑(TopCat.of M)
f : { x // x ∈ V } → M'
h :
  ∀ (x : { x // x ∈ V }),
    ∃ V_1 x i,
      TopCat.PrelocalPredicate.pred
        { pred := fun {U} f => ChartedSpace.LiftProp P f,
          res :=
            (_ :
              ∀ {U V : Opens ↑(TopCat.of M)} (i : U ⟶ V) (f : { x // x ∈ V } → M'),
                ChartedSpace.LiftProp P f →
                  ∀ (x : { x // x ∈ U }), ChartedSpace.LiftPropAt P (f ∘ inclusion (_ : U ≤ V)) x) }
        fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) }) x)
x : { x // x ∈ V }
U : Opens ↑(TopCat.of M)
hxU : ↑x ∈ U
i : U ⟶ V
hU : ChartedSpace.LiftProp P (f ∘ fun x => { val := ↑x, property := (_ : ↑x ∈ ↑V) })
x' : { x // x ∈ U } := { val := ↑x, property := hxU }
hUV : U ≤ V
this : ChartedSpace.LiftPropAt P f (inclusion hUV x')
⊢ ChartedSpace.LiftPropAt P f x
[PROOFSTEP]
convert this
