awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := ⋯
rw : x.toSet = y.toSet
⊢ x = y
have rw₁ : (mkClasses x.toSet sorry).classes = y.toSet
Tactic: rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := ⋯
rw : x.toSet = y.toSet
rw₁ : (mkClasses x.toSet ⋯).classes = y.toSet
⊢ x = y
have rw₂ : (mkClasses x.toSet sorry).classes = (mkClasses y.toSet sorry).classes
Tactic: rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := ⋯
rw : x.toSet = y.toSet
rw₁ : (mkClasses x.toSet ⋯).classes = y.toSet
rw₂ : (mkClasses x.toSet ⋯).classes = (mkClasses y.toSet ⋯).classes
⊢ x = y
have rw₃ : (mkClasses y.toSet sorry).classes = (mkClasses y.toSet sorry).classes
Tactic: rw [Partitions.ext_iff, ← classes_mkClasses x.toSet x.isPartition,
      ← classes_mkClasses y.toSet y.isPartition, h]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
C : Partitions α
⊢ (fun (r : Setoid α) ↦ (Subtype.mk (p := IsPartition) r.classes ⋯ : Subtype (α := Set (Set α)) IsPartition))
      ((fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) ⋯) C) =
    C
have rw : Partitions.toSet
    ((fun (r : Setoid α) ↦ (Subtype.mk (p := IsPartition) r.classes sorry : Subtype (α := Set (Set α)) IsPartition))
      ((fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) sorry) C)) =
  (mkClasses C.toSet sorry).classes
Tactic: rw [Partitions.ext_iff, ← classes_mkClasses C.toSet C.isPartition]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
α : Type u_1
r s : Setoid α
| r ≤ s
have rw : mkClasses r.classes sorry ≤ mkClasses s.classes sorry
Tactic: rw [← mkClasses_classes r, ← mkClasses_classes s]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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 α) ↔
    r ≤ s
have conv_rhs : LE.le (α := Partitions α)
    (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes sorry,
            invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) sorry, left_inv := sorry, right_inv := sorry } :
          (a : Setoid α) → Partitions α)
        r :
      Partitions α)
    (({ toFun := fun (r : Setoid α) ↦ Subtype.mk (p := IsPartition) r.classes sorry,
            invFun := fun (C : Partitions α) ↦ mkClasses (↑C : Set (Set α)) sorry, left_inv := sorry, right_inv := sorry } :
          (a : Setoid α) → Partitions α)
        s :
      Partitions α) ↔
  mkClasses r.classes sorry ≤ mkClasses s.classes sorry
Tactic: conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ Eq.{u_2 + 1} (α := Set α) (⋃ (i : ι), s i) univ
have h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x ↔ Membership.mem (γ := Set α) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x : α
⊢ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} =
    s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))
have h : ∀ (y : α),
  y ∈ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} ↔
    y ∈ s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x_1 : hs.Quotient (s := s)
x y : α
⊢ y ∈ hs.proj (s := s) ⁻¹' {Quotient.mk'' x} ↔
    y ∈ s ((hs.equivQuotient (s := s).symm : (a : hs.Quotient) → ι) (Quotient.mk'' x))
