awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
h :
  ∀ (i : ι) (hi : (↑x : α) ∈ S i),
    iUnionLift S f hf T hT x ∈ t →
      ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
        f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x
⊢ iUnionLift S f hf T hT x ∈ t →
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x

Tactic:
rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩

Premises used: Set.mem_iUnion, Subtype.prop, Iff.mp
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
⊢ iUnionLift S f hf T hT x ∈ t →
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x

Tactic:
fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Subtype.val, rfl
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
h : ∀ (h : iUnionLift S f hf T hT x ∈ t), f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
⊢ iUnionLift S f hf T hT x ∈ t →
    ∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
      f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) ⋯ x_1 = inclusion (s := T) (t := iUnion S) hT x

Tactic:
refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
h : iUnionLift S f hf T hT x ∈ t
h₁ h₂ h₃ h₄ :
  ∀ (h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
⊢ f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t

Tactic:
rwa [iUnionLift_of_mem x hi] at h

Premises used: Set.iUnionLift_of_mem
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
y : α
hi : y ∈ S i
h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) ∈ t
hxy :
  inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) =
    inclusion (s := T) (t := iUnion S) hT x
⊢ y = (↑x : α)

Tactic:
congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
y : α
hi : y ∈ S i
h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) ∈ t
hxy :
  inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) =
    inclusion (s := T) (t := iUnion S) hT x
⊢ (↑x : α) ∈ S i

Tactic:
obtain rfl : y = x := congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val, rfl
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
y : α
hi : y ∈ S i
h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) ∈ t
hxy :
  inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) =
    inclusion (s := T) (t := iUnion S) hT x
hi₁ : (↑x : α) ∈ S i
⊢ f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi₁) ∈ t

Tactic:
obtain rfl : y = x := congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val, rfl
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
y : α
hi : y ∈ S i
h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) ∈ t
hxy :
  inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) y hi) =
    inclusion (s := T) (t := iUnion S) hT x
hi₁ : (↑x : α) ∈ S i
h₁ : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi₁) ∈ t
⊢ inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi₁) =
    inclusion (s := T) (t := iUnion S) hT x

Tactic:
obtain rfl : y = x := congr_arg Subtype.val hxy

Premises used: congr_arg, Subtype.val, rfl
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
h : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
hxy :
  inclusion (s := S i) (t := iUnion S) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) =
    inclusion (s := T) (t := iUnion S) hT x
h₁ h₂ h₃ h₄ : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
⊢ iUnionLift S f hf T hT x ∈ t

Tactic:
rwa [iUnionLift_of_mem x hi]

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)
T : Set α
hT : T ⊆ iUnion S
c : (↑T : Type u_1)
ci : (i : ι) → (↑(S i) : Type u_1)
hci : ∀ (i : ι), (↑(ci i) : α) = (↑c : α)
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
let : ∀ (i : ι) (hi : (↑c : α) ∈ S i), iUnionLift S f hf T hT c = cβ
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)
-- 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)
T : Set α
hT : T ⊆ iUnion S
c : (↑T : Type u_1)
ci : (i : ι) → (↑(S i) : Type u_1)
hci : ∀ (i : ι), (↑(ci i) : α) = (↑c : α)
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : (↑c : α) ∈ S i
⊢ ci i = Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑c : α) hi

Tactic:
have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)
-- 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)
T : Set α
hT : T ⊆ iUnion S
c : (↑T : Type u_1)
ci : (i : ι) → (↑(S i) : Type u_1)
hci : ∀ (i : ι), (↑(ci i) : α) = (↑c : α)
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : (↑c : α) ∈ S i
this : ci i = Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑c : α) hi
rw : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑c : α) hi) = cβ
rw₁ : f i (ci i) = cβ
rw₂ rw₃ : cβ = cβ
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
rw [iUnionLift_of_mem _ hi, ← this, h]

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)
T : Set α
hT' : T = iUnion S
u : (↑T : Type u_1) → (↑T : Type u_1)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)), u (inclusion (s := S i) (t := T) ⋯ x) = inclusion (s := S i) (t := T) ⋯ (ui i x)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
x : (↑T : Type u_1)
subst :
  ∀ (u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1))
    (hui :
      ∀ (i : ι) (x : (↑(S i) : Type u_1)),
        u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x))
    (x : (↑(iUnion S) : Type u_1)), iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
⊢ iUnionLift S f hf T ⋯ (u x) = uβ (iUnionLift S f hf T ⋯ x)

Tactic:
subst hT'
-- 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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
obtain : ∀ (i : ι) (hi : (↑x : α) ∈ S i), iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop

Premises used: Set.mem_iUnion, Subtype.prop, Iff.mp
-- 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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
rw : iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)

Tactic:
rw [iUnionLift_of_mem x hi, ← h i]

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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
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 i) (t := ⋃ (i : ι), S i) ⋯
        (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) hi)
⊢ x = inclusion (s := S i) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi)

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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
i : ι
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 i) (t := ⋃ (i : ι), S i) ⋯
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) hi)

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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
⊢ x = inclusion (s := S i) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi)

Tactic:
have : x = Set.inclusion (Set.subset_iUnion S i) ⟨x, 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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
this : x = inclusion (s := S i) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi)
rw : f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
| iUnionLift S f hf (iUnion S) ⋯ (u x)

Tactic:
rw [this, hui, iUnionLift_inclusion]

Premises used: Set.iUnionLift_inclusion
-- 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)
ui : (i : ι) → (↑(S i) : Type u_1) → (↑(S i) : Type u_1)
uβ : β → β
h : ∀ (i : ι) (x : (↑(S i) : Type u_1)), f i (ui i x) = uβ (f i x)
u : (↑(iUnion S) : Type u_1) → (↑(iUnion S) : Type u_1)
hui :
  ∀ (i : ι) (x : (↑(S i) : Type u_1)),
    u (inclusion (s := S i) (t := iUnion S) ⋯ x) = inclusion (s := S i) (t := iUnion S) ⋯ (ui i x)
x : (↑(iUnion S) : Type u_1)
i : ι
hi : (↑x : α) ∈ S i
this : x = inclusion (s := S i) (t := ⋃ (i : ι), S i) ⋯ (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi)
conv_lhs : iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
conv_lhs₁ :
  f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi)) =
    f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))

Tactic:
conv_lhs => rw [this, hui, iUnionLift_inclusion]

Premises used: Set.iUnionLift_inclusion
-- 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)
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)
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) ⋯ (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)
⊢ iUnionLift S f hf T ⋯ (op x y) = opβ (iUnionLift S f hf T ⋯ x) (iUnionLift S f hf T ⋯ y)

Tactic:
subst hT'
-- 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)
obtain :
  ∀ (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)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.1 x.prop

Premises used: Set.mem_iUnion, Subtype.prop, Iff.mp
-- 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
obtain :
  ∀ (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)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
obtain ⟨j, hj⟩ := Set.mem_iUnion.1 y.prop

Premises used: Set.mem_iUnion, Subtype.prop, Iff.mp
-- 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
rcases :
  ∀ (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)
⊢ iUnionLift S f hf (iUnion S) ⋯ (op x y) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
rcases dir i j with ⟨k, hik, hjk⟩
-- 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
rw :
  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) = opβ (iUnionLift S f hf (iUnion S) ⋯ x) (iUnionLift S f hf (iUnion S) ⋯ y)

Tactic:
rw [iUnionLift_of_mem x (hik hi), iUnionLift_of_mem y (hjk hj), ← h k]

Premises used: Set.iUnionLift_of_mem