awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M ⊕ M') I (M' := M ⊕ M' ⊕ M'') n (Sum.elim Sum.inl (Sum.inr ∘ Sum.inl))

Tactic:
exact contMDiff_id.sumMap ContMDiff.inl

Premises used: ContMDiff.sumMap, ContMDiff.inl, contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M'') I (M' := M ⊕ M' ⊕ M'') n (Sum.inr ∘ Sum.inr)

Tactic:
ContMDiff.inr.comp ContMDiff.inr

Premises used: ContMDiff.comp, ContMDiff.inr
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M'') I (M' := M ⊕ M' ⊕ M'') n (Sum.inr ∘ Sum.inr)

Tactic:
exact ContMDiff.inr.comp ContMDiff.inr

Premises used: ContMDiff.comp, ContMDiff.inr
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
hf : ContMDiff I (M := M) I (M' := (M ⊕ M') ⊕ M'') n (Sum.inl ∘ Sum.inl)
hg : ContMDiff I (M := M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)
⊢ ContMDiff I (M := M ⊕ M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n
    (⇑(Equiv.sumAssoc M M' M'').symm : (a : M ⊕ M' ⊕ M'') → (M ⊕ M') ⊕ M'')

Tactic:
apply ContMDiff.sumElim

Premises used: ContMDiff.sumElim
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M) I (M' := (M ⊕ M') ⊕ M'') n (Sum.inl ∘ Sum.inl)

Tactic:
ContMDiff.inl.comp ContMDiff.inl

Premises used: ContMDiff.comp, ContMDiff.inl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M) I (M' := (M ⊕ M') ⊕ M'') n (Sum.inl ∘ Sum.inl)

Tactic:
exact ContMDiff.inl.comp ContMDiff.inl

Premises used: ContMDiff.comp, ContMDiff.inl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)

Tactic:
ContMDiff.inr.sumMap contMDiff_id