have 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)
Tactic: simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ x = y
have apply : f (hs.index (s := s) x) x = f (hs.index (s := s) x) y
Tactic: apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ x = y
have suffices : hs.index (s := s) x = hs.index (s := s) 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
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ hs.index (s := s) x = hs.index (s := s) y
have 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))
Tactic: apply h_disjoint.elim trivial trivial
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ ¬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))
have 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
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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)
⊢ Bijective (hs.piecewise (s := s) f)
have set : let g := hs.piecewise (s := s) f;
∀ (hg : g = hs.piecewise (s := s) f), Bijective g
Tactic: set g := piecewise hs f with hg
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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)
have refine : ∀ (x : α) (hx : x ∈ s i), f i x = g x
Tactic: refine (hf i).congr fun x hx => ?_
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ f i x = g x
have rw₁ : f i x = f (hs.index (s := s) x) x
Tactic: rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ f i x = g x
have rw₂ : f i x = f i x
Tactic: rw [hg, piecewise_apply, hs.mem_iff_index_eq.mp hx]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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
⊢ Bijective g
have hg_bij : ∀ (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]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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)
have refine : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
Tactic: refine injOn_of_injective (piecewise_inj hs (fun i ↦ BijOn.injOn (hf i)) ?_)
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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)
⊢ PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ f i '' s i
have simp : PairwiseDisjoint.{u_3, u_1} (α := Set β) univ fun (i : ι) ↦ t i
Tactic: simp only [fun i ↦ BijOn.image_eq (hf i)]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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)
⊢ Bijective g
have hg_inj : 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
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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)
⊢ Bijective g
have rw : BijOn g (⋃ (i : ι), s i) (⋃ (i : ι), t i)
Tactic: rw [← bijOn_univ, ← hs.iUnion, ← ht.iUnion]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
have refine_1 : ∀ (x : α) (hx : x ∈ hs.piecewise (s := s) f ⁻¹' t), Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x
Tactic: refine ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
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
⊢ hs.piecewise (s := s) f ⁻¹' t = ⋃ (i : ι), s i ∩ f i ⁻¹' t
have 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
Tactic: refine ext fun x => ⟨fun hx => ?_, fun ⟨a, ⟨i, hi⟩, ha⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i ∩ f i ⁻¹' t) x
have hx₁ : x ∈ f (hs.index (s := s) x) ⁻¹' t
Tactic: rw [mem_preimage, piecewise_apply, ← mem_preimage] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
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
⊢ x ∈ hs.piecewise (s := s) f ⁻¹' t
have ha₁ : 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
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
⊢ range (hs.piecewise (s := s) f) = ⋃ (i : ι), f i '' s i
have refine_1 : ∀ x ∈ range (hs.piecewise (s := s) f), Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
Tactic: refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
refine_1 : ∀ x ∈ range (hs.piecewise (s := s) f), Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
⊢ range (hs.piecewise (s := s) f) = ⋃ (i : ι), f i '' s i
have refine_2 : ∀ (x : β),
  Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x →
    ∀ (t : Set β) (i : ι) (hi : (fun (i : ι) ↦ f i '' s i) i = t) (ht : x ∈ t), x ∈ range (hs.piecewise (s := s) f)
Tactic: refine ext fun x => ⟨?_, fun ⟨t, ⟨i, hi⟩, ht⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
ht : x ∈ t
⊢ x ∈ range (hs.piecewise (s := s) f)
have ht₁ : ∃ x_1 ∈ s i, f i x_1 = x
Tactic: simp only [← hi, mem_image] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
ht : ∃ x_1 ∈ s i, f i x_1 = x
⊢ x ∈ range (hs.piecewise (s := s) f)
have refine_2 : ∀ (a : α) (ha1 : a ∈ s i) (ha2 : f i a = x), x ∈ range (hs.piecewise (s := s) f)
Tactic: obtain ⟨a, ha1, ha2⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha1 : a ∈ s i
ha2 : f i a = x
⊢ x ∈ range (hs.piecewise (s := s) f)
have refine_2 : hs.piecewise (s := s) f a = x
Tactic: refine ⟨a, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
x : β
h : Membership.mem (γ := Set β) (⋃ (i : ι), f i '' s i) x
t : Set β
i : ι
hi : (fun (i : ι) ↦ f i '' s i) i = t
a : α
ha1 : a ∈ s i
ha2 : f i a = x
⊢ hs.piecewise (s := s) f a = x
have ha1₁ : hs.index (s := s) a = i
Tactic: simp only [hs.mem_iff_index_eq] at ha1
Cleared hypotheses: ha1
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxi : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_i}, s i) x
hxj : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_j}, s i) x
⊢ _i = _j
have obtain : ∀ (a : Set α) (ha : x ∈ a) (c : ι) (hc : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_i}), s i : Set α)) c = a), _i = _j
Tactic: obtain ⟨a, ⟨c, hc⟩, ha⟩ := hxi
Cleared hypotheses: hxi
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
x : α
_i _j : κ
hxj : Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {_j}, s i) x
a : Set α
ha : x ∈ a
c : ι
hc : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_i}), s i : Set α)) c = a
⊢ _i = _j
have obtain : ∀ (b : Set α) (hb : x ∈ b) (d : ι) (hd : (fun (i : ι) ↦ (⋃ (_ : i ∈ g ⁻¹' {_j}), s i : Set α)) d = b), _i = _j
Tactic: obtain ⟨b, ⟨d, hd⟩, hb⟩ := hxj
Cleared hypotheses: hxj
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ Membership.mem (γ := Set α) (⋃ i ∈ g ⁻¹' {k}, s i) (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))
have refine : Membership.mem (γ := Set α) (⋃ (_ : sorry.some (s := g ⁻¹' {k}) ∈ g ⁻¹' {k}), s (sorry.some (s := g ⁻¹' {k})))
  (hs.some (s := s) (sorry.some (s := g ⁻¹' {k})))
Tactic: refine mem_iUnion_of_mem ((singleton_nonempty k).preimage hg).some ?_
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ Membership.mem (γ := Set α) (⋃ (_ : ⋯.some (s := g ⁻¹' {k}) ∈ g ⁻¹' {k}), s (⋯.some (s := g ⁻¹' {k})))
    (hs.some (s := s) (⋯.some (s := g ⁻¹' {k})))
have simp : g (sorry.some (s := g ⁻¹' {k})) = k ∧ hs.some (s := s) (sorry.some (s := g ⁻¹' {k})) ∈ s (sorry.some (s := g ⁻¹' {k}))
Tactic: simp only [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g (⋯.some (s := g ⁻¹' {k})) = k ∧ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))
have left : g (sorry.some (s := g ⁻¹' {k})) = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Setoid.Partition (goal)
Goal:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs_1 : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
left : g (⋯.some (s := g ⁻¹' {k})) = k
⊢ g (⋯.some (s := g ⁻¹' {k})) = k ∧ hs.some (s := s) (⋯.some (s := g ⁻¹' {k})) ∈ s (⋯.some (s := g ⁻¹' {k}))
have right : hs.some (s := s) (sorry.some (s := g ⁻¹' {k})) ∈ s (sorry.some (s := g ⁻¹' {k}))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk (β := β) a ∘ f = mk (β := β) b ∘ g
⊢ a = b ∧ f ≍ g
have rcases : ∀ (i : γ), a = b ∧ f ≍ g
Tactic: rcases ‹Nonempty γ› with ⟨i⟩
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : Type u_7
inst : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk (β := β) a ∘ f = mk (β := β) b ∘ g
i : γ
⊢ a = b ∧ f ≍ g
have obtain : ∀ {g : γ → β a} (h : mk (β := β) a ∘ f = mk (β := β) a ∘ g), a = a ∧ f ≍ g
Tactic: obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)
Cleared hypotheses: b, g, h
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) j y)
⊢ Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) j y
have obtain : ∀ (y : β₁ i)
  (h :
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
      Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i y)),
  Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i y
Tactic: obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
Cleared hypotheses: j, y, h
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h :
  Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i y)
⊢ Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i y
have obtain : ∀
  (h :
    Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x) =
      Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ (Sigma.mk (β := β₁) i x)),
  Sigma.mk (β := β₁) i x = Sigma.mk (β := β₁) i x
Tactic: obtain rfl : x = y := h₂ i (sigma_mk_injective h)
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α₁ : Type u_2
α₂ : Type u_3
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂)
have simp : ∀ (x : α₁) (b : β₂ (f₁ x)),
  ∃ (a : Sigma β₁), Sigma.map (β₁ := β₁) (β₂ := β₂) f₁ f₂ a = Sigma.mk (β := fun (a : α₂) ↦ β₂ a) (f₁ x) b
Tactic: simp only [Surjective, Sigma.forall, h₁.forall]
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
i : (a : α) × β a
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
x : γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f i
        x) =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      (i.fst (β := fun (a : α) ↦ β a))
      (update (β := γ (i.fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f (i.fst (β := fun (a : α) ↦ β a))) (i.snd (β := fun (a : α) ↦ β a)) x)
have obtain : ∀ (ia : α) (ib : β ia)
  (x :
    γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))),
  curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x) =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
Tactic: obtain ⟨ia, ib⟩ := i
Cleared hypotheses: i, x