awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
op : {x : (↑X : Type u_3)} → T x → T x
hop :
  ∀ {U : Opens (↑X : Type u_3)} {a : (x : ↥U) → T (↑x : (↑X : Type u_3))},
    P.pred (T := T) a →
      ∀ (p : ↥U),
        ∃ (W : Opens (↑X : Type u_3)) (i : W ⟶ U),
          (↑p : (↑X : Type u_3)) ∈ W ∧ P.pred (T := T) (U := W) fun (x : ↥W) ↦ op (a ((i : (a : ↥W) → ↥U) x))
U : Opens (↑X : Type u_3)
a : (x : ↥U) → T (↑x : (↑X : Type u_3))
ha_1 : P.sheafify (T := T).toPrelocalPredicate (T := T).pred (T := T) a
x : ↥U
Va : Opens (↑X : Type u_3)
ma : (↑x : (↑X : Type u_3)) ∈ Va
ia : Va ⟶ U
ha : P.pred (T := T) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)
W : Opens (↑X : Type u_3)
sa : W ⟶ Va
hx : (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ Va) (↑x : (↑X : Type u_3)) ma) : (↑X : Type u_3)) ∈ W
hw : P.pred (T := T) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥Va) → ↥U) ((sa : (a : ↥W) → ↥Va) x)))
⊢ ∃ (V : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U),
    P.pred (T := T) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨W, hx, sa ≫ ia, hw⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
op : {x : (↑X : Type u_3)} → T x → T x
hop :
  ∀ {U : Opens (↑X : Type u_3)} {a : (x : ↥U) → T (↑x : (↑X : Type u_3))},
    P.pred (T := T) a → P.pred (T := T) (U := U) fun (x : ↥U) ↦ op (a x)
U : Opens (↑X : Type u_3)
a : (x : ↥U) → T (↑x : (↑X : Type u_3))
ha : P.sheafify (T := T).toPrelocalPredicate (T := T).pred (T := T) a
⊢ P.sheafify (T := T).toPrelocalPredicate (T := T).pred (T := T) (U := U) fun (x : ↥U) ↦ op (a x)

Tactic:
P.sheafify_inductionOn op (fun ha p ↦ ⟨_, 𝟙 _, p.2, hop ha⟩) ha

Premises used: TopCat.PrelocalPredicate.sheafify_inductionOn, CategoryTheory.CategoryStruct.id, And.intro, Exists.intro, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        ∀ (p : ↥(U ⊓ V)),
          ∃ (W : Opens (↑X : Type u_5)) (ia : W ⟶ U) (ib : W ⟶ V),
            (↑p : (↑X : Type u_5)) ∈ W ∧
              P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥W) → ↥U) x)) (b ((ib : (a : ↥W) → ↥V) x))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
x : ↥U
rcases :
  ∀ (Va : Opens (↑X : Type u_5)) (ma : (↑x : (↑X : Type u_5)) ∈ Va) (ia : Va ⟶ U)
    (ha : P₁.pred (T := T₁) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)),
    ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
      P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
    P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
rcases ha x with ⟨Va, ma, ia, ha⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        ∀ (p : ↥(U ⊓ V)),
          ∃ (W : Opens (↑X : Type u_5)) (ia : W ⟶ U) (ib : W ⟶ V),
            (↑p : (↑X : Type u_5)) ∈ W ∧
              P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥W) → ↥U) x)) (b ((ib : (a : ↥W) → ↥V) x))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha_1 : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
x : ↥U
Va : Opens (↑X : Type u_5)
ma : (↑x : (↑X : Type u_5)) ∈ Va
ia : Va ⟶ U
ha : P₁.pred (T := T₁) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)
rcases :
  ∀ (Vb : Opens (↑X : Type u_5)) (mb : (↑x : (↑X : Type u_5)) ∈ Vb) (ib : Vb ⟶ U)
    (hb : P₂.pred (T := T₂) (U := Vb) fun (x : ↥Vb) ↦ b ((ib : (a : ↥Vb) → ↥U) x)),
    ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
      P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
    P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
rcases hb x with ⟨Vb, mb, ib, hb⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        ∀ (p : ↥(U ⊓ V)),
          ∃ (W : Opens (↑X : Type u_5)) (ia : W ⟶ U) (ib : W ⟶ V),
            (↑p : (↑X : Type u_5)) ∈ W ∧
              P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥W) → ↥U) x)) (b ((ib : (a : ↥W) → ↥V) x))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha_1 : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb_1 : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
