awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι),
    ∀ x ∉ g i, p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
⊢ p f

Tactic:
induction_on_pi_of_choice (fun _ x s ↦ x ∉ s) (fun _ s ⟨x, hx⟩ ↦ ⟨x, hx, notMem_erase x s⟩) f
    h0 step

Premises used: Finset.induction_on_pi_of_choice, Membership.mem, Not
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → LinearOrder (α i)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    (∀ y ∈ g i, y < x) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
⊢ p f

Tactic:
induction_on_pi_of_choice (fun _ x s ↦ ∀ y ∈ s, y < x)
    (fun _ s hs ↦ ⟨s.max' hs, s.max'_mem hs, fun _ ↦ s.lt_max'_of_mem_erase_max' _⟩) f h0 step

Premises used: Finset.max'_mem, Finset.induction_on_pi_of_choice, Finset.max', And.intro, Exists.intro, Finset.lt_max'_of_mem_erase_max'
-- Module: Mathlib.Data.Finset.PiInduction
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Finite ι
inst_1 : DecidableEq ι
inst_2 : (i : ι) → DecidableEq (α i)
inst_3 : (i : ι) → LinearOrder (α i)
p : ((i : ι) → Finset (α i)) → Prop
f : (i : ι) → Finset (α i)
h0 : p fun (x : ι) ↦ ∅
step :
  ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i),
    (∀ y ∈ g i, x < y) → p g → p (update (β := fun (i : ι) ↦ Finset (α i)) g i (insert x (g i)))
⊢ p f

Tactic:
induction_on_pi_max (α := fun i ↦ (α i)ᵒᵈ) _ h0 step

Premises used: Finset.induction_on_pi_max
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : DecidableEq ι
j : ι
inst_1 : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (π := π) f g j = f j

Tactic:
simp [piecewise]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : (i : ι) → Decidable (Membership.mem (γ := Finset ι) ∅ i)
h : ∀ (i : ι), piecewise (π := π) ∅ f g i = g i
⊢ piecewise (π := π) ∅ f g = g

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : (i : ι) → Decidable (Membership.mem (γ := Finset ι) ∅ i)
i : ι
⊢ piecewise (π := π) ∅ f g i = g i

Tactic:
simp [piecewise]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
h : ∀ (x : ι), (↑s : Set ι).piecewise (β := π) f g x = s.piecewise (π := π) f g x
⊢ (↑s : Set ι).piecewise (β := π) f g = s.piecewise (π := π) f g

Tactic:
ext
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
x : ι
⊢ (↑s : Set ι).piecewise (β := π) f g x = s.piecewise (π := π) f g x

Tactic:
congr
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
hi : i ∈ s
⊢ s.piecewise (π := π) f g i = f i

Tactic:
simp [piecewise, hi]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
hi : i ∉ s
⊢ s.piecewise (π := π) f g i = g i

Tactic:
simp [piecewise, hi]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
f f' g g' : (i : ι) → π i
hf : ∀ i ∈ s, f i = f' i
hg : ∀ i ∉ s, g i = g' i
⊢ s.piecewise (π := π) f g = s.piecewise (π := π) f' g'

Tactic:
funext fun i => if_ctx_congr Iff.rfl (hf i) (hg i)

Premises used: if_ctx_congr, Iff.rfl, funext
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
h : i ≠ j
⊢ (insert j s).piecewise (π := π) f g i = s.piecewise (π := π) f g i

