awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
x : (↑(TopCat.of M) : Type u)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι
        ((OpenNhds.inclusion x).op ⋙
          ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))) (smoothSheaf IM I M N))
        U ≫
      evalHom IM I N x =
    ↾evalAt IM I N x (unop U)

Tactic:
colimit.ι_desc _ _

Premises used: TopCat.subpresheafToTypes, Set.Mem, smoothSheaf.evalAt, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
x : M
w :
  ∀ (t : N),
    ∃ (U : OpenNhds (X := TopCat.of M) x) (f : (y : ↥(↑U : Opens (↑(TopCat.of M) : Type u))) → N) (_ :
      TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
        (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
          (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM I ∞) M N ⋯))
        f),
      f (Subtype.mk (p := fun (x_2 : (↑(TopCat.of M) : Type u)) ↦ x_2 ∈ (↑U : Opens (↑(TopCat.of M) : Type u))) x ⋯) = t
⊢ Function.Surjective (α := TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) x)
    (eval IM I N x)

Tactic:
apply TopCat.stalkToFiber_surjective

Premises used: TopCat.stalkToFiber_surjective
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
x : M
n : N
⊢ ∃ (U : OpenNhds (X := TopCat.of M) x) (f : (y : ↥(↑U : Opens (↑(TopCat.of M) : Type u))) → N) (_ :
    TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
      (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
        (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM I ∞) M N ⋯))
      f),
    f (Subtype.mk (p := fun (x_2 : (↑(TopCat.of M) : Type u)) ↦ x_2 ∈ (↑U : Opens (↑(TopCat.of M) : Type u))) x ⋯) = n

Tactic:
⟨⊤, fun _ ↦ n, contMDiff_const, rfl⟩

Premises used: contMDiff_const, Exists.intro, Top.top, rfl
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
x : M
n : N
⊢ ∃ (U : OpenNhds (X := TopCat.of M) x) (f : (y : ↥(↑U : Opens (↑(TopCat.of M) : Type u))) → N) (_ :
    TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
      (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
        (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM I ∞) M N ⋯))
      f),
    f (Subtype.mk (p := fun (x_2 : (↑(TopCat.of M) : Type u)) ↦ x_2 ∈ (↑U : Opens (↑(TopCat.of M) : Type u))) x ⋯) = n

Tactic:
exact ⟨⊤, fun _ ↦ n, contMDiff_const, rfl⟩
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Nontrivial N
x : M
⊢ Nontrivial.{u} (TopCat.Presheaf.stalk (X := TopCat.of M) (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) x)

Tactic:
(smoothSheaf.eval_surjective IM I N x).nontrivial

Premises used: Function.Surjective.nontrivial, smoothSheaf.eval_surjective
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
U : Opens M
x : M
hx : x ∈ U
f : Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) (op U)
⊢ eval IM I N x
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (TopCat.Presheaf.germ (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) U x hx) :
          (a : (fun (X : Type u) ↦ X) ((smoothSheaf IM I M N).presheaf.obj (op U))) →
            (fun (X : Type u) ↦ X) ((smoothSheaf IM I M N).presheaf.stalk x))
        f) =
    (↑f : (x : ↥(unop (op U))) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ N) (↑x : (↑(TopCat.of M) : Type u)))
      (Subtype.mk (p := fun (x : (↑(TopCat.of M) : Type u)) ↦ x ∈ unop (op U)) x hx)

Tactic:
TopCat.stalkToFiber_germ ((contDiffWithinAt_localInvariantProp ∞).localPredicate M N) _ _ _ _

Premises used: TopCat.stalkToFiber_germ, smoothSheaf.eval, contDiffWithinAt_localInvariantProp, WithTop.some, StructureGroupoid.LocalInvariantProp.localPredicate, Top.top
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace HM M
N : Type u
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H N
U : (Opens (↑(TopCat.of M) : Type u))ᵒᵖ
f : Functor.obj (TopCat.Sheaf.presheaf (smoothSheaf IM I M N)) U
⊢ ContMDiff IM I ∞ (↑f : (x : ↥(unop U)) → (fun (x : (↑(TopCat.of M) : Type u)) ↦ N) (↑x : (↑(TopCat.of M) : Type u)))

Tactic:
(contDiffWithinAt_localInvariantProp ∞).section_spec _ _ _ _

Premises used: ChartedSpace.LiftProp, ContMDiffWithinAt, ContMDiff, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.section_spec, WithTop.some, ContMDiffAt, Top.top, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens (↑(TopCat.of P) : Type u))ᵒᵖ
g :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of P) : Type u)))
      (smoothSheaf IP I P N))
    U
apply :
  ContMDiff IM (M := ↥(unop ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ : C(M, P) })).op.obj U))) IP ∞
    (Set.restrictPreimage (unop U).1 f)
⊢ TopCat.PrelocalPredicate.pred (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
    (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(TopCat.of M) : Type u)) ↦ N)
      (StructureGroupoid.LocalInvariantProp.localPredicate (P := ContDiffWithinAtProp IM I ∞) M N ⋯))
    ((↑g : (x : ↥(unop U)) → (fun (x : (↑(TopCat.of P) : Type u)) ↦ N) (↑x : (↑(TopCat.of P) : Type u))) ∘
      Set.restrictPreimage (unop U).1 f)

