awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r s : Setoid α
conv_rhs :
  LE.le (α := Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          r :
        Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          s :
        Partitions α) ↔
    mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯
⊢ LE.le (α := Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          r :
        Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          s :
        Partitions α) ↔
    r ≤ s

Tactic:
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]

Premises used: Setoid.mkClasses_classes
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
r s : Setoid α
⊢ LE.le (α := Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          r :
        Partitions α)
      (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes ⋯,
              invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯, left_inv := ⋯, right_inv := ⋯ } :
            (a : Setoid α) → Partitions α)
          s :
        Partitions α) ↔
    mkClasses r.classes ⋯ ≤ mkClasses s.classes ⋯

Tactic:
rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
α : Type u_1
f : Finpartition (α := Set α) Set.univ
⊢ Setoid.IsPartition (↑(f.parts (a := Set.univ)) : Set (Set α))

Tactic:
⟨f.bot_notMem,
    Setoid.eqv_classes_of_disjoint_union (f.parts.sup_id_set_eq_sUnion.symm.trans f.sup_parts)
      f.supIndep.pairwiseDisjoint⟩

Premises used: Finpartition.parts, Setoid.IsPartition, Setoid.eqv_classes_of_disjoint_union, And.intro, Finset.SupIndep.pairwiseDisjoint, Finpartition.supIndep, Finpartition.bot_notMem, Eq.symm, Finpartition.sup_parts, Finset.sup_id_set_eq_sUnion, Eq.trans
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ ∃ (i : ι), x ∈ s i

Tactic:
⟨hs.index x, hs.mem_index x⟩

Premises used: IndexedPartition.index, Exists.intro, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x ↔ Membership.mem (γ := Set α) univ x
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ

Tactic:
ext x
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x ↔ Membership.mem (γ := Set α) univ x

Tactic:
simp [hs.exists_mem x]

Premises used: IndexedPartition.exists_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ Pairwise (Disjoint on s)

Tactic:
fun {_i _j} h =>
  disjoint_left.mpr fun {_x} hxi hxj => h (hs.eq_of_mem hxi hxj)

Premises used: Iff.mpr, Set.disjoint_left, IndexedPartition.eq_of_mem, Pairwise
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
i : ι
⊢ x ∈ s i ↔ hs.index (s := s) x = i

Tactic:
⟨fun hxi => (hs.eq_of_mem hxi (hs.mem_index x)).symm, fun h => h ▸ hs.mem_index _⟩

Premises used: IndexedPartition.eq_of_mem, Eq.rec, Iff.intro, Eq.symm, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
i : ι
⊢ s i = {x : α | hs.index (s := s) x = i}

Tactic:
Set.ext fun _ => hs.mem_iff_index_eq

Premises used: Set.ext, IndexedPartition.mem_iff_index_eq
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
i : ι
⊢ hs.index (s := s) (hs.some (s := s) i) = i

Tactic:
(mem_iff_index_eq _).1 <| hs.some_mem i

Premises used: IndexedPartition.mem_iff_index_eq, IndexedPartition.some_mem, Iff.mp
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (hs.setoid : α → α → Prop) (hs.some (s := s) (hs.index (s := s) x)) x

Tactic:
hs.index_some (hs.index x)

Premises used: IndexedPartition.index_some, IndexedPartition.index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x y : α
⊢ hs.proj (s := s) x = hs.proj (s := s) y ↔ hs.index (s := s) x = hs.index (s := s) y

Tactic:
Quotient.eq''

Premises used: IndexedPartition.Quotient, Quotient.eq'', IndexedPartition.proj
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ hs.proj (s := s) (hs.some (s := s) (hs.index (s := s) x)) = hs.proj (s := s) x

Tactic:
Quotient.eq''.2 (hs.some_index x)

Premises used: Iff.mpr, IndexedPartition.Quotient, IndexedPartition.some_index, Quotient.eq'', IndexedPartition.proj
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (hs.equivQuotient (s := s) : (a : ι) → hs.Quotient) (hs.index (s := s) x) = hs.proj (s := s) x

