awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
x : ↥U
V : Opens (↑X : Type u_2)
m : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
w : ∀ (x : ↥V), ContinuousAt.{u_2, u_3} (Y := T) (fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)) x
⊢ ContinuousAt.{u_2, u_3} (Y := T) (fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x))
    (Subtype.mk (p := fun (x : (↑X : Type u_2)) ↦ x ∈ V) (↑x : (↑X : Type u_2)) m)

Tactic:
specialize w ⟨x, m⟩

Premises used: Subtype.mk, Subtype.val
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_2) → Type u_1
T : Type u_3
inst : TopologicalSpace T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T
x : ↥U
V : Opens (↑X : Type u_2)
m : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
w :
  ContinuousAt.{u_2, u_3} (Y := T) (fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x))
    (Subtype.mk (p := fun (x : (↑X : Type u_2)) ↦ x ∈ V) (↑x : (↑X : Type u_2)) m)
⊢ ContinuousAt f x

Tactic:
simpa using (Opens.isOpenEmbedding_of_le i.le).continuousAt_iff.1 w

Premises used: Quiver.Hom.le, Topology.IsOpenEmbedding.continuousAt_iff, Iff.mp, TopologicalSpace.Opens.isOpenEmbedding_of_le
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) f

Tactic:
⟨P.locality f ?_, Q.locality f ?_⟩

Premises used: And.intro, TopCat.LocalPredicate.locality
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
refine_1 :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
refine_2 :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) f

Tactic:
refine ⟨P.locality f ?_, Q.locality f ?_⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
refine_1 :
  ∀ (V : Opens (↑X : Type u_2)) (hV : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U)
    (h :
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
have ⟨V, hV, i, h⟩ := w x
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
V : Opens (↑X : Type u_2)
hV : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
h :
  (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V) fun (x : ↥V) ↦
    f ((i : (a : ↥V) → ↥U) x)
h₁ : P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
use V, hV, i
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
refine_2 :
  ∀ (V : Opens (↑X : Type u_2)) (hV : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U)
    (h :
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
have ⟨V, hV, i, h⟩ := w x
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
V : Opens (↑X : Type u_2)
hV : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
h :
  (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V) fun (x : ↥V) ↦
    f ((i : (a : ↥V) → ↥U) x)
h₁ : Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
use V, hV, i
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
V : Opens (↑X : Type u_2)
hV : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
h :
  (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V) fun (x : ↥V) ↦
    f ((i : (a : ↥V) → ↥U) x)
⊢ P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
V : Opens (↑X : Type u_2)
hV : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
h :
  (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V) fun (x : ↥V) ↦
    f ((i : (a : ↥V) → ↥U) x)
⊢ Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P Q : LocalPredicate T
U : Opens (↑X : Type u_2)
f : (x : ↥U) → T (↑x : (↑X : Type u_2))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
      (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V)
        fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥U
V : Opens (↑X : Type u_2)
hV : (↑x : (↑X : Type u_2)) ∈ V
i : V ⟶ U
h :
  (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) (U := V) fun (x : ↥V) ↦
    f ((i : (a : ↥V) → ↥U) x)
⊢ P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
exacts [h.1, h.2]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
V U : Opens (↑X : Type u_3)
i : V ⟶ U
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U),
      P.pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
x : ↥V
⊢ ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type u_3)) ∈ V_1) (i : V_1 ⟶ U),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥U) x)

Tactic:
specialize w (i x)

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
V U : Opens (↑X : Type u_3)
i : V ⟶ U
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥V
w :
  ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type u_3)) ∈ V_1) (i : V_1 ⟶ U),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦ f ((i : (a : ↥V_1) → ↥U) x)