Tactic:
simp [piecewise, h]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
simp : (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g
⊢ (insert j s).piecewise (π := π) f g = update (β := π) (s.piecewise (π := π) f g) j (f j)

Tactic:
simp only [← piecewise_coe, ← Set.piecewise_insert]

Premises used: Set.piecewise_insert, Finset.piecewise_coe
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
classical : (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g
⊢ (insert j s).piecewise (π := π) f g = update (β := π) (s.piecewise (π := π) f g) j (f j)

Tactic:
classical simp only [← piecewise_coe, ← Set.piecewise_insert]

Premises used: Set.piecewise_insert, Finset.piecewise_coe
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
h : ∀ (x : ι), (↑(insert j s) : Set ι).piecewise (β := π) f g x = (insert j (↑s : Set ι)).piecewise (β := π) f g x
⊢ (↑(insert j s) : Set ι).piecewise (β := π) f g = (insert j (↑s : Set ι)).piecewise (β := π) f g

Tactic:
ext
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
x : ι
h : (↑(insert j s) : Set ι) = insert j (↑s : Set ι)
⊢ (↑(insert j s) : Set ι).piecewise (β := π) f g x = (insert j (↑s : Set ι)).piecewise (β := π) f g x

Tactic:
congr
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
inst_2 : (i : ι) → Decidable (i ∈ insert j s)
x : ι
⊢ (↑(insert j s) : Set ι) = insert j (↑s : Set ι)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
pos : ∀ (hi : i ∈ s), p (s.piecewise (π := π) f g i)
neg : ∀ (hi : i ∉ s), p (s.piecewise (π := π) f g i)
⊢ p (s.piecewise (π := π) f g i)

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (s.piecewise (π := π) f g i)

Tactic:
simpa [hi]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∉ s
⊢ p (s.piecewise (π := π) f g i)

Tactic:
simpa [hi]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst : DecidableEq ι
i : ι
rw : piecewise (π := π) (insert i ∅) f g = update (β := π) g i (f i)
rw₁ : update (β := π) (piecewise (π := π) ∅ f g) i (f i) = update (β := π) g i (f i)
rw₂ rw₃ : update (β := π) g i (f i) = update (β := π) g i (f i)
⊢ piecewise (π := π) {i} f g = update (β := π) g i (f i)

Tactic:
rw [← insert_empty_eq, piecewise_insert, piecewise_empty]

Premises used: Finset.piecewise_insert, LawfulSingleton.insert_empty_eq, Finset.piecewise_empty
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s t : Finset ι
inst : (i : ι) → Decidable (i ∈ s)
inst_1 : (i : ι) → Decidable (i ∈ t)
h : s ⊆ t
f₁ f₂ g : (a : ι) → π a
⊢ s.piecewise (π := π) (t.piecewise (π := π) f₁ f₂) g = s.piecewise (π := π) f₁ g

Tactic:
s.piecewise_congr (fun _i hi => piecewise_eq_of_mem _ _ _ (h hi)) fun _ _ => rfl

Premises used: Finset.piecewise_eq_of_mem, rfl, Finset.piecewise_congr
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
f₁ f₂ g : (a : ι) → π a
⊢ s.piecewise (π := π) (s.piecewise (π := π) f₁ f₂) g = s.piecewise (π := π) f₁ g

Tactic:
piecewise_piecewise_of_subset_left (Subset.refl _) _ _ _

Premises used: Finset.piecewise_piecewise_of_subset_left, Finset.Subset.refl
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s t : Finset ι
inst : (i : ι) → Decidable (i ∈ s)
inst_1 : (i : ι) → Decidable (i ∈ t)
h : t ⊆ s
f g₁ g₂ : (a : ι) → π a
⊢ s.piecewise (π := π) f (t.piecewise (π := π) g₁ g₂) = s.piecewise (π := π) f g₂

Tactic:
s.piecewise_congr (fun _ _ => rfl) fun _i hi => t.piecewise_eq_of_notMem _ _ (mt (@h _) hi)

Premises used: mt, Finset.piecewise_eq_of_notMem, rfl, Finset.piecewise_congr
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
f g₁ g₂ : (a : ι) → π a
⊢ s.piecewise (π := π) f (s.piecewise (π := π) g₁ g₂) = s.piecewise (π := π) f g₂

Tactic:
piecewise_piecewise_of_subset_right (Subset.refl _) f g₁ g₂

Premises used: Finset.Subset.refl, Finset.piecewise_piecewise_of_subset_right
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
β : Type u_3
inst : DecidableEq ι
f : ι → β
i : ι
v : β
⊢ update (β := fun (a : ι) ↦ β) f i v = piecewise (π := fun (x : ι) ↦ β) {i} (fun (x : ι) ↦ v) f

Tactic:
(piecewise_singleton (fun _ => v) _ _).symm

Premises used: Finset.piecewise_singleton, Eq.symm
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
h :
  ∀ (j : ι),
    update (β := π) (s.piecewise (π := π) f g) i v j =
      s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v)

Tactic:
ext j
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
h :
  ∀ (v : π j),
    update (β := π) (s.piecewise (π := π) f g) j v j =
      s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
h₁ :
  ∀ (hj : ¬j = i),
    update (β := π) (s.piecewise (π := π) f g) i v j =
      s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j

Tactic:
rcases em (j = i) with (rfl | hj)

Premises used: em, Eq, rfl
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
v : π j
pos :
  ∀ (hs : j ∈ s),
    update (β := π) (s.piecewise (π := π) f g) j v j =
      s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
neg :
  ∀ (hs : j ∉ s),
    update (β := π) (s.piecewise (π := π) f g) j v j =
      s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j
⊢ update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j

Tactic:
by_cases hs : j ∈ s
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
pos :
  ∀ (hs : j ∈ s),
    update (β := π) (s.piecewise (π := π) f g) i v j =
      s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
neg :
  ∀ (hs : j ∉ s),
    update (β := π) (s.piecewise (π := π) f g) i v j =
      s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j

Tactic:
by_cases hs : j ∈ s
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
v : π j
hs : j ∈ s
⊢ update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
j : ι
v : π j
hs : j ∉ s
⊢ update (β := π) (s.piecewise (π := π) f g) j v j =
    s.piecewise (π := π) (update (β := π) f j v) (update (β := π) g j v) j

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∈ s
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
v : π i
j : ι
hj : ¬j = i
hs : j ∉ s
⊢ update (β := π) (s.piecewise (π := π) f g) i v j =
    s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) j

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
rw :
  s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) (update (β := π) f i v) g
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) (update (β := π) f i v) g

