awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.UnionLift
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
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) ⋯
        (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ⋯)
⊢ x = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑x : α) ⋯)

Tactic:
cases x
-- Module: Mathlib.Data.Set.UnionLift
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)
y : (↑(iUnion S) : Type u_1)
i j : ι
hj : (↑y : α) ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
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) ⋯
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Set.UnionLift
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 : α) ⋯)

Tactic:
have hx : x = Set.inclusion (Set.subset_iUnion S k) ⟨x, hik hi⟩ := by
    cases x
    rfl
-- Module: Mathlib.Data.Set.UnionLift
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 : α) ⋯)
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) ⋯
        (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ⋯)
⊢ y = inclusion (s := S k) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑y : α) ⋯)

Tactic:
cases y
-- Module: Mathlib.Data.Set.UnionLift
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 : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
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 : α) ⋯)
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) ⋯
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S k) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) ⋯)

Tactic:
rfl
-- Module: Mathlib.Data.Set.UnionLift
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 : α) ⋯)

Tactic:
have hy : y = Set.inclusion (Set.subset_iUnion S k) ⟨y, hjk hj⟩ := by
    cases y
    rfl
-- Module: Mathlib.Data.Set.UnionLift
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 : α) ⋯)
⊢ (↑(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

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
-- Module: Mathlib.Data.Set.UnionLift
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
rw :
  f k
    (Subtype.mk (p := fun (x : α) ↦ x ∈ S k)
      (↑(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 : α) ⋯))) :
        α)
      hxy)
| iUnionLift S f hf (iUnion S) ⋯ (op x y)

Tactic:
rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

Premises used: Set.iUnionLift_of_mem
-- Module: Mathlib.Data.Set.UnionLift
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 : α) ⋯))
conv_lhs₁ :
  f k
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S k)
        (↑(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 : α) ⋯))) :
          α)
        hxy) =
    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 : α) ⋯))

Tactic:
conv_lhs => rw [hx, hy, ← hopi, iUnionLift_of_mem _ hxy]

Premises used: Set.iUnionLift_of_mem
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort 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
i : ι
x : (↑(S i) : Type u_1)
⊢ liftCover S f hf hS (↑x : α) = f i x

Tactic:
iUnionLift_mk x _

Premises used: Set.iUnionLift_mk, Set.liftCover
-- Module: Mathlib.Data.Set.UnionLift
Goal:
α : Type u_1
ι : Sort u_3
β : Sort 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
i : ι
x : α
hx : x ∈ S i
⊢ liftCover S f hf hS x = f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) x hx)

Tactic:
iUnionLift_of_mem ⟨x, mem_univ x⟩ hx

Premises used: Set.iUnionLift_of_mem, Subtype.mk, Set.liftCover, Set.mem_univ
-- Module: Mathlib.Data.Set.UnionLift
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 β
change :
  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)
⊢ liftCover S f hf hS ⁻¹' 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 = _

Premises used: Set.univ, Function.comp, Subtype.mk, Eq.subset, Set.mem_univ, Eq.symm, Set.iUnionLift
-- Module: Mathlib.Data.Set.UnionLift
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 β
rw :
  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)
⊢ 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)

Tactic:
rw [preimage_comp, preimage_iUnionLift]

Premises used: Set.preimage_comp, Set.preimage_iUnionLift
-- Module: Mathlib.Data.Set.UnionLift
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 β
h :
  ∀ (x : α),
    Membership.mem (γ := 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)
        x ↔
      Membership.mem (γ := Set α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t) x
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Data.Set.UnionLift
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 β
x : α
⊢ Membership.mem (γ := 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)
      x ↔
    Membership.mem (γ := Set α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ S i) '' f i ⁻¹' t) x

Tactic:
simp
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
⊢ (↑(↑p : Set B) : Type u_2) = ↥p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
q : ↥p → Prop
⊢ (∃ (x : ↥p), q x) ↔ ∃ (x : B), ∃ (h : x ∈ p), q (Subtype.mk (p := fun (x : B) ↦ x ∈ p) x h)

Tactic:
SetCoe.exists

Premises used: SetCoe.exists
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
q : ↥p → Prop
⊢ (∀ (x : ↥p), q x) ↔ ∀ (x : B) (h : x ∈ p), q (Subtype.mk (p := fun (x : B) ↦ x ∈ p) x h)

Tactic:
SetCoe.forall

Premises used: SetCoe.forall
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A) SetLike.coe

Tactic:
fun _ _ h =>
  SetLike.coe_injective' h

Premises used: SetLike.coe_injective', Function.Injective
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ (↑p : Set B) = (↑q : Set B) ↔ p = q

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, SetLike.coe_injective
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ (↑p : Set B) ≠ (↑q : Set B) ↔ p ≠ q

