mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : Limits.HasPullbacks C
F : Sheaf J A
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y_1 : (Over Y)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    (F.over Y).obj.map f_1 ≫ F.obj.map (Limits.pullback.fst (Opposite.unop Y_1).hom f).op =
      F.obj.map (Limits.pullback.fst (Opposite.unop X_1).hom f).op ≫
        (((Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)).obj.map f_1

Tactic:
by simp [← Functor.map_comp, ← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ K.toGrothendieck.over X ≤ (Precoverage.comap (Over.forget X) K).toGrothendieck
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ (Precoverage.comap (Over.forget X) K).toGrothendieck ≤ K.toGrothendieck.over X
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
⊢ s₁ = s₂

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
⊢ ∃ a, F.sectionsPrecomp a = t

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
⊢ s₁ = s₂
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
⊢ ∃ a, F.sectionsPrecomp a = t

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
⊢ ∃ a, F.sectionsPrecomp a = t
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
⊢ (ConcreteCategory.hom (P.map f)) (val Y₁) = val Y₂

pp: case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
⊢ (ConcreteCategory.hom (P.map f)) (val Y₁) = val Y₂
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
⊢ F.sectionsPrecomp ⟨val, ⋯⟩ = t
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Injective (F.colimitTypePrecomp P)

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Injective (F.colimitTypePrecomp P)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_1
inst✝⁶ : Category.{v_1, u_1} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁴ : F.PreservesMonomorphisms
inst✝³ : F.PreservesZeroMorphisms
inst✝² : F.ReflectsIsomorphisms
inst✝¹ : F.Faithful
X : C
inst✝ : Simple (F.obj X)
Y : C
g : Y ⟶ X
x✝ : Mono g
⊢ IsIso g ↔ g ≠ 0

Tactic:
by
    rw [← isIso_iff_of_reflects_iso g F, Simple.mono_isIso_iff_nonzero (F.map g),
      ne_eq, ne_eq, not_iff_not, F.map_eq_zero_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f → f ≠ 0

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f → f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
Y : C
i : Y ⟶ X
w✝ : Mono i
h : ¬i = 0
⊢ mk i = ⊥ ∨ mk i = ⊤
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0

pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr.inl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f

pp: case mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f

Tactic:
·

Goal state after:
case mpr.inl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f

Tactic:
·

Goal state after:
case mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U

pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Tactic:
·

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Tactic:
·

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Tactic:
· intro x hx
    obtain ⟨U, hU⟩ := U
    obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU
    exact Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
·

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
·

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case refine_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1

pp: case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯

Tactic:
·

Goal state after:
case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) → x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)

pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
·

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) → x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
·

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U

pp: case mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
·

Goal state after:
case mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
·

Goal state after:
case mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = ?m.15

pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.15 = Finset.univ.inf f

pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Tactic:
·

Goal state after:
α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∏ᶜ f = ?m.15
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.15

pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.15 = Finset.univ.sup f

pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Tactic:
·

Goal state after:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.15
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T

pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology

Tactic:
·

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology

Tactic:
·

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case refine_1
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
h :
  Sieve.ofObjects U ⊤ ∈
    { sieves := fun X ↦ {S | ∀ x ∈ X, ∃ U, (∃ x, S.arrows x) ∧ x ∈ U}, top_mem' := ⋯, pullback_stable' := ⋯,
        transitive' := ⋯ }
      ⊤
x : T
⊢ ∃ i, x ∈ U i

pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1

Tactic:
·

Goal state after:
case refine_1
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
h :
  Sieve.ofObjects U ⊤ ∈
    { sieves := fun X ↦ {S | ∀ x ∈ X, ∃ U, (∃ x, S.arrows x) ∧ x ∈ U}, top_mem' := ⋯, pullback_stable' := ⋯,
        transitive' := ⋯ }
      ⊤
x : T
⊢ ∃ i, x ∈ U i
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1

Tactic:
·

Goal state after:
case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1