awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
T : Set α
hT' : T = iUnion S
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
op : (↑T : Type u_1) → (↑T : Type u_1) → (↑T : Type u_1)
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := T) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := T) ⋯ x) (inclusion (s := S i) (t := T) ⋯ y)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
x y : (↑T : Type u_1)
⊢ iUnionLift S f hf T ⋯ (op x y) = opβ (iUnionLift S f hf T ⋯ x) (iUnionLift S f hf T ⋯ y)
have subst : ∀ (op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1))
  (hopi :
    ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
      inclusion (s := S i) (t := iUnion S) sorry (opi i x y) =
        op (inclusion (s := S i) (t := iUnion S) sorry x) (inclusion (s := S i) (t := iUnion S) sorry y))
  (x y : (↑(iUnion S) : Type u_1)),
  iUnionLift S f hf (iUnion S) sorry (op x y) = opβ (iUnionLift S f hf (iUnion S) sorry x) (iUnionLift S f hf (iUnion S) sorry y)
Tactic: subst hT'
Cleared hypotheses: T, hT', op, hopi, x, y
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
have obtain : ∀ (i : ι) (hi : (↑x : α) ∈ S i),
  iUnionLift S f hf (iUnion S) sorry (op x y) = opβ (iUnionLift S f hf (iUnion S) sorry x) (iUnionLift S f hf (iUnion S) sorry y)
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
have obtain : ∀ (j : ι) (hj : (↑y : α) ∈ S j),
  iUnionLift S f hf (iUnion S) sorry (op x y) = opβ (iUnionLift S f hf (iUnion S) sorry x) (iUnionLift S f hf (iUnion S) sorry y)
Tactic: obtain ⟨j, hj⟩ := Set.mem_iUnion.1 y.prop
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
have rcases : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k),
  iUnionLift S f hf (iUnion S) sorry (op x y) = opβ (iUnionLift S f hf (iUnion S) sorry x) (iUnionLift S f hf (iUnion S) sorry y)
Tactic: rcases dir i j with ⟨k, hik, hjk⟩
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)
have rw : iUnionLift S f hf (iUnion S) sorry (op x y) =
  f k (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))
Tactic: rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
have mk : ∀ (val : α) (property : val ∈ iUnion S) (hi : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ∈ S i),
  Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property =
    inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) sorry)
Tactic: cases x
Cleared hypotheses: x, hi
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
have hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry)
Tactic: have hx : x = Set.inclusion (Set.subset_iUnion S k) ⟨x, hik hi⟩ := by
    cases x
    rfl
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
⊢ y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)
have mk : ∀ (val : α) (property : val ∈ iUnion S) (hj : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ∈ S j),
  Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property =
    inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) sorry)
Tactic: cases y
Cleared hypotheses: y, hj
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
have hy : y = inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry)
Tactic: have hy : y = Set.inclusion (Set.subset_iUnion S k) ⟨y, hjk hj⟩ := by
    cases y
    rfl
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
hy : y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
have hxy : (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry
        (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))) :
    α) ∈
  S k
Tactic: have hxy : (Set.inclusion (Set.subset_iUnion S k) (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩) : α) ∈ S k :=
    (opi k ⟨x, hik hi⟩ ⟨y, hjk hj⟩).prop
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
hy : y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)
hxy :
  (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯
          (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))) :
      α) ∈
    S k
| iUnionLift S f hf (iUnion S) ⋯ (op x y)
have rw : f k
  (Subtype.mk (p := fun (x : α) ↦ x ∈ S k)
    (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry
          (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))) :
      α)
    hxy)
Tactic: rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
hy : y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)
hxy :
  (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯
          (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))) :
      α) ∈
    S k
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
have conv_lhs : iUnionLift S f hf (iUnion S) sorry (op x y) =
  f k (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))
Tactic: conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
dir : Directed (fun (x1 x2 : Set α) ↦ x1 ≤ x2) S
opi : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
opβ : β → β → β
h : ∀ (i : ι) (x y : (↑(S i) : Type u_1)), f i (opi i x y) = opβ (f i x) (f i y)
op : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hopi :
  ∀ (i : ι) (x y : (↑(S i) : Type u_1)),
    inclusion (s := S i) (t := iUnion S) ⋯ (opi i x y) =
      op (inclusion (s := S i) (t := iUnion S) ⋯ x) (inclusion (s := S i) (t := iUnion S) ⋯ y)
x y : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
hx : x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
hy : y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)
hxy :
  (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯
          (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))) :
      α) ∈
    S k
conv_lhs :
  iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) =
    f k
      (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯))
have conv_lhs₁ : f k
    (Subtype.mk (p := fun (x : α) ↦ x ∈ S k)
      (↑(inclusion (s := S k) (t := ⋃ (i : ι), S i) sorry
            (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry)
              (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))) :
        α)
      hxy) =
  f k (opi k (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) sorry))
Tactic: conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
hS : iUnion S = univ
t : Set β
⊢ liftCover S f hf hS ⁻¹' t = ⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t
have change : Eq (α := Set α)
  ((iUnionLift S f hf univ sorry ∘ fun (a : α) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) a sorry) ⁻¹'
    t)
  (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t)
Tactic: change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
hS : iUnion S = univ
t : Set β
⊢ Eq (α := Set α)
    ((iUnionLift S f hf univ ⋯ ∘ fun (a : α) ↦
        Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) a ⋯) ⁻¹'
      t)
    (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t)
have rw : Eq (α := Set α)
  ((fun (a : α) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) a sorry) ⁻¹'
    inclusion (s := univ) (t := iUnion S) sorry ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) sorry '' f i ⁻¹' t)
  (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t)
Tactic: rw [preimage_comp, preimage_iUnionLift]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
Goal:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → (↑(S i) : Type u_1) → β
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ S j) x hxj)
hS : iUnion S = univ
t : Set β
⊢ Eq (α := Set α)
    ((fun (a : α) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) a ⋯) ⁻¹'
      inclusion (s := univ) (t := iUnion S) ⋯ ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t)
    (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t)
have h : ∀ (x : α),
  Membership.mem (γ := Set α)
      ((fun (a : α) ↦ Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) a sorry) ⁻¹'
        inclusion (s := univ) (t := iUnion S) sorry ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) sorry '' f i ⁻¹' t)
      x ↔
    Membership.mem (γ := Set α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
inst : Subsingleton B
S : A
h : Nonempty.{u_2 + 1} ↥S
b : B
⊢ b ∈ S
have obtain : ∀ (s : B) (hs : s ∈ S), b ∈ S
Tactic: obtain ⟨s, hs⟩ := nonempty_subtype.mp h
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
S T : A
⊢ (↑S : Set B) ⊂ (↑T : Set B) ↔ S < T
have rw : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S < T
Tactic: rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
S T : A
rw : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S < T
⊢ (↑S : Set B) ⊂ (↑T : Set B) ↔ S < T
have rw₁ : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
Tactic: rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]
-- Lean 4 proof step from Mathlib.Data.SetLike.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : PartialOrder A
inst_2 : IsConcreteLE A B
S T : A
rw : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S < T
rw₁ : (↑S : Set B) ⊆ (↑T : Set B) ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
⊢ (↑S : Set B) ⊂ (↑T : Set B) ↔ S < T
have rw₂ : S ≤ T ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
Tactic: rw [ssubset_iff_subset_ne, lt_iff_le_and_ne, coe_subset_coe, SetLike.coe_ne_coe]