awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
⊢ Eq.{u_2 + 1} (α := Set α) {b : α | b ∈ s ⊻ t ∧ b ≤ a} ({b : α | b ∈ s ∧ b ≤ a} ⊻ {b : α | b ∈ t ∧ b ≤ a})
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {b : α | b ∈ s ⊻ t ∧ b ≤ a} x ↔
    Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ b ≤ a} ⊻ {b : α | b ∈ t ∧ b ≤ a}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
⊢ Eq.{u_2 + 1} (α := Set α) {b : α | b ∈ s ⊼ t ∧ a ≤ b} ({b : α | b ∈ s ∧ a ≤ b} ⊼ {b : α | b ∈ t ∧ a ≤ b})
have h : ∀ (x : α),
  Membership.mem (γ := Set α) {b : α | b ∈ s ⊼ t ∧ a ≤ b} x ↔
    Membership.mem (γ := Set α) ({b : α | b ∈ s ∧ a ≤ b} ⊼ {b : α | b ∈ t ∧ a ≤ b}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
⊢ Eq (α := UpperSet α) (upperClosure (s ⊻ t)) (upperClosure s ⊔ upperClosure t)
have a : ∀ (a : α), a ∈ (↑(upperClosure (s ⊻ t)) : Set α) ↔ a ∈ (↑(upperClosure s ⊔ upperClosure t) : Set α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a
have a₁ : (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
s t : Set α
a : α
a₁ : (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a
have a₂ : ((∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a) → ∃ (a_2 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_2) ∧ a_2 ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
⊢ Eq (α := LowerSet α) (lowerClosure (s ⊼ t)) (lowerClosure s ⊓ lowerClosure t)
have a : ∀ (a : α), a ∈ (↑(lowerClosure (s ⊼ t)) : Set α) ↔ a ∈ (↑(lowerClosure s ⊓ lowerClosure t) : Set α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a
have a₁ : (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) →
  Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Sups (goal)
Goal:
α : Type u_2
inst : SemilatticeInf α
s t : Set α
a : α
a₁ :
  (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) →
    Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a
⊢ (∃ (a_1 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_1) ∧ a ≤ a_1) ↔
    Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a
have a₂ : Membership.mem (γ := LowerSet α) (lowerClosure s ⊓ lowerClosure t) a →
  ∃ (a_2 : α), (∃ a ∈ s, ∃ b ∈ t, a ⊓ b = a_2) ∧ a ≤ a_2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
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
x : (↑T : Type u_1)
i : ι
hx : (↑x : α) ∈ S i
⊢ iUnionLift S f hf T hT x = f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hx)
have obtain : ∀ (x : α) (hx : x ∈ T) (hx_1 : (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) : α) ∈ S i),
  iUnionLift S f hf T hT (Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) =
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ T) x hx) : α) hx_1)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x, hx
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
⊢ iUnionLift S f hf T hT ⁻¹' t =
    inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t
have h : ∀ (x : (↑T : Type u_1)),
  x ∈ iUnionLift S f hf T hT ⁻¹' t ↔
    x ∈ inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) sorry '' f i ⁻¹' t
Tactic: ext x
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
⊢ x ∈ iUnionLift S f hf T hT ⁻¹' t ↔
    x ∈ inclusion (s := T) (t := iUnion S) hT ⁻¹' ⋃ (i : ι), inclusion (s := S i) (t := iUnion S) ⋯ '' f i ⁻¹' t
have h : 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) sorry x_1 = inclusion (s := T) (t := iUnion S) hT x
Tactic: simp only [mem_preimage, mem_iUnion, mem_image]
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
⊢ 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
have h : 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) sorry x_1 = inclusion (s := T) (t := iUnion S) hT x
Tactic: constructor
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
h :
  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
have h₁ : (∃ (i : ι) (x_1 : (↑(S i) : Type u_1)),
    f i x_1 ∈ t ∧ inclusion (s := S i) (t := iUnion S) sorry x_1 = inclusion (s := T) (t := iUnion S) hT x) →
  iUnionLift S f hf T hT x ∈ t
