[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ classes (ker f) ⊆ Set.range fun y => {x | f x = y}
[PROOFSTEP]
rintro s ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ {x_1 | Rel (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}
[PROOFSTEP]
rw [Set.mem_range]
[GOAL]
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | Rel (ker f) x_1 x}
[PROOFSTEP]
exact ⟨f x, rfl⟩
[GOAL]
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
[PROOFSTEP]
classical exact le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)
[GOAL]
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Fintype β
f : α → β
inst✝ : Fintype ↑(classes (ker f))
⊢ Fintype.card ↑(classes (ker f)) ≤ Fintype.card β
[PROOFSTEP]
exact le_trans (Set.card_le_of_subset (classes_ker_subset_fiber_set f)) (Fintype.card_range_le _)
[GOAL]
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
c : Set α
z : α
hz : c = {x | Rel r x z}
hx : x ∈ c
hy : y ∈ c
⊢ Rel r x y
[PROOFSTEP]
subst c
[GOAL]
α : Type u_1
r : Setoid α
x y : α
x✝ : ∃ c, c ∈ classes r ∧ x ∈ c ∧ y ∈ c
z : α
hx : x ∈ {x | Rel r x z}
hy : y ∈ {x | Rel r x z}
⊢ Rel r x y
[PROOFSTEP]
exact r.trans' hx (r.symm' hy)
[GOAL]
α : Type u_1
r₁ r₂ : Setoid α
h : classes r₁ = classes r₂
a b : α
⊢ Rel r₁ a b ↔ Rel r₂ a b
[PROOFSTEP]
simp only [rel_iff_exists_classes, exists_prop, h]
[GOAL]
α : Type u_1
r : Setoid α
a : α
⊢ ∀ (y : Set α), y ∈ classes r → a ∈ y → y = {x | Rel r x a}
[PROOFSTEP]
rintro _ ⟨y, rfl⟩ ha
[GOAL]
case intro
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
⊢ {x | Rel r x y} = {x | Rel r x a}
[PROOFSTEP]
ext x
[GOAL]
case intro.h
α : Type u_1
r : Setoid α
a y : α
ha : a ∈ {x | Rel r x y}
x : α
⊢ x ∈ {x | Rel r x y} ↔ x ∈ {x | Rel r x a}
[PROOFSTEP]
exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩
[GOAL]
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b x, a ∈ b
x : α
⊢ {y | Rel (mkClasses c H) x y} ∈ c
[PROOFSTEP]
convert @Setoid.eqv_class_mem _ _ H x using 3
[GOAL]
case h.e'_4.h.e'_2.h.a
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b x, a ∈ b
x x✝ : α
⊢ Rel (mkClasses c H) x x✝ ↔ Rel (mkClasses c H) x✝ x
[PROOFSTEP]
rw [Setoid.comm']
[GOAL]
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : Set.PairwiseDisjoint c id
a : α
⊢ a ∈ ⋃₀ c
[PROOFSTEP]
rw [hu]
[GOAL]
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : Set.PairwiseDisjoint c id
a : α
⊢ a ∈ Set.univ
[PROOFSTEP]
exact Set.mem_univ a
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (fun b => ∃! x_1, x ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x_1, x ∈ b) y → y = t
⊢ t ∈ c ∧ x ∈ t
[PROOFSTEP]
simp only [exists_unique_iff_exists] at ht 
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
x : α
t : Set α
ht : (∃ x_1, x ∈ t) ∧ ∀ (y : Set α), (∃ x_1, x ∈ y) → y = t
⊢ t ∈ c ∧ x ∈ t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
x✝ : s ∈ classes (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b))
y : α
hs : s = {x | Rel (mkClasses c (_ : ∀ (a : α), ∃! b x, a ∈ b)) x y}
b : Set α
hm : b ∈ c
hb : y ∈ b
_hy : ∀ (y_1 : Set α), y_1 ∈ c → y ∈ y_1 → y_1 = b
⊢ s ∈ c
[PROOFSTEP]
rwa [show s = b from
    hs.symm ▸
      Set.ext fun x =>
        ⟨fun hx => symm' (mkClasses c hc.2) hx b hm hb, fun hx b' hc' hx' =>
          eq_of_mem_eqv_class hc.2 hm hx hc' hx' ▸ hb⟩]
[GOAL]
α : Type u_1
x y : Subtype IsPartition
hx : x ≤ y
hy : y ≤ x
⊢ x = y
[PROOFSTEP]
let h := @le_antisymm (Setoid α) _ _ _ hx hy
[GOAL]
α : Type u_1
x y : Subtype IsPartition
hx : x ≤ y
hy : y ≤ x
h : mkClasses ↑x (_ : ∀ (a : α), ∃! b x, a ∈ b) = mkClasses ↑y (_ : ∀ (a : α), ∃! b x, a ∈ b) := le_antisymm hx hy
⊢ x = y
[PROOFSTEP]
rw [Subtype.ext_iff_val, ← classes_mkClasses x.1 x.2, ← classes_mkClasses y.1 y.2, h]
[GOAL]
α : Type u_1
C : { C // IsPartition C }
⊢ (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
    C
[PROOFSTEP]
rw [Subtype.ext_iff_val, ← classes_mkClasses C.1 C.2]
[GOAL]
α : Type u_1
r s : Setoid α
⊢ ↑{ toFun := fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) },
            invFun := fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b),
            left_inv := (_ : ∀ (r : Setoid α), mkClasses (classes r) (_ : ∀ (a : α), ∃! b x, a ∈ b) = r),
            right_inv :=
              (_ :
                ∀ (C : { C // IsPartition C }),
                  (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
                      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
                    C) }
        r ≤
      ↑{ toFun := fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) },
            invFun := fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b),
            left_inv := (_ : ∀ (r : Setoid α), mkClasses (classes r) (_ : ∀ (a : α), ∃! b x, a ∈ b) = r),
            right_inv :=
              (_ :
                ∀ (C : { C // IsPartition C }),
                  (fun r => { val := classes r, property := (_ : ¬∅ ∈ classes r ∧ ∀ (a : α), ∃! b x, a ∈ b) })
                      ((fun C => mkClasses ↑C (_ : ∀ (a : α), ∃! b x, a ∈ b)) C) =
                    C) }
        s ↔
    r ≤ s
[PROOFSTEP]
conv_rhs => rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
α : Type u_1
r s : Setoid α
| r ≤ s
[PROOFSTEP]
rw [← mkClasses_classes r, ← mkClasses_classes s]
[GOAL]
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
⊢ ⋃ (i : ι), s i = univ
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ x ∈ ⋃ (i : ι), s i ↔ x ∈ univ
[PROOFSTEP]
simp [hs.exists_mem x]
[GOAL]
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x : α
⊢ proj hs ⁻¹' {Quotient.mk'' x} = s (↑(equivQuotient hs).symm (Quotient.mk'' x))
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ y ∈ proj hs ⁻¹' {Quotient.mk'' x} ↔ y ∈ s (↑(equivQuotient hs).symm (Quotient.mk'' x))
[PROOFSTEP]
simp only [Set.mem_preimage, Set.mem_singleton_iff, hs.mem_iff_index_eq]
[GOAL]
case h
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : IndexedPartition.Quotient hs
x y : α
⊢ proj hs y = Quotient.mk'' x ↔ index hs y = ↑(equivQuotient hs).symm (Quotient.mk'' x)
[PROOFSTEP]
exact Quotient.eq''
