Theorem: exercise4_2 (LeanCourse/Assignments/Assignment4.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Tactic:
have h := wf.wf.has_min
State after:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
h : ∀ (s : Set ι), Set.Nonempty s → ∃ a ∈ s, ∀ x ∈ s, ¬x < a
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i

State before:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrder ι
wf : WellFoundedLT ι
A C : ι → Set α
hC : ∀ (i : ι), C i = A i \ ⋃ j, ⋃ (_ : j < i), A j
h : ∀ (s : Set ι), Set.Nonempty s → ∃ a ∈ s, ∀ x ∈ s, ¬x < a
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Tactic:
sorry
State after:
no goals