awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
f₁ : ∀ (i : ι) (hi : i ∈ s \ t) (a : α) (ha : a ∈ f i), a ∉ ⋃ x ∈ t, f x
⊢ Eq.{u_1 + 1} (α := Set α) ((⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i) (⋃ i ∈ s \ t, f i)

Tactic:
refine
    (biUnion_diff_biUnion_subset f s t).antisymm
      (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, ?_⟩)

Premises used: Iff.mpr, Set.biUnion_diff_biUnion_subset, Set.iUnion₂_subset, Set.mem_biUnion, And.left, Set.mem_diff, HasSubset.Subset.antisymm, And.intro
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
rw : ¬∃ (i : ι) (_ : i ∈ t), a ∈ f i
⊢ a ∉ ⋃ x ∈ t, f x

Tactic:
rw [mem_iUnion₂]

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False

Tactic:
(h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

Premises used: Disjoint.le_bot, Set.Mem, Ne.symm, ne_of_mem_of_not_mem, And.right, And.left, And.intro, Or.inl, Or.inr
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
s t : Set ι
f : ι → Set α
h : (s ∪ t).PairwiseDisjoint f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False

Tactic:
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩

Premises used: Disjoint.le_bot, Ne.symm, ne_of_mem_of_not_mem, And.right, And.left, And.intro, Or.inl, Or.inr
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_5
ι : Type u_6
s : Set ι
f : ι → Set α
h : s.PairwiseDisjoint f
x : (i : (↑s : Type u_6)) × (↑(f (↑i : ι)) : Type u_5)
⊢ (↑(((biUnionEqSigmaOfDisjoint (s := s) (f := f) h).symm :
            (a : (i : (↑s : Type u_6)) × (↑(f (↑i : ι)) : Type u_5)) → (↑(⋃ i ∈ s, f i) : Type u_5))
          x) :
      α) =
    (↑(x.snd (β := fun (i : (↑s : Type u_6)) ↦ (↑(f (↑i : ι)) : Type u_5))) : α)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_5
ι : Type u_6
s : Set ι
f : ι → Set α
h : s.PairwiseDisjoint f
x : (↑(⋃ i ∈ s, f i) : Type u_5)
⊢ (↑(Sigma.snd (β := fun (i : (↑s : Type u_6)) ↦ (↑(f (↑i : ι)) : Type u_5))
            ((biUnionEqSigmaOfDisjoint (s := s) (f := f) h :
                (a : (↑(⋃ i ∈ s, f i) : Type u_5)) → (i : (↑s : Type u_6)) × (↑(f (↑i : ι)) : Type u_5))
              x) :
          (↑(f
                (↑(Sigma.fst (β := fun (i : (↑s : Type u_6)) ↦ (↑(f (↑i : ι)) : Type u_5))
                      ((biUnionEqSigmaOfDisjoint (s := s) (f := f) h :
                          (a : (↑(⋃ i ∈ s, f i) : Type u_5)) → (i : (↑s : Type u_6)) × (↑(f (↑i : ι)) : Type u_5))
                        x)) :
                  ι)) :
            Type u_5)) :
      α) =
    (↑x : α)

Tactic:
simp [biUnionEqSigmaOfDisjoint]

Premises used: Set.biUnionEqSigmaOfDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]

Premises used: Function.onFun, not_imp_comm, Set.PairwiseDisjoint, Set.not_disjoint_iff_nonempty_inter, Set.Pairwise
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
rw :
  ∀ ⦃i : Set α⦄,
    i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → Set.Nonempty (α := Set α) ({i, insert a i} ∩ {j, insert a j}) → i = j
⊢ (𝒫 s).PairwiseDisjoint (α := Set (Set α)) fun (t : Set α) ↦ {t, insert a t}

Tactic:
rw [pairwiseDisjoint_iff]

Premises used: Set.pairwiseDisjoint_iff
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ insert a i = insert a j → i = j

Tactic:
have := insert_erase_invOn.2.injOn (notMem_subset hi ha) (notMem_subset hj ha)
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
this : insert a i = insert a j → i = j
⊢ Set.Nonempty (α := Set α) ({i, insert a i} ∩ {j, insert a j}) → i = j

Tactic:
aesop (add simp [Set.Nonempty, Set.subset_def])

Premises used: Set.subset_def, Set.Nonempty
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
i : ι
hi : i ∈ s
obtain : ∀ (a : α) (hai : a ∈ f i), i ∈ t
⊢ i ∈ t

Tactic:
obtain ⟨a, hai⟩ := h₁ i hi
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
obtain : ∀ (j : ι) (hj : j ∈ t) (haj : a ∈ f j), i ∈ t
⊢ i ∈ t

Tactic:
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)