Premises used: Sum.map, ContMDiff.inr, ContMDiff.sumMap, contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
E' : Type u_3
inst_3 : NormedAddCommGroup E'
inst_4 : NormedSpace 𝕜 E'
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
H : Type u_5
inst_7 : TopologicalSpace H
H' : Type u_6
inst_8 : TopologicalSpace H'
G : Type u_7
inst_9 : TopologicalSpace G
G' : Type u_8
inst_10 : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J_1 : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F G'
M : Type u_9
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace H M
M'_1 : Type u_10
inst_13 : TopologicalSpace M'_1
inst_14 : ChartedSpace H' M'_1
N_1 : Type u_11
inst_15 : TopologicalSpace N_1
inst_16 : ChartedSpace G N_1
N'_1 : Type u_12
inst_17 : TopologicalSpace N'_1
inst_18 : ChartedSpace G' N'_1
n : ℕ∞ω
M' : Type u_13
inst_19 : TopologicalSpace M'
inst_20 : ChartedSpace H M'
M'' : Type u_14
inst_21 : TopologicalSpace M''
inst_22 : ChartedSpace H M''
N : Type u_15
J_2 : Type u_16
inst_23 : TopologicalSpace N
inst_24 : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst_25 : TopologicalSpace N'
inst_26 : ChartedSpace H N'
⊢ ContMDiff I (M := M' ⊕ M'') I (M' := (M ⊕ M') ⊕ M'') n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)

Tactic:
exact ContMDiff.inr.sumMap contMDiff_id

Premises used: ContMDiff.inr, ContMDiff.sumMap, contMDiff_id
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
M'' : Type u_14
inst_8 : TopologicalSpace M''
inst_9 : ChartedSpace H M''
⊢ Eq (α := (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'') (⇑(sumAssoc I M n M' M'') : (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'')
    (⇑(Equiv.sumAssoc M M' M'') : (a : (M ⊕ M') ⊕ M'') → M ⊕ M' ⊕ M'')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
inst_8 : IsEmpty M'
⊢ toEquiv (sumEmpty I M n) = Equiv.sumEmpty M M'

Tactic:
rfl

Premises used: rfl, Equiv.sumEmpty
-- Module: Mathlib.Geometry.Manifold.Diffeomorph
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_5
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
n : ℕ∞ω
M' : Type u_13
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
inst_8 : IsEmpty M'
x : M
⊢ (sumEmpty I M n : (a : M ⊕ M') → M) (Sum.inl x) = x

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
carrier : TopCat
presheaf : Presheaf.{u_1, v, u} C carrier
h : presheaf.IsSheaf
⊢ (↑{ carrier := carrier, presheaf := presheaf, IsSheaf := h : SheafedSpace.{u, v, u_1} C }.toPresheafedSpace :
      TopCat) =
    carrier

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
rw rw₁ : (Opens.map β.hom.base).op = (Opens.map β.hom.base).op
⊢ (Opens.map α.hom.base).op = (Opens.map β.hom.base).op

Tactic:
rw [w]
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
w : α.hom.base = β.hom.base
h : α.hom.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.hom.c
⊢ α = β

Tactic:
InducedCategory.hom_ext (PresheafedSpace.ext _ _ w h)

Premises used: CategoryTheory.InducedCategory.hom_ext, AlgebraicGeometry.PresheafedSpace.ext
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : obj forgetToPresheafedSpace X ⟶ obj forgetToPresheafedSpace Y
⊢ (FullyFaithful.preimage fullyFaithfulForgetToPresheafedSpace f).hom = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Full (C := SheafedSpace.{u, v, u_1} C) forgetToPresheafedSpace

Tactic:
fullyFaithfulForgetToPresheafedSpace.full

Premises used: AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Faithful (C := SheafedSpace.{u, v, u_1} C) forgetToPresheafedSpace

Tactic:
fullyFaithfulForgetToPresheafedSpace.faithful

Premises used: AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.hom

Tactic:
SheafedSpace.forgetToPresheafedSpace.map_isIso f

Premises used: AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : SheafedSpace.{u, v, u_1} C
⊢ InducedCategory.Hom.hom (𝟙 X) = 𝟙 X.toPresheafedSpace

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : SheafedSpace.{u, v, u_1} C
⊢ (InducedCategory.Hom.hom (𝟙 X)).base = 𝟙 (↑X.toPresheafedSpace : TopCat)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : SheafedSpace.{u, v, u_1} C
⊢ (InducedCategory.Hom.hom (𝟙 X)).c = eqToHom ⋯

Tactic:
rfl

Premises used: Eq.mpr, Set.Mem, Quiver.Hom.op, CategoryTheory.eqToHom, setOf, CategoryTheory.Functor.comp, TopCat.Presheaf, Set.preimage, rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : SheafedSpace.{u, v, u_1} C
U : (Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ (InducedCategory.Hom.hom (𝟙 X)).c.app U = 𝟙 (X.presheaf.obj U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom.base = f.hom.base ≫ g.hom.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
α : X ⟶ Y
β : Y ⟶ Z
U : (Opens (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ (α ≫ β).hom.c.app U = β.hom.c.app U ≫ α.hom.c.app (op ((Opens.map β.hom.base).obj (unop U)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
α : X ⟶ Y
β : Y ⟶ Z
U : Opens (↑(↑Z.toPresheafedSpace : TopCat) : Type u_1)
⊢ Eq (α := Z.presheaf.obj (op U) ⟶ (obj (Presheaf.pushforward C (α ≫ β).hom.base) X.presheaf).obj (op U))
    ((α ≫ β).hom.c.app (op U)) (β.hom.c.app (op U) ≫ α.hom.c.app (op ((Opens.map β.hom.base).obj U)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
subst : (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U
⊢ (Opens.map β.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
subst h
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α : X ⟶ Y
U : (Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ (Opens.map α.hom.base).op.obj U = (Opens.map α.hom.base).op.obj U

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
α β : X ⟶ Y
h : α = β
U : (Opens (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
rw rw₁ : β.hom = β.hom
⊢ α.hom = β.hom

Tactic:
rw [h]
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
⊢ Eq (α := (SheafedSpace.{u, v, u_1} C)ᵒᵖ ⥤ C) Γ (Functor.op forgetToPresheafedSpace ⋙ PresheafedSpace.Γ)

Tactic:
rfl

Premises used: rfl, AlgebraicGeometry.SheafedSpace.Γ
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : (SheafedSpace.{u, v, u_1} C)ᵒᵖ
⊢ obj Γ X = (unop X).presheaf.obj (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X : SheafedSpace.{u, v, u_1} C
⊢ obj Γ (op X) = X.presheaf.obj (op ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : (SheafedSpace.{u, v, u_1} C)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α := obj Γ X ⟶ obj Γ Y) (map Γ f) (f.unop.hom.c.app (op ⊤))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
⊢ Eq (α := obj Γ (op Y) ⟶ obj Γ (op X)) (map Γ f.op) (f.hom.c.app (op ⊤))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
inst_3 : HasLimitsOfShape.{w', w, v, u} Jᵒᵖ C
⊢ HasColimitsOfShape J (SheafedSpace.{u, v, v} C)

Tactic:
hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape forgetToPresheafedSpace

Premises used: CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{w', w} J
inst_2 : Small.{v, w} J
inst_3 : HasLimitsOfShape.{w', w, v, u} Jᵒᵖ C
⊢ PreservesColimitsOfShape (C := SheafedSpace.{u, v, v} C) J (forget C)

Tactic:
Limits.comp_preservesColimitsOfShape forgetToPresheafedSpace (PresheafedSpace.forget C)

Premises used: CategoryTheory.Functor.comp, AlgebraicGeometry.SheafedSpace.forget, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace, CategoryTheory.Limits.comp_preservesColimitsOfShape, AlgebraicGeometry.PresheafedSpace.forget
-- Module: Mathlib.Geometry.RingedSpace.SheafedSpace
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_1 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_2 : HasColimits.{v, u} C
inst_3 : HasLimits.{v, u} C
inst_4 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f g : X ⟶ Y
h : f.hom.base = g.hom.base
h' :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    Eq (α :=
      Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
            x) ⟶
        X.presheaf.stalk x)
      (PresheafedSpace.Hom.stalkMap f.hom x) (Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ PresheafedSpace.Hom.stalkMap g.hom x)
obtain :
  ∀ (f : (↑X.toPresheafedSpace : TopCat) ⟶ (↑Y.toPresheafedSpace : TopCat))
    (fc : Y.presheaf ⟶ obj (pushforward C f) X.presheaf)
    (h : PresheafedSpace.Hom.base (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) = g.hom.base)
    (h' :
      ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
        Eq (α :=
          Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := carrier)
                    (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                    (PresheafedSpace.Hom.base
                      (InducedCategory.Hom.hom
                        { hom := { base := f, c := fc : X.Hom Y.toPresheafedSpace } :
                          InducedCategory.Hom (D := PresheafedSpace.{v, u, v} C) (F := toPresheafedSpace) X Y })) :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
                x) ⟶
            X.presheaf.stalk x)
          (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom { hom := { base := f, c := fc } }) x)
          (Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ PresheafedSpace.Hom.stalkMap g.hom x)),
    { hom := { base := f, c := fc } } = g
⊢ f = g

Tactic:
obtain ⟨f, fc⟩ := f