Tactic:
coe_injective.ne_iff

Premises used: Function.Injective.ne_iff, SetLike.coe_injective
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
h : (↑p : Set B) = (↑q : Set B)
⊢ p = q

Tactic:
coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ p = q ↔ (↑p : Set B) = (↑q : Set B)

Tactic:
coe_set_eq.symm

Premises used: SetLike.coe_set_eq, Iff.symm
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
h : ∀ (x : B), x ∈ p ↔ x ∈ q
⊢ p = q

Tactic:
coe_injective <| Set.ext h

Premises used: Set.ext, SetLike.coe_injective
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q

Tactic:
coe_injective.eq_iff.symm.trans Set.ext_iff

Premises used: Function.Injective.eq_iff, SetLike.coe_injective, Iff.trans, Set.ext_iff, Iff.symm
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
x : B
⊢ x ∈ (↑p : Set B) ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
x y : ↥p
⊢ (↑x : B) = (↑y : B) ↔ x = y

Tactic:
Subtype.ext_iff.symm

Premises used: Subtype.ext_iff, Iff.symm
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
x : ↥p
⊢ (↑x : B) ∈ p

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
s : Set B
hp : s ⊆ (↑p : Set B)
x : B
hx : x ∈ s
⊢ x ∈ p

Tactic:
hp hx
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
p : A
x : ↥p
hx : (↑x : B) ∈ p
⊢ Subtype.mk (p := fun (x : B) ↦ x ∈ p) (↑x : B) hx = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
a : A
⊢ {b : B | b ∈ a} = (↑a : Set B)

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.SetLike.Basic
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
obtain : ∀ (s : B) (hs : s ∈ S), b ∈ S
⊢ b ∈ S

Tactic:
obtain ⟨s, hs⟩ := nonempty_subtype.mp h

Premises used: nonempty_subtype, Iff.mp
-- Module: Mathlib.Data.SetLike.Basic
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 s : B
hs : s ∈ S
⊢ b ∈ S

Tactic:
simpa [Subsingleton.elim b s]

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
i : SetLike A B
inst : LE A
inst_1 : OrderTop A
s : A
hs : s ≠ ⊤
h_top : (↑⊤ : Set B) = Set.univ
⊢ ∃ (b : B), ¬b ∈ s

Tactic:
simpa [-SetLike.coe_set_eq, SetLike.ext'_iff, h_top, Set.ne_univ_iff_exists_notMem] using hs

Premises used: Set.ne_univ_iff_exists_notMem, SetLike.ext'_iff, SetLike.coe_set_eq
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
⊢ IsConcreteLE A B

Tactic:
letI := PartialOrder.ofSetLike A B; { coe_subset_coe' := Iff.rfl }

Premises used: Iff.rfl, IsConcreteLE.mk
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : LE A
inst_2 : IsConcreteLE A B
S T : A
⊢ (↑S : Set B) ⊆ (↑T : Set B) ↔ S ≤ T

Tactic:
IsConcreteLE.coe_subset_coe'

Premises used: IsConcreteLE.coe_subset_coe'
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : LE A
inst_2 : IsConcreteLE A B
S T : A
⊢ S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T

Tactic:
simp [← coe_subset_coe, Set.subset_def]

Premises used: Set.subset_def, SetLike.coe_subset_coe
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : LE A
inst_2 : IsConcreteLE A B
p q : A
⊢ ¬p ≤ q ↔ ∃ (x : B), x ∈ p ∧ ¬x ∈ q

Tactic:
simpa [← coe_subset_coe] using Set.not_subset

Premises used: SetLike.coe_subset_coe, Set.not_subset
-- Module: Mathlib.Data.SetLike.Basic
Goal:
A : Type u_1
B : Type u_2
inst : SetLike A B
inst_1 : Preorder A
inst_2 : IsConcreteLE A B
⊢ Monotone.{u_1, u_2} (α := A) SetLike.coe

Tactic:
fun _ _ => coe_subset_coe.mpr

Premises used: Iff.mpr, Monotone, SetLike.coe_subset_coe
-- Module: Mathlib.Data.SetLike.Basic
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
rw₂ : S ≤ T ∧ (↑S : Set B) ≠ (↑T : Set B) ↔ S ≤ T ∧ S ≠ T
rw₃ rw₄ : S ≤ T ∧ S ≠ T ↔ S ≤ T ∧ S ≠ T
⊢ (↑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]

Premises used: lt_iff_le_and_ne, SetLike.coe_ne_coe, SetLike.coe_subset_coe, ssubset_iff_subset_ne