Premises used: Set.mem_iUnion₂_of_mem, Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : (s ∪ t).PairwiseDisjoint f
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
rwa rwa₁ rwa₂ rwa₃ : j ∈ t
⊢ i ∈ t

Tactic:
rwa [h₀.eq (subset_union_left hi) (subset_union_right hj)
      (not_disjoint_iff.2 ⟨a, hai, haj⟩)]

Premises used: Iff.mpr, Set.subset_union_right, Set.not_disjoint_iff, Set.subset_union_left, And.intro, Exists.intro, Set.Pairwise.eq
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s t : Set ι
h₀ : Pairwise (Disjoint on f)
h₁ : ∀ i ∈ s, (f i).Nonempty
h : Subset.{u_1} (α := Set α) (⋃ i ∈ s, f i) (⋃ i ∈ t, f i)
⊢ s ⊆ t

Tactic:
Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion (h₀.set_pairwise _) h₁ h

Premises used: Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion, Pairwise.set_pairwise
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
h₀ : Pairwise (Disjoint on f)
h₁ : ∀ (i : ι), (f i).Nonempty
⊢ Injective.{u_2 + 1, u_1 + 1} (β := Set α) fun (s : Set ι) ↦ ⋃ i ∈ s, f i

Tactic:
fun _s _t h =>
  ((h₀.subset_of_biUnion_subset_biUnion fun _ _ => h₁ _) <| h.subset).antisymm <|
    (h₀.subset_of_biUnion_subset_biUnion fun _ _ => h₁ _) <| h.superset

Premises used: Pairwise.subset_of_biUnion_subset_biUnion, Eq.subset, HasSubset.Subset.antisymm, Function.Injective, Eq.superset
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
⊢ ∃! i : ι, i ∈ s ∧ y ∈ f i

Tactic:
existsUnique_of_exists_of_unique ?ex ?unique

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
ex : ∃ x ∈ s, y ∈ f x
unique : ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂
⊢ ∃! i : ι, i ∈ s ∧ y ∈ f i

Tactic:
refine existsUnique_of_exists_of_unique ?ex ?unique
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
⊢ ∃ x ∈ s, y ∈ f x

Tactic:
simpa only [mem_iUnion, exists_prop] using hy

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
i j : ι
his : i ∈ s
hi : y ∈ f i
hjs : j ∈ s
hj : y ∈ f j
⊢ i = j

Tactic:
h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

Premises used: Iff.mpr, Set.not_disjoint_iff, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : Membership.mem (γ := Set α) (⋃ i ∈ s, f i) y
i j : ι
his : i ∈ s
hi : y ∈ f i
hjs : j ∈ s
hj : y ∈ f j
⊢ i = j

Tactic:
exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

Premises used: Iff.mpr, Set.not_disjoint_iff, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
l : List α
r : α → α → Prop
hl : l.Nodup
h : Set.Pairwise {x : α | x ∈ l} r
⊢ Pairwise r l

Tactic:
hl.pairwise_of_forall_ne h

Premises used: List.Nodup.pairwise_of_forall_ne
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l : List α
inst : Std.Symm r
hl : Nodup.{u_1} (α := α) []
⊢ Set.Pairwise {a : α | Membership.mem (γ := List α) [] a} r ↔ Pairwise r []

Tactic:
simp
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : (a :: l).Nodup
⊢ Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)

Tactic:
?_
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l : List α
inst : Std.Symm r
hl : l.Nodup
cons :
  ∀ (a : α) (l : List α) (ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l) (hl : (a :: l).Nodup),
    Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
⊢ Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l

Tactic:
induction l with | nil => simp | cons a l ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : (a :: l).Nodup
⊢ ¬a ∈ l ∧ l.Nodup

Tactic:
rw [List.nodup_cons] at hl

Premises used: List.nodup_cons
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : ¬a ∈ l ∧ l.Nodup
⊢ ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)