Tactic:
hs.proj_eq_iff.mpr (some_index hs x)

Premises used: Iff.mpr, IndexedPartition.some_index, IndexedPartition.proj_eq_iff, IndexedPartition.proj
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (hs.proj (s := s) x) = hs.index (s := s) x

Tactic:
rfl

Premises used: Setoid.kerLift, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ (⇑(hs.equivQuotient (s := s)) : (a : ι) → hs.Quotient) ∘ hs.index (s := s) = hs.proj (s := s)

Tactic:
funext hs.equivQuotient_index_apply

Premises used: IndexedPartition.equivQuotient_index_apply, funext
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (hs.out (s := s) : (a : hs.Quotient) → α) (hs.proj (s := s) x) = hs.some (s := s) (hs.index (s := s) x)

Tactic:
rfl

Premises used: Setoid.kerLift, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : hs.Quotient (s := s)
⊢ hs.index (s := s) (Quotient.out x) = hs.index (s := s) ((hs.out (s := s) : (a : hs.Quotient) → α) x)

Tactic:
Quotient.inductionOn' x fun x => (Setoid.ker_apply_mk_out x).trans (hs.index_some _).symm

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : hs.Quotient (s := s)
⊢ hs.proj (s := s) ((hs.out (s := s) : (a : hs.Quotient) → α) x) = x

Tactic:
Quotient.inductionOn' x fun x => Quotient.sound' <| hs.some_index x

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ setOf ((hs.setoid : α → α → Prop) x) = s (hs.index (s := s) x)

Tactic:
Set.ext fun _y => eq_comm.trans hs.mem_iff_index_eq.symm

Premises used: Set.ext, IndexedPartition.mem_iff_index_eq, eq_comm, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x : α
h :
  ∀ (y : α),
    y ∈ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} ↔
      y ∈ s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))
⊢ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} =
    s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))

Tactic:
ext y
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x y : α
h :
  hs.proj (s := s) y = Quotient.mk'' x ↔
    hs.index (s := s) y = (hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x)
⊢ y ∈ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} ↔
    y ∈ s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]

Premises used: IndexedPartition.mem_iff_index_eq, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x y : α
⊢ hs.proj (s := s) y = Quotient.mk'' x ↔
    hs.index (s := s) y = (hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x)

Tactic:
Quotient.eq''

Premises used: IndexedPartition.Quotient, Quotient.eq'', Setoid.kerLift, IndexedPartition.proj
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x y : α
⊢ hs.proj (s := s) y = Quotient.mk'' x ↔
    hs.index (s := s) y = (hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x)

Tactic:
exact Quotient.eq''

Premises used: Quotient.eq''
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : α
⊢ hs.piecewise (s := s) f x = f (hs.index (s := s) x) x

Tactic:
rfl

Premises used: IndexedPartition.piecewise, rfl
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : hs.piecewise (s := s) f x = hs.piecewise (s := s) f y
this : hs.index (s := s) x = hs.index (s := s) y
apply : f (hs.index (s := s) x) x = f (hs.index (s := s) x) y
⊢ x = y

Tactic:
apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)

Premises used: IndexedPartition.index, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : hs.piecewise (s := s) f x = hs.piecewise (s := s) f y
this : hs.index (s := s) x = hs.index (s := s) y
⊢ f (hs.index (s := s) x) x = f (hs.index (s := s) x) y

Tactic:
simpa only [piecewise_apply, this] using h

Premises used: IndexedPartition.piecewise_apply
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : hs.piecewise (s := s) f x = hs.piecewise (s := s) f y
suffices : hs.index (s := s) x = hs.index (s := s) y
⊢ x = y

Tactic:
suffices hs.index x = hs.index y by
    apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)
    simpa only [piecewise_apply, this] using h
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : hs.piecewise (s := s) f x = hs.piecewise (s := s) f y
apply :
  ¬Disjoint (f (hs.index (s := s) x) '' s (hs.index (s := s) x)) (f (hs.index (s := s) y) '' s (hs.index (s := s) y))
⊢ hs.index (s := s) x = hs.index (s := s) y