Tactic:
rw [update_piecewise]

Premises used: Finset.update_piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) (update (β := π) f i v) g

Tactic:
s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..

Premises used: rfl, Finset.piecewise_congr, Function.update_of_ne
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
refine : ∀ (j : ι) (hj : j ∉ s), j ≠ i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) (update (β := π) f i v) g

Tactic:
refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..

Premises used: rfl, Finset.piecewise_congr, Function.update_of_ne
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
j : ι
hj : j ∉ s
⊢ j ≠ i

Tactic:
fun h => hj (h.symm ▸ hi)

Premises used: Eq.rec, Eq.symm, Not
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
j : ι
hj : j ∉ s
⊢ j ≠ i

Tactic:
exact fun h => hj (h.symm ▸ hi)
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
rw :
  s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) f (update (β := π) g i v)
⊢ update (β := π) (s.piecewise (π := π) f g) i v = s.piecewise (π := π) f (update (β := π) g i v)

Tactic:
rw [update_piecewise]

Premises used: Finset.update_piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) f (update (β := π) g i v)

Tactic:
s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl

Premises used: rfl, Finset.piecewise_congr, Function.update_of_ne
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
refine : ∀ (j : ι) (hj : j ∈ s), j ≠ i
⊢ s.piecewise (π := π) (update (β := π) f i v) (update (β := π) g i v) = s.piecewise (π := π) f (update (β := π) g i v)

Tactic:
refine s.piecewise_congr (fun j hj => update_of_ne ?_ ..) fun _ _ => rfl

Premises used: rfl, Finset.piecewise_congr, Function.update_of_ne
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
fun h => hi (h ▸ hj)

Premises used: Eq.rec, Not
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
inst_1 : DecidableEq ι
i : ι
hi : i ∉ s
v : π i
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
exact fun h => hi (h ▸ hj)
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
h : ∀ (i : ι), s.piecewise (π := π) f f i = f i
⊢ s.piecewise (π := π) f f = f

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
pos : ∀ (h : i ∈ s), s.piecewise (π := π) f f i = f i
neg : ∀ (h : i ∉ s), s.piecewise (π := π) f f i = f i
⊢ s.piecewise (π := π) f f i = f i

