awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
have refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
Tactic: classical
  refine s.induction ?_ ?_
  · simp
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Union (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
refine_1 : Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Disjoint (f i) t
⊢ Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
have refine_2 : ∀ (a : α) (s : Finset α),
  a ∉ s →
    (Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t) →
      (Disjoint ((insert a s).biUnion f) t ↔ ∀ i ∈ insert a s, Disjoint (f i) t)
Tactic: classical
  refine s.induction ?_ ?_
  · simp
  · intro i s his ih
    simp only [disjoint_union_left, biUnion_insert, forall_mem_insert, ih]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
⊢ updateFinset (π := π) x {i} y =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
have h : ∀ (j : ι),
  updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) : ι))
      j
Tactic: congr with j
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j
have pos : ∀ (hj : j = i),
  updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) : ι))
      j
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
pos :
  ∀ (hj : j = i),
    updateFinset (π := π) x {i} y j =
      update (β := π) x i
        (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
          π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
        j
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j
have neg : ∀ (hj : ¬j = i),
  updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) : ι))
      j
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π (↑i_1 : ι)
j : ι
hj : j = i
⊢ updateFinset (π := π) x {i} y j =
    update (β := π) x i
      (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) :
        π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯) : ι))
      j
have pos : updateFinset (π := π) x {i} y i =
  update (β := π) x i
    (y (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) :
      π (↑(Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry) : ι))
    i
Tactic: cases hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
⊢ update (β := π) x i y = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)
have h : ∀ (j : ι), update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
Tactic: congr with j
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
have pos : ∀ (hj : j = i),
  update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
pos :
  ∀ (hj : j = i),
    update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
have neg : ∀ (hj : ¬j = i),
  update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
Tactic: by_cases hj : j = i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update (β := π) x i y j = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) j
have pos : update (β := π) x i y i = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) i
Tactic: cases hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
i : ι
y : π i
⊢ update (β := π) x i y i = updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y) i
have pos : y =
  uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y
    (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i sorry)
Tactic: simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α) (fun (x : (i : ι) → π i) ↦ f (Function.updateFinset (π := π) x t y))
    (s \ (↑t : Set ι))
have refine : ∀ (x₁ x₂ : (i : ι) → π i) (h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i) (i : ι) (hi : i ∈ s),
  Function.updateFinset (π := π) x₁ t y i = Function.updateFinset (π := π) x₂ t y i
Tactic: refine fun x₁ x₂ h ↦ hf (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i
i : ι
hi : i ∈ s
⊢ Eq.{u_3 + 1} (α := π i) (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₁ i)
    (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₂ i)
have pos : ∀ (h : i ∈ t),
  Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : ι))
    (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Set ι
hf : DependsOn (α := π) f s
t : Finset ι
y : (i : ↥t) → π (↑i : ι)
x₁ x₂ : (i : ι) → π i
h : ∀ i ∈ s \ (↑t : Set ι), x₁ i = x₂ i
i : ι
hi : i ∈ s
pos :
  ∀ (h : i ∈ t),
    Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h) : ι))
      (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i h))
⊢ Eq.{u_3 + 1} (α := π i) (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₁ i)
    (if hi : i ∈ t then y (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i hi) else x₂ i)
have neg : i ∉ t → x₁ i = x₂ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_2
π : ι → Type u_3
inst : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn (α := π) f (↑s : Set ι)
i : ι
y : π i
⊢ DependsOn.{u_2, u_3, u_1} (α := π) (β := α) (fun (x : (i : ι) → π i) ↦ f (Function.update (β := π) x i y))
    (↑(s.erase i) : Set ι)
have simp_rw : DependsOn.{u_2, u_3, u_1} (α := π) (β := α)
  (fun (x : (i : ι) → π i) ↦ f (updateFinset (π := π) x {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) y)))
  ((↑s : Set ι) \ (↑{i} : Set ι))
Tactic: simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
have h : ∀ (i : ι),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have pos : ∀ (his : i ∈ s),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases his : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
pos :
  ∀ (his : i ∈ s),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have neg : ∀ (his : i ∉ s),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases his : i ∈ s
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have pos : ∀ (hit : i ∈ t),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
pos :
  ∀ (hit : i ∈ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have neg : ∀ (hit : i ∉ t),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have pos : ∀ (hit : i ∈ t),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
pos :
  ∀ (hit : i ∈ t),
    updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
      updateFinset (π := π) x (s ∪ t)
        ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
          (y, z))
        i
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have neg : ∀ (hit : i ∉ t),
  updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