Tactic:
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
    imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
-- Module: Mathlib.Data.Set.Pairwise.List
Goal:
α : Type u_1
r : α → α → Prop
l_1 : List α
inst : Std.Symm r
a : α
l : List α
ih : ∀ (hl : l.Nodup), Set.Pairwise {a : α | a ∈ l} r ↔ Pairwise r l
hl : ¬a ∈ l ∧ l.Nodup
this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
⊢ Set.Pairwise {a_1 : α | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)

Tactic:
simp [Set.setOf_or, Set.pairwise_insert_of_symmetric fun _ _ ↦ symm_of r, ih hl.2, and_comm,
    forall₂_congr this]

Premises used: and_comm, symm_of, Set.pairwise_insert_of_symmetric, forall₂_congr, And.right, Set.setOf_or
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) ∅ i)
h : ∀ (i : α), piecewise (β := δ) ∅ f g i = g i
⊢ piecewise (β := δ) ∅ f g = g

Tactic:
ext i
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) ∅ i)
i : α
⊢ piecewise (β := δ) ∅ f g i = g i

Tactic:
simp [piecewise]

Premises used: Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) univ i)
h : ∀ (i : α), piecewise (β := δ) univ f g i = f i
⊢ piecewise (β := δ) univ f g = f

Tactic:
ext i
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
f g : (i : α) → δ i
inst : (i : α) → Decidable (Membership.mem (γ := Set α) univ i)
i : α
⊢ piecewise (β := δ) univ f g i = f i

Tactic:
simp [piecewise]

Premises used: Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
j : α
inst : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (β := δ) f g j = f j

Tactic:
simp [piecewise]

Premises used: Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
simp :
  (fun (i : α) ↦ if i = j ∨ i ∈ s then f i else g i) =
    update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j)
⊢ (insert j s).piecewise (β := δ) f g = update (β := δ) (s.piecewise (β := δ) f g) j (f j)

Tactic:
simp +unfoldPartialApp only [piecewise, mem_insert_iff]

Premises used: Set.mem_insert_iff, Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
h :
  ∀ (i : α), (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
⊢ (fun (i : α) ↦ if i = j ∨ i ∈ s then f i else g i) =
    update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j)

Tactic:
ext i
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
pos :
  ∀ (h : i = j),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
neg :
  ∀ (h : ¬i = j),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
by_cases h : i = j
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
pos : (if j = j ∨ j ∈ s then f j else g j) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) j
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) j