Tactic:
apply h_disjoint.elim trivial trivial

Premises used: trivial, Set.PairwiseDisjoint.elim
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : hs.piecewise (s := s) f x = hs.piecewise (s := s) f y
contrapose! :
  ∀
    (h :
      Disjoint (f (hs.index (s := s) x) '' s (hs.index (s := s) x))
        (f (hs.index (s := s) y) '' s (hs.index (s := s) y))),
    hs.piecewise (s := s) f x ≠ hs.piecewise (s := s) f y
⊢ ¬Disjoint (f (hs.index (s := s) x) '' s (hs.index (s := s) x)) (f (hs.index (s := s) y) '' s (hs.index (s := s) y))

Tactic:
contrapose! h
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : Disjoint (f (hs.index (s := s) x) '' s (hs.index (s := s) x)) (f (hs.index (s := s) y) '' s (hs.index (s := s) y))
⊢ hs.piecewise (s := s) f x ≠ hs.piecewise (s := s) f y

Tactic:
h.ne_of_mem (mem_image_of_mem _ (hs.mem_index x)) (mem_image_of_mem _ (hs.mem_index y))

Premises used: IndexedPartition.piecewise, Set.mem_image_of_mem, Disjoint.ne_of_mem, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
x y : α
h : Disjoint (f (hs.index (s := s) x) '' s (hs.index (s := s) x)) (f (hs.index (s := s) y) '' s (hs.index (s := s) y))
⊢ hs.piecewise (s := s) f x ≠ hs.piecewise (s := s) f y

Tactic:
exact h.ne_of_mem (mem_image_of_mem _ (hs.mem_index x)) (mem_image_of_mem _ (hs.mem_index y))

Premises used: Set.mem_image_of_mem, Disjoint.ne_of_mem, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
set :
  let g := hs.piecewise (s := s) f;
  ∀ (hg : g = hs.piecewise (s := s) f), Bijective g
⊢ Bijective (hs.piecewise (s := s) f)

Tactic:
set g := piecewise hs f with hg

Premises used: IndexedPartition.piecewise
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
i : ι
⊢ BijOn g (s i) (t i)

Tactic:
(hf i).congr fun x hx => ?_

Premises used: Set.BijOn.congr
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
i : ι
refine : ∀ (x : α) (hx : x ∈ s i), f i x = g x
⊢ BijOn g (s i) (t i)

Tactic:
refine (hf i).congr fun x hx => ?_

Premises used: Set.BijOn.congr
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
i : ι
x : α
hx : x ∈ s i
rw : f i x = hs.piecewise (s := s) f x
rw₁ : f i x = f (hs.index (s := s) x) x
rw₂ rw₃ : f i x = f i x
⊢ f i x = g x

Tactic:
rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]

Premises used: IndexedPartition.mem_iff_index_eq, Iff.mp, IndexedPartition.piecewise_apply
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
⊢ ∀ (i : ι), BijOn g (s i) (t i)

Tactic:
have hg_bij (i) : BijOn g (s i) (t i) := by
    refine (hf i).congr fun x hx => ?_
    rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
⊢ InjOn g (⋃ (i : ι), s i)

Tactic:
injOn_of_injective (piecewise_inj hs (fun i ↦ BijOn.injOn (hf i)) ?_)

Premises used: IndexedPartition.piecewise_inj, Set.BijOn.injOn, Set.injOn_of_injective
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
refine : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
⊢ InjOn g (⋃ (i : ι), s i)

Tactic:
refine injOn_of_injective (piecewise_inj hs (fun i ↦ BijOn.injOn (hf i)) ?_)

Premises used: IndexedPartition.piecewise_inj, Set.BijOn.injOn, Set.injOn_of_injective
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
simp : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ t i
⊢ PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i

Tactic:
simp only [fun i ↦ BijOn.image_eq (hf i)]

Premises used: Set.BijOn.image_eq
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
i j : ι
hij : i ≠ j
⊢ onFun.{u_1 + 1, u_3 + 1, 1} (β := Set β) Disjoint (fun (i : ι) ↦ t i) i j