Tactic: by_cases hit : i ∈ t
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have pos : Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i sorry) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i sorry) : ι))
  (if h : True ∨ True then
    (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι)) (y, z)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i sorry)
  else x i)
Tactic: simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∉ t
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have neg : Eq (α := π i) (y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i sorry) : ι))
  (if h : True ∨ False then
    (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι)) (y, z)
      (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i sorry)
  else x i)
Tactic: simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∉ s
hit : i ∈ t
⊢ updateFinset (π := π) (updateFinset (π := π) x s y) t z i =
    updateFinset (π := π) x (s ∪ t)
      ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z))
      i
have pos : Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i sorry) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i sorry) : ι))
  ((piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι)) (y, z)
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i sorry))
Tactic: simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
hst : Disjoint s t
e : ↥s ⊕ ↥t ≃ ↥(s ∪ t) := Finset.union s t hst
i : ι
his : i ∈ s
hit : i ∈ t
⊢ Eq (α := π i) (z (Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : π (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ t) i ⋯) : ι))
    (if h : True ∨ True then
      (piFinsetUnion π hst : (a : ((i : ↥s) → π (↑i : ι)) × ((i : ↥t) → π (↑i : ι))) → (i : ↥(s ∪ t)) → π (↑i : ι))
        (y, z) (Subtype.mk (p := fun (x : ι) ↦ x ∈ s ∪ t) i ⋯)
    else x i)
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s t : Finset ι
hst : s ⊆ t
x : (i : ι) → π i
y : (i : ↥t) → π (↑i : ι)
⊢ s.restrict (π := π) (updateFinset (π := π) x t y) = restrict₂ (π := π) hst y
have h : ∀ (i : ↥s), s.restrict (π := π) (updateFinset (π := π) x t y) i = restrict₂ (π := π) hst y i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
y : (i : ↥s) → π (↑i : ι)
⊢ s.restrict (π := π) (updateFinset (π := π) x s y) = y
have rw : restrict₂ (π := π) sorry y = y
Tactic: rw [restrict_updateFinset_of_subset subset_rfl]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
s : Finset ι
x : (i : ι) → π i
⊢ updateFinset (π := π) x s (s.restrict (π := π) x) = x
have h : ∀ (i : ι), updateFinset (π := π) x s (s.restrict (π := π) x) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π (↑i : ι)
i : ι
z : π i
hi : i ∉ s
⊢ update (β := π) (updateFinset (π := π) x s y) i z =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
have rw : updateFinset (π := π) (updateFinset (π := π) x s y) {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z) =
  updateFinset (π := π) x (s ∪ {i})
    ((piFinsetUnion π sorry :
        (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
      (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
Tactic: rw [update_eq_updateFinset, updateFinset_updateFinset]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π (↑i : ι)
i : ι
z : π i
hi : i ∉ s
rw :
  updateFinset (π := π) (updateFinset (π := π) x s y) {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
⊢ update (β := π) (updateFinset (π := π) x s y) i z =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
have rw₁ : updateFinset (π := π) x (s ∪ {i})
    ((piFinsetUnion π sorry :
        (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
      (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z)) =
  updateFinset (π := π) x (s ∪ {i})
    ((piFinsetUnion π sorry :
        (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
      (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
Tactic: rw [update_eq_updateFinset, updateFinset_updateFinset]
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
x : (i : ι) → π i
inst : DecidableEq ι
s : Finset ι
y : (i : ↥s) → π (↑i : ι)
i : ι
z : π i
hi : i ∉ s
rw :
  updateFinset (π := π) (updateFinset (π := π) x s y) {i} (uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
rw₁ :
  updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z)) =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
⊢ update (β := π) (updateFinset (π := π) x s y) i z =
    updateFinset (π := π) x (s ∪ {i})
      ((piFinsetUnion π ⋯ :
          (a : ((i : ↥s) → π (↑i : ι)) × ((i_1 : ↥{i}) → π (↑i_1 : ι))) → (i_1 : ↥(s ∪ {i})) → π (↑i_1 : ι))
        (y, uniqueElim (α := fun (i_1 : ↥{i}) ↦ π (↑i_1 : ι)) z))
have rw₂ : Disjoint s {i}
Tactic: rw [update_eq_updateFinset, updateFinset_updateFinset]