x : ↥U
Va : Opens (↑X : Type u_5)
ma : (↑x : (↑X : Type u_5)) ∈ Va
ia : Va ⟶ U
ha : P₁.pred (T := T₁) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)
Vb : Opens (↑X : Type u_5)
mb : (↑x : (↑X : Type u_5)) ∈ Vb
ib : Vb ⟶ U
hb : P₂.pred (T := T₂) (U := Vb) fun (x : ↥Vb) ↦ b ((ib : (a : ↥Vb) → ↥U) x)
rcases :
  ∀ (W : Opens (↑X : Type u_5)) (sa : W ⟶ Va) (sb : W ⟶ Vb)
    (hx : (↑(Subtype.mk (p := fun (x : (↑X : Type u_5)) ↦ x ∈ Va ⊓ Vb) (↑x : (↑X : Type u_5)) ⋯) : (↑X : Type u_5)) ∈ W)
    (hw :
      P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦
        op (a ((ia : (a : ↥Va) → ↥U) ((sa : (a : ↥W) → ↥Va) x))) (b ((ib : (a : ↥Vb) → ↥U) ((sb : (a : ↥W) → ↥Vb) x)))),
    ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
      P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
    P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
rcases hop ha hb ⟨x, ma, mb⟩ with ⟨W, sa, sb, hx, hw⟩

Premises used: Subtype.mk, And.intro, Subtype.val
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        ∀ (p : ↥(U ⊓ V)),
          ∃ (W : Opens (↑X : Type u_5)) (ia : W ⟶ U) (ib : W ⟶ V),
            (↑p : (↑X : Type u_5)) ∈ W ∧
              P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥W) → ↥U) x)) (b ((ib : (a : ↥W) → ↥V) x))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha_1 : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb_1 : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
x : ↥U
Va : Opens (↑X : Type u_5)
ma : (↑x : (↑X : Type u_5)) ∈ Va
ia : Va ⟶ U
ha : P₁.pred (T := T₁) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)
Vb : Opens (↑X : Type u_5)
mb : (↑x : (↑X : Type u_5)) ∈ Vb
ib : Vb ⟶ U
hb : P₂.pred (T := T₂) (U := Vb) fun (x : ↥Vb) ↦ b ((ib : (a : ↥Vb) → ↥U) x)
W : Opens (↑X : Type u_5)
sa : W ⟶ Va
sb : W ⟶ Vb
hx : (↑(Subtype.mk (p := fun (x : (↑X : Type u_5)) ↦ x ∈ Va ⊓ Vb) (↑x : (↑X : Type u_5)) ⋯) : (↑X : Type u_5)) ∈ W
hw :
  P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦
    op (a ((ia : (a : ↥Va) → ↥U) ((sa : (a : ↥W) → ↥Va) x))) (b ((ib : (a : ↥Vb) → ↥U) ((sb : (a : ↥W) → ↥Vb) x)))
⊢ ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
    P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨W, hx, sa ≫ ia, hw⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        ∀ (p : ↥(U ⊓ V)),
          ∃ (W : Opens (↑X : Type u_5)) (ia : W ⟶ U) (ib : W ⟶ V),
            (↑p : (↑X : Type u_5)) ∈ W ∧
              P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦ op (a ((ia : (a : ↥W) → ↥U) x)) (b ((ib : (a : ↥W) → ↥V) x))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha_1 : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb_1 : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
x : ↥U
Va : Opens (↑X : Type u_5)
ma : (↑x : (↑X : Type u_5)) ∈ Va
ia : Va ⟶ U
ha : P₁.pred (T := T₁) (U := Va) fun (x : ↥Va) ↦ a ((ia : (a : ↥Va) → ↥U) x)
Vb : Opens (↑X : Type u_5)
mb : (↑x : (↑X : Type u_5)) ∈ Vb
ib : Vb ⟶ U
hb : P₂.pred (T := T₂) (U := Vb) fun (x : ↥Vb) ↦ b ((ib : (a : ↥Vb) → ↥U) x)
W : Opens (↑X : Type u_5)
sa : W ⟶ Va
sb : W ⟶ Vb
hx : (↑(Subtype.mk (p := fun (x : (↑X : Type u_5)) ↦ x ∈ Va ⊓ Vb) (↑x : (↑X : Type u_5)) ⋯) : (↑X : Type u_5)) ∈ W
hw :
  P₃.pred (T := T₃) (U := W) fun (x : ↥W) ↦
    op (a ((ia : (a : ↥Va) → ↥U) ((sa : (a : ↥W) → ↥Va) x))) (b ((ib : (a : ↥Vb) → ↥U) ((sb : (a : ↥W) → ↥Vb) x)))