Tactic:
simp
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
pos :
  ∀ (h' : i ∈ s),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
neg :
  ∀ (h' : ¬i ∈ s),
    (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
by_cases h' : i ∈ s
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
simp [h, h']
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : DecidableEq α
j : α
inst_2 : (i : α) → Decidable (i ∈ insert j s)
i : α
h : ¬i = j
h' : ¬i ∈ s
⊢ (if i = j ∨ i ∈ s then f i else g i) = update (β := δ) (fun (i : α) ↦ if i ∈ s then f i else g i) j (f j) i

Tactic:
simp [h, h']
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
i : α
hi : i ∈ s
⊢ s.piecewise (β := δ) f g i = f i

Tactic:
if_pos hi

Premises used: if_pos, Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
i : α
hi : ¬i ∈ s
⊢ s.piecewise (β := δ) f g i = g i

Tactic:
if_neg hi

Premises used: Set.piecewise, if_neg
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
h : ∀ (y : α), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g = update (β := fun (a : α) ↦ β) g x (f x)

Tactic:
ext y
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
pos : ∀ (hy : y = x), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
neg : ∀ (hy : ¬y = x), piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y

Tactic:
by_cases hy : y = x
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
hy : y = x
pos : piecewise (β := fun (i : α) ↦ β) {x} f g x = update (β := fun (a : α) ↦ β) g x (f x) x
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y

Tactic:
subst y
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g x = update (β := fun (a : α) ↦ β) g x (f x) x

Tactic:
simp
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
x : α
inst : (y : α) → Decidable (Membership.mem (γ := Set α) {x} y)
inst_1 : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ piecewise (β := fun (i : α) ↦ β) {x} f g y = update (β := fun (a : α) ↦ β) g x (f x) y

Tactic:
simp [hy]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f g) f s

Tactic:
fun _ =>
  piecewise_eq_of_mem _ _ _

Premises used: Set.EqOn, Set.piecewise_eq_of_mem
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ EqOn (s.piecewise (β := fun (a : α) ↦ β) f g) g sᶜ

Tactic:
fun _ =>
  piecewise_eq_of_notMem _ _ _

Premises used: Set.piecewise_eq_of_notMem, Set.Mem, setOf, Set.EqOn, Not
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : i ∈ s
⊢ s.piecewise (β := δ) f₁ f₂ i ≤ g i

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g i
i : α
h : ¬i ∈ s
⊢ s.piecewise (β := δ) f₁ f₂ i ≤ g i

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → g i ≤ f₁ i
h₂ : ∀ (i : α), ¬i ∈ s → g i ≤ f₂ i
⊢ g ≤ s.piecewise (β := δ) f₁ f₂

Tactic:
@piecewise_le α (fun i => (δ i)ᵒᵈ) _ s _ _ _ _ h₁ h₂

Premises used: Set.piecewise_le, OrderDual
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
h₃ : ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise (β := δ) g₁ g₂ i
h₄ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ s.piecewise (β := δ) g₁ g₂ i
⊢ s.piecewise (β := δ) f₁ f₂ ≤ s.piecewise (β := δ) g₁ g₂

Tactic:
apply piecewise_le

Premises used: Set.piecewise_le
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i : α
h : i ∈ s
⊢ f₁ i ≤ s.piecewise (β := δ) g₁ g₂ i

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Type u_8
inst : (i : α) → Preorder (δ i)
s : Set α
inst_1 : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
i : α
h : ¬i ∈ s
⊢ f₂ i ≤ s.piecewise (β := δ) g₁ g₂ i

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst_1 : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise (β := δ) f g i = s.piecewise (β := δ) f g i

Tactic:
simp [piecewise, h]

Premises used: Set.piecewise
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ sᶜ.piecewise (β := δ) f g x = s.piecewise (β := δ) g f x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst : (j : α) → Decidable (j ∈ s)
inst_1 : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : ¬x ∈ s
⊢ sᶜ.piecewise (β := δ) f g x = s.piecewise (β := δ) g f x

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_8
f : ι → α
inst : (j : α) → Decidable (j ∈ range f)
g₁ g₂ : α → β
⊢ (range f).piecewise (β := fun (a : α) ↦ β) g₁ g₂ ∘ f = g₁ ∘ f

Tactic:
(piecewise_eqOn ..).comp_eq

Premises used: Set.piecewise_eqOn, Set.EqOn.comp_eq
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst : (j : α) → Decidable (j ∈ s)
f g : α → γ
h : β → α
⊢ s.piecewise (β := fun (a : α) ↦ γ) f g ∘ h = (h ⁻¹' s).piecewise (β := fun (a : β) ↦ γ) (f ∘ h) (g ∘ h)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.piecewise, rfl, ite
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ MapsTo (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
(h₁.congr ?_).union_union (h₂.congr ?_)

Premises used: Set.ite, Set.MapsTo.union_union, Set.MapsTo.congr
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
refine_1 : EqOn f₁ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₁ ∩ s)
refine_2 : EqOn f₂ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₂ ∩ sᶜ)
⊢ MapsTo (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s.ite s₁ s₂) (t.ite t₁ t₂)

Tactic:
refine (h₁.congr ?_).union_union (h₂.congr ?_)

Premises used: Set.MapsTo.union_union, Set.MapsTo.congr
-- Module: Mathlib.Data.Set.Piecewise
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
t t₁ t₂ : Set β
f₁ f₂ : α → β
inst : (i : α) → Decidable (i ∈ s)
h₁ : MapsTo f₁ (s₁ ∩ s) (t₁ ∩ t)
h₂ : MapsTo f₂ (s₂ ∩ sᶜ) (t₂ ∩ tᶜ)
⊢ EqOn f₁ (s.piecewise (β := fun (a : α) ↦ β) f₁ f₂) (s₁ ∩ s)

Tactic:
(piecewise_eqOn s f₁ f₂).symm.mono inter_subset_right

Premises used: Set.piecewise_eqOn, Set.EqOn.symm, Set.EqOn.mono, Set.inter_subset_right