mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
⊢ toMatrix' (star f).ofConv = (toMatrix' f.ofConv).map star

Tactic:
ext

Goal state after:
R : Type u_4
m : Type u_5
n : Type u_6
inst✝³ : CommSemiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : WithConv ((m → R) →ₗ[R] n → R)
i✝ : n
j✝ : m
⊢ toMatrix' (star f).ofConv i✝ j✝ = (toMatrix' f.ofConv).map star i✝ j✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝¹ x✝ : HVertexOperator Γ R V W
⊢ (fun n ↦ { toFun := fun v ↦ ((of R).symm ((x✝¹ + x✝) v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) =
    (fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝¹ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) + fun n ↦
      { toFun := fun v ↦ ((of R).symm (x✝ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝³ x✝² : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ { toFun := fun v ↦ ((of R).symm ((x✝³ + x✝²) v)).coeff x✝¹, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝³ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) + fun n ↦
          { toFun := fun v ↦ ((of R).symm (x✝² v)).coeff n, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝¹ : R
x✝ : HVertexOperator Γ R V W
⊢ (fun n ↦ { toFun := fun v ↦ ((of R).symm ((x✝¹ • x✝) v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }) =
    (RingHom.id R) x✝¹ • fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝ v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
x✝³ : R
x✝² : HVertexOperator Γ R V W
x✝¹ : Γ
x✝ : V
⊢ { toFun := fun v ↦ ((of R).symm ((x✝³ • x✝²) v)).coeff x✝¹, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((RingHom.id R) x✝³ • fun n ↦ { toFun := fun v ↦ ((of R).symm (x✝² v)).coeff n, map_add' := ⋯, map_smul' := ⋯ })
        x✝¹)
      x✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝¹ x✝ : V
⊢ (of R) { coeff := fun g ↦ (f g) (x✝¹ + x✝), isPWO_support' := ⋯ } =
    (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ } +
      (of R) { coeff := fun g ↦ (f g) x✝, isPWO_support' := ⋯ }

Tactic:
ext

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝² x✝¹ : V
x✝ : Γ
⊢ ((of R).symm ((of R) { coeff := fun g ↦ (f g) (x✝² + x✝¹), isPWO_support' := ⋯ })).coeff x✝ =
    ((of R).symm
          ((of R) { coeff := fun g ↦ (f g) x✝², isPWO_support' := ⋯ } +
            (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ })).coeff
      x✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝¹ : R
x✝ : V
⊢ (of R) { coeff := fun g ↦ (f g) (x✝¹ • x✝), isPWO_support' := ⋯ } =
    (RingHom.id R) x✝¹ • (of R) { coeff := fun g ↦ (f g) x✝, isPWO_support' := ⋯ }

Tactic:
ext

Goal state after:
Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
f : Γ → V →ₗ[R] W
hf : ∀ (x : V), (Function.support fun x_1 ↦ (f x_1) x).IsPWO
x✝² : R
x✝¹ : V
x✝ : Γ
⊢ ((of R).symm ((of R) { coeff := fun g ↦ (f g) (x✝² • x✝¹), isPWO_support' := ⋯ })).coeff x✝ =
    ((of R).symm ((RingHom.id R) x✝² • (of R) { coeff := fun g ↦ (f g) x✝¹, isPWO_support' := ⋯ })).coeff x✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

Tactic:
ext

Goal state after:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (u + v)).coeff x✝¹).coeff x✝ = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x✝¹).coeff x✝
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
ext

Goal state after:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : PartialOrder Γ
inst✝⁷ : PartialOrder Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (r • u)).coeff x✝¹).coeff x✝ = ((r • A.compHahnSeries B u).coeff x✝¹).coeff x✝
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
⊢ (stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x = 𝟙 (X.presheaf.stalk x)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : PresheafedSpace C
x : ↑↑X
U✝ : Opens ↑↑X
hxU✝ : x ∈ U✝
⊢ X.presheaf.germ U✝ x hxU✝ ≫ (stalkFunctor C x).map (𝟙 X).c ≫ stalkPushforward C (𝟙 ↑X) X.presheaf x =
    X.presheaf.germ U✝ x hxU✝ ≫ 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ Mono f

Tactic:
constructor

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Injective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Epi (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ ∀ {Z : SheafedSpace C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ = eqToHom ⋯ ≫ Hom.stalkMap β x'

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h₁ : α = β
x x' : ↑↑X
h₂ : x = x'
U✝ : Opens ↑↑Y
hxU✝ : (ConcreteCategory.hom α.base) x ∈ U✝
⊢ Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ Hom.stalkMap α x ≫ eqToHom ⋯ =
    Y.presheaf.germ U✝ ((ConcreteCategory.hom α.base) x) hxU✝ ≫ eqToHom ⋯ ≫ Hom.stalkMap β x'
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Hom.stalkMap α x = eqToHom ⋯ ≫ Hom.stalkMap β x

Tactic:
by
  rw [← stalkMap.congr α β h x x rfl, eqToHom_refl, Category.comp_id]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ Epi f

Tactic:
constructor

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ ∀ {Z : SheafedSpace C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
use V, i, hv

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case h
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J TopCat
inst✝ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
F : J ⥤ PresheafedSpace C
j j' : J
f : j ⟶ j'
⊢ (F.map f ≫ { base := colimit.ι (F ⋙ forget C) j', c := limit.π (pushforwardDiagramToColimit F).leftOp (op j') }).c ≫
      whiskerRight (eqToHom ⋯) (F.obj j).presheaf =
    ({ base := colimit.ι (F ⋙ forget C) j, c := limit.π (pushforwardDiagramToColimit F).leftOp (op j) } ≫
        ((Functor.const J).obj (colimit F)).map f).c

Tactic:
· ext ⟨⟩
          simp [← congr_arg NatTrans.app (limit.w (pushforwardDiagramToColimit F).leftOp f.op)]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑X
⊢ (ConcreteCategory.hom
        ({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base)
      x✝ =
    (ConcreteCategory.hom (𝟙 X).base) x✝

case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
          whiskerRight (eqToHom ⋯) X.presheaf).app
      (op U✝) =
    (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
⊢ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv } = 𝟙 Y

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑Y
⊢ (ConcreteCategory.hom
        ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).base)
      x✝ =
    (ConcreteCategory.hom (𝟙 Y).base) x✝

case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
          whiskerRight (eqToHom ⋯) Y.presheaf).app
      (op U✝) =
    (𝟙 Y).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ Mono (X.ofRestrict hf)

Tactic:
constructor

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ ∀ {Z : PresheafedSpace C} (g h : Z ⟶ X.restrict hf), g ≫ X.ofRestrict hf = h ≫ X.ofRestrict hf → g = h
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) ↔
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
constructor

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) →
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

case mpr
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s)) →
    x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s))
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) ↔ x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
constructor

Goal state after:
case mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) → x ∈ ↑(unop V ⊓ X.basicOpen f)

case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.ofRestrict ⋯).c = eqToHom ⋯

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ (X.ofRestrict ⋯).c.app (op U✝) = (eqToHom ⋯).app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
⊢ colimit.ι (F ⋙ forget C) j ≫ m.base =
    colimit.ι (F ⋙ forget C) j ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)

Tactic:
ext

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑((F ⋙ forget C).obj j)
⊢ (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ m.base)) x✝ =
    (ConcreteCategory.hom (colimit.ι (F ⋙ forget C) j ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))) x✝
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.ofRestrict ⋯ ≫ X.toRestrictTop = 𝟙 (X.restrict ⋯)

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑(X.restrict ⋯)
⊢ (ConcreteCategory.hom (X.ofRestrict ⋯ ≫ X.toRestrictTop).base) x✝ = (ConcreteCategory.hom (𝟙 (X.restrict ⋯)).base) x✝

case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((X.ofRestrict ⋯ ≫ X.toRestrictTop).c ≫ whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ X.toRestrictTop ≫ X.ofRestrict ⋯ = 𝟙 X

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
x✝ : ↑↑X
⊢ (ConcreteCategory.hom (X.toRestrictTop ≫ X.ofRestrict ⋯).base) x✝ = (ConcreteCategory.hom (𝟙 X).base) x✝

case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
⊢ { base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F } = 𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
x✝ : ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.base) x✝ =
    (ConcreteCategory.hom (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).base) x✝

case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U✝ : Opens ↑↑{ carrier := ↑X, presheaf := X.presheaf ⋙ F }
⊢ ({ base := (𝟙 X).base, c := whiskerRight (𝟙 X).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X, presheaf := X.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    (𝟙 { carrier := ↑X, presheaf := X.presheaf ⋙ F }).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F } =
    { base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }

Tactic:
ext

Goal state after:
case w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑↑{ carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }
⊢ (ConcreteCategory.hom { base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.base) x✝ =
    (ConcreteCategory.hom
        ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).base)
      x✝

case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U✝ : Opens ↑↑{ carrier := ↑Z✝, presheaf := Z✝.presheaf ⋙ F }
⊢ ({ base := (f ≫ g).base, c := whiskerRight (f ≫ g).c F }.c ≫
          whiskerRight (eqToHom ⋯) { carrier := ↑X✝, presheaf := X✝.presheaf ⋙ F }.presheaf).app
      (op U✝) =
    ({ base := f.base, c := whiskerRight f.c F } ≫ { base := g.base, c := whiskerRight g.c F }).c.app (op U✝)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
have ⟨V, hV, i, h⟩ := w x

Goal state after:
case refine_1
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)

Tactic:
have ⟨V, hV, i, h⟩ := w x

Goal state after:
case refine_2
X : TopCat
T : ↑X → Type u_1
P Q : LocalPredicate T
U✝ : Opens ↑X
f : (x : ↥U✝) → T ↑x
w : ∀ (x : ↥U✝), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
x : ↥U✝
V : Opens ↑X
hV : ↑x ∈ V
i : V ⟶ U✝
h : (P.and Q.toPrelocalPredicate).pred fun x ↦ f (i x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, Q.pred fun x ↦ f (i x)