Theorem: Setoid.isPartition_on (Jordan/Mathlib/Partitions.lean)

State before:
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ IsPartition {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
Tactic:
constructor
State after:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∅ ∉ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}

case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∀ (a : ↑s), ∃! b x, a ∈ b

State before:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∅ ∉ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
Tactic:
intro h
State after:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
⊢ False

State before:
case left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
⊢ False
Tactic:
obtain ⟨t, _, ht, hts⟩ := Set.mem_setOf_eq.mp h
State after:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ False

State before:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ False
Tactic:
apply hts
State after:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ t ∩ s = ∅

State before:
case left.intro.intro.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
h : ∅ ∈ {u | ∃ t ∈ P, Subtype.val ⁻¹' t = u ∧ t ∩ s ≠ ∅}
t : Set α
left✝ : t ∈ P
ht : Subtype.val ⁻¹' t = ∅
hts : t ∩ s ≠ ∅
⊢ t ∩ s = ∅
Tactic:
rw [Set.inter_comm, ← Subtype.image_preimage_coe, ht, Set.image_empty]
State after:
no goals

State before:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
⊢ ∀ (a : ↑s), ∃! b x, a ∈ b
Tactic:
intro a
State after:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
⊢ ∃! b x, a ∈ b

State before:
case right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
⊢ ∃! b x, a ∈ b
Tactic:
obtain ⟨t, ht⟩ := hP.right ↑a
State after:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (fun b => ∃! x, ↑a ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x, ↑a ∈ b) y → y = t
⊢ ∃! b x, a ∈ b

State before:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (fun b => ∃! x, ↑a ∈ b) t ∧ ∀ (y : Set α), (fun b => ∃! x, ↑a ∈ b) y → y = t
⊢ ∃! b x, a ∈ b
Tactic:
simp only [exists_unique_iff_exists, exists_prop, and_imp] at ht
State after:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∃! b x, a ∈ b

State before:
case right.intro
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∃! b x, a ∈ b
Tactic:
use Subtype.val ⁻¹' t
State after:
case h
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t) ∧ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t

State before:
case h
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t) ∧ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Tactic:
constructor
State after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t)

case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t

State before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (fun b => ∃! x, a ∈ b) (Subtype.val ⁻¹' t)
Tactic:
simp only [Ne.def, Set.mem_setOf_eq, Set.mem_preimage, exists_unique_iff_exists, exists_prop]
State after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (∃ t_1 ∈ P, Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' t ∧ ¬t_1 ∩ s = ∅) ∧ ↑a ∈ t

State before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ (∃ t_1 ∈ P, Subtype.val ⁻¹' t_1 = Subtype.val ⁻¹' t ∧ ¬t_1 ∩ s = ∅) ∧ ↑a ∈ t
Tactic:
refine ⟨⟨t, ht.1.1, rfl, ?_⟩, ht.1.2⟩
State after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ¬t ∩ s = ∅

State before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ¬t ∩ s = ∅
Tactic:
intro h
State after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ False

State before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ False
Tactic:
rw [← Set.mem_empty_iff_false (a : α), ← h]
State after:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ ↑a ∈ t ∩ s

State before:
case h.left
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
h : t ∩ s = ∅
⊢ ↑a ∈ t ∩ s
Tactic:
exact Set.mem_inter ht.left.right (Subtype.mem a)
State after:
no goals

State before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), (fun b => ∃! x, a ∈ b) y → y = Subtype.val ⁻¹' t
Tactic:
simp only [Ne.def, Set.mem_setOf_eq, exists_unique_iff_exists,
  exists_prop, and_imp, forall_exists_index]
State after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), ∀ x ∈ P, Subtype.val ⁻¹' x = y → ¬x ∩ s = ∅ → a ∈ y → y = Subtype.val ⁻¹' t

State before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
⊢ ∀ (y : Set ↑s), ∀ x ∈ P, Subtype.val ⁻¹' x = y → ¬x ∩ s = ∅ → a ∈ y → y = Subtype.val ⁻¹' t
Tactic:
intro y x hxP hxy _ hay
State after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ y = Subtype.val ⁻¹' t

State before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ y = Subtype.val ⁻¹' t
Tactic:
rw [← hxy, Subtype.preimage_coe_eq_preimage_coe_iff]
State after:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ s ∩ x = s ∩ t

State before:
case h.right
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ s ∩ x = s ∩ t
Tactic:
congr
State after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ x = t

State before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ x = t
Tactic:
apply ht.right x hxP
State after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ ↑a ∈ x

State before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ ↑a ∈ x
Tactic:
rw [← Set.mem_preimage, hxy]
State after:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ a ∈ y

State before:
case h.right.e_a
α✝ : Type ?u.49
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
a : ↑s
t : Set α
ht : (t ∈ P ∧ ↑a ∈ t) ∧ ∀ y ∈ P, ↑a ∈ y → y = t
y : Set ↑s
x : Set α
hxP : x ∈ P
hxy : Subtype.val ⁻¹' x = y
a✝ : ¬x ∩ s = ∅
hay : a ∈ y
⊢ a ∈ y
Tactic:
exact hay
State after:
no goals