⊢ ∃ (V : Opens (↑X : Type u_5)) (_ : (↑x : (↑X : Type u_5)) ∈ V) (i : V ⟶ U),
    P₃.pred (T := T₃) (U := V) fun (x : ↥V) ↦ (fun (x : ↥U) ↦ op (a x) (b x)) ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨W, hx, sa ≫ ia, hw⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T₁ : (↑X : Type u_5) → Type u_2
T₂ : (↑X : Type u_5) → Type u_3
T₃ : (↑X : Type u_5) → Type u_4
P₁ : PrelocalPredicate T₁
P₂ : PrelocalPredicate T₂
P₃ : PrelocalPredicate T₃
op : {x : (↑X : Type u_5)} → T₁ x → T₂ x → T₃ x
hop :
  ∀ {U V : Opens (↑X : Type u_5)} {a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))} {b : (x : ↥V) → T₂ (↑x : (↑X : Type u_5))},
    P₁.pred (T := T₁) a →
      P₂.pred (T := T₂) b →
        P₃.pred (T := T₃) (U := U ⊓ V) fun (x : ↥(U ⊓ V)) ↦
          op (a (Subtype.mk (p := fun (x : (↑X : Type u_5)) ↦ x ∈ U) (↑x : (↑X : Type u_5)) ⋯))
            (b (Subtype.mk (p := fun (x : (↑X : Type u_5)) ↦ x ∈ V) (↑x : (↑X : Type u_5)) ⋯))
U : Opens (↑X : Type u_5)
a : (x : ↥U) → T₁ (↑x : (↑X : Type u_5))
b : (x : ↥U) → T₂ (↑x : (↑X : Type u_5))
ha : P₁.sheafify (T := T₁).toPrelocalPredicate (T := T₁).pred (T := T₁) a
hb : P₂.sheafify (T := T₂).toPrelocalPredicate (T := T₂).pred (T := T₂) b
⊢ P₃.sheafify (T := T₃).toPrelocalPredicate (T := T₃).pred (T := T₃) (U := U) fun (x : ↥U) ↦ op (a x) (b x)

Tactic:
P₁.sheafify_inductionOn₂ P₂ P₃ op
    (fun ha hb p ↦ ⟨_, Opens.infLELeft _ _, Opens.infLERight _ _, p.2, hop ha hb⟩) ha hb

Premises used: And.intro, Exists.intro, TopologicalSpace.Opens.infLELeft, TopologicalSpace.Opens.infLERight, TopCat.PrelocalPredicate.sheafify_inductionOn₂, Min.min, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
⊢ (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'

Tactic:
have sf'_comp : (presheafToTypes X T).IsCompatible U sf' := fun i j ↦
      congr_arg Subtype.val (sf_comp i j)
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
⊢ IsCompatible (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'

Tactic:
sf'_comp

Premises used: TopCat.presheafToTypes
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
⊢ IsCompatible (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'

Tactic:
exact sf'_comp
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
obtain :
  ∀
    (gl :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U))))
    (gl_spec :
      IsGluing (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U
        sf' gl)
    (gl_uniq :
      ∀
        (y :
          ToType (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
              (op (iSup U)))),
        (fun
                (s :
                  ToType (FC := TypeCat.Fun)
                    ((X.sheafToTypes T).obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                      (op (iSup U)))) ↦
              IsGluing (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
                U sf' s)
            y →
          y = gl),
    ∃! s :
      ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U))),
      (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s
⊢ ∃! s : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U))),
    (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s

Tactic:
obtain ⟨gl, gl_spec, gl_uniq⟩ := (sheafToTypes X T).existsUnique_gluing U sf'
      -- `by exact` to help Lean infer the `ConcreteCategory` instance
      (by exact sf'_comp)

Premises used: TopCat.sheafToTypes, TopCat.Sheaf.existsUnique_gluing
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
⊢ ∃! s : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U))),
    (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s

Tactic:
⟨⟨gl, ?_⟩, ?_, ?_⟩

Premises used: Subtype.mk, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
refine_1 : P.toPrelocalPredicate (T := T).pred (T := T) gl
refine_2 :
  (fun
        (s :
          ToType (FC := TypeCat.Fun)
            ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))) ↦
      (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s)
    (Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
      P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯)
refine_3 :
  ∀ (y : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))) ↦
          (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s)
        y →
      y =
        Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯
⊢ ∃! s : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U))),
    (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s

Tactic:
refine ⟨⟨gl, ?_⟩, ?_, ?_⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
refine_1 :
  ∀ (x : ↥(unop (op (iSup U)))),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ unop (op (iSup U))),
      P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ gl ((i : (a : ↥V) → ↥(unop (op (iSup U)))) x)
⊢ P.toPrelocalPredicate (T := T).pred (T := T) gl

Tactic:
apply P.locality

Premises used: TopCat.LocalPredicate.locality