Tactic:
apply ContMDiff.comp (I' := IP) g.2

Premises used: ContMDiff.comp, Subtype.property
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens (↑(TopCat.of P) : Type u))ᵒᵖ
g :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of P) : Type u)))
      (smoothSheaf IP I P N))
    U
rw :
  ContMDiff IM (M := ↥(unop ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ : C(M, P) })).op.obj U))) IP ∞
    (Subtype.val (p := fun (x : P) ↦ x ∈ unop U) ∘ Set.restrictPreimage (unop U).1 f)
⊢ ContMDiff IM (M := ↥(unop ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ : C(M, P) })).op.obj U))) IP ∞
    (Set.restrictPreimage (unop U).1 f)

Tactic:
rw [← ContMDiff.subtypeVal_comp_iff]

Premises used: ContMDiff.subtypeVal_comp_iff
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens (↑(TopCat.of P) : Type u))ᵒᵖ
g :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of P) : Type u)))
      (smoothSheaf IP I P N))
    U
⊢ ContMDiff IM (M := ↥(unop ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ : C(M, P) })).op.obj U))) IP ∞
    (Subtype.val (p := fun (x : P) ↦ x ∈ unop U) ∘ Set.restrictPreimage (unop U).1 f)

Tactic:
hf.comp contMDiff_subtype_val

Premises used: ContMDiff.comp, contMDiff_subtype_val
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
f : M → P
hf : ContMDiff IM IP ∞ f
U : (Opens (↑(TopCat.of P) : Type u))ᵒᵖ
g :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(TopCat.of P) : Type u)))
      (smoothSheaf IP I P N))
    U
⊢ ContMDiff IM (M := ↥(unop ((Opens.map (TopCat.ofHom { toFun := f, continuous_toFun := ⋯ : C(M, P) })).op.obj U))) IP ∞
    (Subtype.val (p := fun (x : P) ↦ x ∈ unop U) ∘ Set.restrictPreimage (unop U).1 f)

Tactic:
exact hf.comp contMDiff_subtype_val

Premises used: ContMDiff.comp, contMDiff_subtype_val
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Group G
inst_26 : LieGroup I ∞ G
rw :
  CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G)
      (CategoryTheory.forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        GrpCat.carrier)))
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u)) (smoothPresheafGroup IM I M G)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget GrpCat)]

Premises used: GrpCat, CategoryTheory.forget, CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Group G
inst_26 : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G)
      (CategoryTheory.forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        GrpCat.carrier)))

Tactic:
(smoothSheaf IM I M G).property

Premises used: TopCat.subpresheafToTypes, ChartedSpace.LiftProp, ContMDiffWithinAt, Set.Mem, ContMDiff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, smoothSheaf, ContMDiffAt, ChartedSpace.LiftPropAt
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : Group G
inst_26 : LieGroup I ∞ G
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafGroup IM I M G)
      (CategoryTheory.forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        GrpCat.carrier)))

Tactic:
exact (smoothSheaf IM I M G).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, smoothSheaf
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommGroup A
inst_26 : CommGroup A'
inst_27 : LieGroup I ∞ A
inst_28 : LieGroup I' ∞ A'
rw :
  CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A)
      (CategoryTheory.forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        CommGrpCat.carrier)))
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u)) (smoothPresheafCommGroup IM I M A)

Tactic:
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _
        (CategoryTheory.forget CommGrpCat)]

Premises used: CommGrpCat, CategoryTheory.forget, CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
-- Module: Mathlib.Geometry.Manifold.Sheaf.Smooth
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
EM : Type u_2
inst_1 : NormedAddCommGroup EM
inst_2 : NormedSpace 𝕜 EM
HM : Type u_3
inst_3 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace 𝕜 E
H : Type u_5
inst_6 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
H' : Type u_6
inst_7 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst_8 : TopologicalSpace M
inst_9 : ChartedSpace HM M
N G A A' R : Type u
inst_10 : TopologicalSpace N
inst_11 : ChartedSpace H N
inst_12 : TopologicalSpace G
inst_13 : ChartedSpace H G
inst_14 : TopologicalSpace A
inst_15 : ChartedSpace H A
inst_16 : TopologicalSpace A'
inst_17 : ChartedSpace H' A'
inst_18 : TopologicalSpace R
inst_19 : ChartedSpace H R
EP : Type u_7
inst_20 : NormedAddCommGroup EP
inst_21 : NormedSpace 𝕜 EP
HP : Type u_8
inst_22 : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst_23 : TopologicalSpace P
inst_24 : ChartedSpace HP P
inst_25 : CommGroup A
inst_26 : CommGroup A'
inst_27 : LieGroup I ∞ A
inst_28 : LieGroup I' ∞ A'
⊢ CategoryTheory.Presheaf.IsSheaf (C := Opens (↑(TopCat.of M) : Type u))
    (Opens.grothendieckTopology (↑(TopCat.of M) : Type u))
    (CategoryTheory.Functor.comp (smoothPresheafCommGroup IM I M A)
      (CategoryTheory.forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
        CommGrpCat.carrier)))

Tactic:
(smoothSheaf IM I M A).property

Premises used: TopCat.subpresheafToTypes, ChartedSpace.LiftProp, ContMDiffWithinAt, Set.Mem, ContMDiff, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, smoothSheaf, ContMDiffAt, ChartedSpace.LiftPropAt