rcases :
  ∀ (V' : Opens (↑X : Type u_3)) (m' : (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type u_3)) ∈ V') (i' : V' ⟶ U)
    (p : P.pred (T := T) (U := V') fun (x : ↥V') ↦ f ((i' : (a : ↥V') → ↥U) x)),
    ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
      P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
        (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
          ((i_1 : (a : ↥V_1) → ↥V) x)
⊢ ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
      (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
        ((i_1 : (a : ↥V_1) → ↥V) x)

Tactic:
rcases w with ⟨V', m', i', p⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
V U : Opens (↑X : Type u_3)
i : V ⟶ U
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥V
V' : Opens (↑X : Type u_3)
m' : (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type u_3)) ∈ V'
i' : V' ⟶ U
p : P.pred (T := T) (U := V') fun (x : ↥V') ↦ f ((i' : (a : ↥V') → ↥U) x)
⊢ ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
      (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
        ((i_1 : (a : ↥V_1) → ↥V) x)

Tactic:
⟨V ⊓ V', ⟨x.2, m'⟩, V.infLELeft _, P.res (V.infLERight V') _ p⟩

Premises used: TopCat.PrelocalPredicate.res, And.intro, Exists.intro, TopologicalSpace.Opens.infLELeft, TopologicalSpace.Opens.infLERight, Min.min, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
V U : Opens (↑X : Type u_3)
i : V ⟶ U
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥V
V' : Opens (↑X : Type u_3)
m' : (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type u_3)) ∈ V'
i' : V' ⟶ U
p : P.pred (T := T) (U := V') fun (x : ↥V') ↦ f ((i' : (a : ↥V') → ↥U) x)
⊢ ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
      (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
        ((i_1 : (a : ↥V_1) → ↥V) x)

Tactic:
exact ⟨V ⊓ V', ⟨x.2, m'⟩, V.infLELeft _, P.res (V.infLERight V') _ p⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
w :
  ∀ (x : ↥U),
    ∃ (V : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U),
      ∀ (x : ↥V),
        ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
          P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
            (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
              ((i_1 : (a : ↥V_1) → ↥V) x)
x : ↥U
⊢ ∃ (V : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U),
    ∀ (x : ↥V),
      ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
        P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
          (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
            ((i_1 : (a : ↥V_1) → ↥V) x)

Tactic:
specialize w x
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥U
w :
  ∃ (V : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U),
    ∀ (x : ↥V),
      ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
        P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
          (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
            ((i_1 : (a : ↥V_1) → ↥V) x)
rcases :
  ∀ (V : Opens (↑X : Type u_3)) (m : (↑x : (↑X : Type u_3)) ∈ V) (i : V ⟶ U)
    (p :
      ∀ (x : ↥V),
        ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
          P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
            (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
              ((i_1 : (a : ↥V_1) → ↥V) 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) ↦ f ((i : (a : ↥V) → ↥U) 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) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
rcases w with ⟨V, m, i, p⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥U
V : Opens (↑X : Type u_3)
m : (↑x : (↑X : Type u_3)) ∈ V
i : V ⟶ U
p :
  ∀ (x : ↥V),
    ∃ (V_1 : Opens (↑X : Type u_3)) (_ : (↑x : (↑X : Type u_3)) ∈ V_1) (i_1 : V_1 ⟶ V),
      P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
        (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
          ((i_1 : (a : ↥V_1) → ↥V) x)
⊢ ∃ (V_1 : Opens (↑X : Type u_3)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ V) (↑x : (↑X : Type u_3)) m) : (↑X : Type u_3)) ∈ V_1) (i_1 :
    V_1 ⟶ V),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
      (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
        ((i_1 : (a : ↥V_1) → ↥V) x)

Tactic:
specialize p ⟨x.1, m⟩

Premises used: Subtype.mk, Subtype.val
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥U
V : Opens (↑X : Type u_3)
m : (↑x : (↑X : Type u_3)) ∈ V
i : V ⟶ U
p :
  ∃ (V_1 : Opens (↑X : Type u_3)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ V) (↑x : (↑X : Type u_3)) m) : (↑X : Type u_3)) ∈ V_1) (i_1 :
    V_1 ⟶ V),
    P.pred (T := T) (U := V_1) fun (x : ↥V_1) ↦
      (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
        ((i_1 : (a : ↥V_1) → ↥V) x)
rcases :
  ∀ (V' : Opens (↑X : Type u_3))
    (m' : (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ V) (↑x : (↑X : Type u_3)) m) : (↑X : Type u_3)) ∈ V')
    (i' : V' ⟶ V)
    (p' :
      P.pred (T := T) (U := V') fun (x : ↥V') ↦
        (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
          ((i' : (a : ↥V') → ↥V) 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) ↦ f ((i : (a : ↥V) → ↥U) 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) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
rcases p with ⟨V', m', i', p'⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥U
V : Opens (↑X : Type u_3)
m : (↑x : (↑X : Type u_3)) ∈ V
i : V ⟶ U
V' : Opens (↑X : Type u_3)
m' : (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ V) (↑x : (↑X : Type u_3)) m) : (↑X : Type u_3)) ∈ V'
i' : V' ⟶ V
p' :
  P.pred (T := T) (U := V') fun (x : ↥V') ↦
    (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
      ((i' : (a : ↥V') → ↥V) 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) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
⟨V', m', i' ≫ i, p'⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T_1 : (↑X : Type u_3) → Type u_1
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
x : ↥U
V : Opens (↑X : Type u_3)
m : (↑x : (↑X : Type u_3)) ∈ V
i : V ⟶ U
V' : Opens (↑X : Type u_3)
m' : (↑(Subtype.mk (p := fun (x : (↑X : Type u_3)) ↦ x ∈ V) (↑x : (↑X : Type u_3)) m) : (↑X : Type u_3)) ∈ V'
i' : V' ⟶ V
p' :
  P.pred (T := T) (U := V') fun (x : ↥V') ↦
    (fun (x : ↥V) ↦ (f ((i : (a : ↥V) → ↥U) x) : T (↑((i : (a : ↥V) → ↥U) x) : (↑X : Type ?u.8860))))
      ((i' : (a : ↥V') → ↥V) 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) ↦ f ((i : (a : ↥V) → ↥U) x)

Tactic:
exact ⟨V', m', i' ≫ i, p'⟩
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
h : P.pred (T := T) f
x : ↥U
⊢ P.pred (T := T) f

Tactic:
h
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_3) → Type u_2
P : PrelocalPredicate T
U : Opens (↑X : Type u_3)
f : (x : ↥U) → T (↑x : (↑X : Type u_3))
h : P.pred (T := T) f
x : ↥U
⊢ P.pred (T := T) (U := U) fun (x : ↥U) ↦ f ((𝟙 U : (a : ↥U) → ↥U) x)

Tactic:
convert! h
-- 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 : P.sheafify (T := T).toPrelocalPredicate (T := T).pred (T := T) a
x : ↥U
rcases :
  ∀ (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)),
    ∃ (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)
⊢ ∃ (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:
rcases ha x with ⟨Va, ma, ia, ha⟩
-- 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)
rcases :
  ∀ (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)
⊢ ∃ (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:
rcases hop ha ⟨x, ma⟩ with ⟨W, sa, hx, hw⟩

Premises used: Subtype.mk, Subtype.val
-- 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:
⟨W, hx, sa ≫ ia, hw⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp