awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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
w :
  ∃ (V : Opens (↑X : Type u_2)) (_ : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U),
    (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ContinuousAt f x
have rcases : ∀ (V : Opens (↑X : Type u_2)) (m : (↑x : (↑X : Type u_2)) ∈ V) (i : V ⟶ U)
  (w :
    (X.continuousPrelocal T).pred (T := fun (x : (↑X : Type u_2)) ↦ T) (U := V) fun (x : ↥V) ↦
      f ((i : (a : ↥V) → ↥U) x)),
  ContinuousAt f x
Tactic: rcases w with ⟨V, m, i, w⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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 : Continuous.{u_2, u_3} (Y := T) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
⊢ ContinuousAt f x
have w₁ : ∀ (x : ↥V), ContinuousAt.{u_2, u_3} (Y := T) (fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)) x
Tactic: rw [continuous_iff_continuousAt] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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 f x
have 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)
Tactic: specialize w ⟨x, m⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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
have 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)
Tactic: refine ⟨P.locality f ?_, Q.locality f ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ (P.toPrelocalPredicate (T := T).and (T := T) (Q.toPrelocalPredicate (T := T))).pred (T := T) f
have 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)
Tactic: refine ⟨P.locality f ?_, Q.locality f ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)) (_ : (↑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)
have 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)
Tactic: have ⟨V, hV, i, h⟩ := w x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have h₁ : P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
Tactic: use V, hV, i
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)) (_ : (↑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)
have 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)
Tactic: have ⟨V, hV, i, h⟩ := w x
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have h₁ : Q.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
Tactic: use V, hV, i
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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)) (_ : (↑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)
have 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)
Tactic: specialize w (i x)
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases w with ⟨V', m', i', p⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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),
    P.pred (T := T) (U := V) fun (x : ↥V) ↦ f ((i : (a : ↥V) → ↥U) x)
have 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)
Tactic: specialize w x
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases w with ⟨V, m, i, p⟩
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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 : 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)
have 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)
Tactic: specialize p ⟨x.1, m⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases p with ⟨V', m', i', p'⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rcases ha x with ⟨Va, ma, ia, ha⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hop ha ⟨x, ma⟩ with ⟨W, sa, hx, hw⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rcases ha x with ⟨Va, ma, ia, ha⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases hb x with ⟨Vb, mb, ib, hb⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (goal)
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)
⊢ ∃ (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)
have 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)) sorry) : (↑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: rcases hop ha hb ⟨x, ma, mb⟩ with ⟨W, sa, sb, hx, hw⟩
-- Lean 4 proof step from Mathlib.Topology.Sheaves.LocalPredicate (hypothesis)
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)))
⊢ ∃! 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
have sf'_comp : (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)