Tactic:
ht.disjoint hij

Premises used: IndexedPartition.disjoint
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
i j : ι
hij : i ≠ j
⊢ onFun.{u_1 + 1, u_3 + 1, 1} (β := Set β) Disjoint (fun (i : ι) ↦ t i) i j

Tactic:
exact ht.disjoint hij

Premises used: IndexedPartition.disjoint
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
⊢ InjOn g (⋃ (i : ι), s i)

Tactic:
have hg_inj : InjOn g (⋃ i, s i) := by
    refine injOn_of_injective (piecewise_inj hs (fun i ↦ BijOn.injOn (hf i)) ?_)
    simp only [fun i ↦ BijOn.image_eq (hf i)]
    rintro i - j - hij
    exact ht.disjoint hij
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ (i : ι), s i)
rw : BijOn g (⋃ (i : ι), s i) (⋃ (i : ι), t i)
⊢ Bijective g

Tactic:
rw [← bijOn_univ, ← hs.iUnion, ← ht.iUnion]

Premises used: IndexedPartition.iUnion, Set.bijOn_univ
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ (i : ι), s i)
⊢ BijOn g (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
bijOn_iUnion hg_bij hg_inj

Premises used: Set.bijOn_iUnion
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise (s := s) f
hg : g = hs.piecewise (s := s) f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ (i : ι), s i)
⊢ BijOn g (⋃ (i : ι), s i) (⋃ (i : ι), t i)

Tactic:
exact bijOn_iUnion hg_bij hg_inj

Premises used: Set.bijOn_iUnion
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
⊢ hs.piecewise (s := s) f ⁻¹' t = ⋃ (i : ι), s i ∩ f i ⁻¹' t

Tactic:
ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩

Premises used: Set.ext, IndexedPartition.piecewise, Membership.mem, _private.0.IndexedPartition.piecewise_preimage.match_1, Set.preimage, Iff.intro
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
refine_1 :
  ∀ (x : α) (hx : x ∈ hs.piecewise (s := s) f ⁻¹' t), Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x
refine_2 :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x →
      ∀ (a : Set α) (i : ι) (hi : (fun (i : ι) ↦ s i ∩ f i ⁻¹' t) i = a) (ha : x ∈ a), x ∈ hs.piecewise (s := s) f ⁻¹' t
⊢ hs.piecewise (s := s) f ⁻¹' t = ⋃ (i : ι), s i ∩ f i ⁻¹' t

Tactic:
refine ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ hs.piecewise (s := s) f ⁻¹' t
⊢ x ∈ f (hs.index (s := s) x) ⁻¹' t

Tactic:
rw [mem_preimage, piecewise_apply, ← mem_preimage] at hx

Premises used: IndexedPartition.piecewise_apply, Set.mem_preimage
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index (s := s) x) ⁻¹' t
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x

Tactic:
mem_iUnion_of_mem (hs.index x) (mem_inter (hs.mem_index x) hx)

Premises used: Set.mem_inter, IndexedPartition.index, Set.mem_iUnion_of_mem, IndexedPartition.mem_index
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index (s := s) x) ⁻¹' t
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x

Tactic:
exact mem_iUnion_of_mem (hs.index x) (mem_inter (hs.mem_index x) hx)

Premises used: IndexedPartition.index, Set.mem_iUnion_of_mem
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
h : Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x
a : Set α
i : ι
hi : (fun (i : ι) ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ a
⊢ Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i ∩ f i ⁻¹' t) (hs.index (s := s) x)) x

Tactic:
rw [← hi, ← (mem_iff_index_eq hs).mp ha.1] at ha
-- Module: Mathlib.Data.Setoid.Partition
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
h : Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x
a : Set α
i : ι
hi : (fun (i : ι) ↦ s i ∩ f i ⁻¹' t) i = a
ha : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i ∩ f i ⁻¹' t) (hs.index (s := s) x)) x
⊢ x ∈ hs.piecewise (s := s) f ⁻¹' t

Tactic:
simp_all [piecewise_apply]

Premises used: IndexedPartition.piecewise_apply