Tactic: constructor
-- 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)
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : (↑T : Type u_1)
⊢ 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
have 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) sorry x_1 = inclusion (s := T) (t := iUnion S) hT x
Tactic: rcases mem_iUnion.1 (hT x.prop) with ⟨i, hi⟩
-- 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)
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
have h : ∀ (h : iUnionLift S f hf T hT x ∈ t), f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
Tactic: refine fun h => ⟨i, ⟨x, hi⟩, ?_, rfl⟩
-- 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)
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
⊢ f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi) ∈ t
have 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
Tactic: rwa [iUnionLift_of_mem x hi] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
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
⊢ iUnionLift S f hf T hT x ∈ t
have hi₁ : (↑x : α) ∈ S i
Tactic: obtain rfl : y = x := congr_arg Subtype.val hxy
Cleared hypotheses: y, hi, h, hxy
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
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
⊢ iUnionLift S f hf T hT x ∈ t
have h₁ : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi₁) ∈ t
Tactic: obtain rfl : y = x := congr_arg Subtype.val hxy
Cleared hypotheses: y, hi, h, hxy
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
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
⊢ iUnionLift S f hf T hT x ∈ t
have hxy₁ : inclusion (s := S i) (t := iUnion S) sorry (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
Cleared hypotheses: y, hi, h, hxy
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
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β
⊢ iUnionLift S f hf T hT c = cβ
have let : ∀ (i : ι) (hi : (↑c : α) ∈ S i), iUnionLift S f hf T hT c = cβ
Tactic: let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (hypothesis)
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
⊢ iUnionLift S f hf T hT c = cβ
have this : ci i = Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑c : α) hi
Tactic: have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
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
⊢ iUnionLift S f hf T hT c = cβ
have rw : f i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑c : α) hi) = cβ
Tactic: rw [iUnionLift_of_mem _ hi, ← this, h]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
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β
⊢ iUnionLift S f hf T hT c = cβ
have rw₁ : f i (ci i) = cβ
Tactic: rw [iUnionLift_of_mem _ hi, ← this, h]
-- Lean 4 proof step from Mathlib.Data.Set.UnionLift (goal)
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β
⊢ iUnionLift S f hf T hT c = cβ
have rw₂ : cβ = cβ
Tactic: rw [iUnionLift_of_mem _ hi, ← this, h]
-- 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
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)
⊢ iUnionLift S f hf T ⋯ (u x) = uβ (iUnionLift S f hf T ⋯ x)
have 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) sorry x) = inclusion (s := S i) (t := iUnion S) sorry (ui i x))
  (x : (↑(iUnion S) : Type u_1)), iUnionLift S f hf (iUnion S) sorry (u x) = uβ (iUnionLift S f hf (iUnion S) sorry x)
Tactic: subst hT'
Cleared hypotheses: T, hT', u, hui, x
-- 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)
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)
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
have obtain : ∀ (i : ι) (hi : (↑x : α) ∈ S i), iUnionLift S f hf (iUnion S) sorry (u x) = uβ (iUnionLift S f hf (iUnion S) sorry x)
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)
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
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
have rw : iUnionLift S f hf (iUnion S) sorry (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
Tactic: rw [iUnionLift_of_mem x hi, ← h i]
-- 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)
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)
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 i) (t := ⋃ (i : ι), S i) sorry
      (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ iUnion S) val property) : α) hi)
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)
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
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
have this : x = inclusion (s := S i) (t := ⋃ (i : ι), S i) sorry (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
-- 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)
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)
| iUnionLift S f hf (iUnion S) ⋯ (u x)
have rw : f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
Tactic: rw [this, hui, iUnionLift_inclusion]
-- 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)
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)
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
have conv_lhs : iUnionLift S f hf (iUnion S) sorry (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
Tactic: conv_lhs => rw [this, hui, iUnionLift_inclusion]
-- 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)
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))
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i (Subtype.mk (p := fun (x : α) ↦ x ∈ S i) (↑x : α) hi))
have 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))
Tactic: conv_lhs => rw [this, hui, iUnionLift_inclusion]