Tactic:
by_cases h : i ∈ s
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∈ s
⊢ s.piecewise (π := π) f f i = f i

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f : (i : ι) → π i
inst : (j : ι) → Decidable (j ∈ s)
i : ι
h : i ∉ s
⊢ s.piecewise (π := π) f f i = f i

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : (i : ι) → Decidable (Membership.mem (γ := Finset ι) univ i)
f g : (i : ι) → π i
h : ∀ (i : ι), piecewise (π := π) univ f g i = f i
⊢ piecewise (π := π) univ f g = f

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : (i : ι) → Decidable (Membership.mem (γ := Finset ι) univ i)
f g : (i : ι) → π i
i : ι
⊢ piecewise (π := π) univ f g i = f i

Tactic:
simp [piecewise]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
s : Finset ι
inst_2 : (i : ι) → Decidable (i ∈ s)
inst_3 : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
h : ∀ (i : ι), sᶜ.piecewise (π := π) f g i = s.piecewise (π := π) g f i
⊢ sᶜ.piecewise (π := π) f g = s.piecewise (π := π) g f

Tactic:
ext i
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
s : Finset ι
inst_2 : (i : ι) → Decidable (i ∈ s)
inst_3 : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
i : ι
⊢ sᶜ.piecewise (π := π) f g i = s.piecewise (π := π) g f i

Tactic:
simp [piecewise]

Premises used: Finset.piecewise
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
π : ι → Sort u_2
inst : Fintype ι
inst_1 : DecidableEq ι
i : ι
f g : (i : ι) → π i
rw : piecewise (π := π) {i}ᶜ f g = update (β := π) f i (g i)
rw₁ : piecewise (π := π) {i} g f = update (β := π) f i (g i)
rw₂ rw₃ : update (β := π) f i (g i) = update (β := π) f i (g i)
⊢ (erase univ i).piecewise (π := π) f g = update (β := π) f i (g i)

Tactic:
rw [← compl_singleton, piecewise_compl, piecewise_singleton]

Premises used: Finset.compl_singleton, Finset.piecewise_compl, Finset.piecewise_singleton
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
rw : (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'
⊢ s.piecewise (π := π) f g ∈ t.pi (α := π) t'

Tactic:
rw [← piecewise_coe]

Premises used: Finset.piecewise_coe
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
⊢ (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'

Tactic:
Set.piecewise_mem_pi (↑s) hf hg

Premises used: Set.piecewise_mem_pi
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
⊢ (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'

Tactic:
exact Set.piecewise_mem_pi (↑s) hf hg

Premises used: Set.piecewise_mem_pi
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi (α := π) t'
hg : g ∈ t.pi (α := π) t'
classical classical₁ classical₂ classical₃ : (↑s : Set ι).piecewise (β := π) f g ∈ t.pi (α := π) t'
⊢ s.piecewise (π := π) f g ∈ t.pi (α := π) t'

Tactic:
classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

Premises used: Set.piecewise_mem_pi, Finset.piecewise_coe
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g h : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : f ≤ h
hg : g ≤ h
⊢ s.piecewise (π := π) f g ≤ h

Tactic:
fun x =>
  piecewise_cases s f g (· ≤ h x) (hf x) (hg x)

Premises used: LE.le, Finset.piecewise_cases
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g h : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : h ≤ f
hg : h ≤ g
⊢ h ≤ s.piecewise (π := π) f g

Tactic:
fun x =>
  piecewise_cases s f g (fun y => h x ≤ y) (hf x) (hg x)

Premises used: LE.le, Finset.piecewise_cases
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
pos : ∀ (hx : x ∈ s), s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
neg : ∀ (hx : x ∉ s), s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x
⊢ s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∈ s
⊢ s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Piecewise
Goal:
ι : Type u_1
s : Finset ι
inst : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst_1 : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
hx : x ∉ s
⊢ s.piecewise (π := π) f g x ≤ s.piecewise (π := π) f' g' x

Tactic:
simp [*]