Theorem: exercise4_2 (LeanCourse/Assignments/Solutions/Solutions4.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:
have lem1 : ∀ i j, i < j → Disjoint (C i) (C j)
State after:
case lem1
ι : 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
⊢ ∀ (i j : ι), i < j → Disjoint (C i) (C j)

ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ Pairwise (Disjoint on C) ∧ ⋃ i, C i = ⋃ i, A i
Tactic:
constructor
State after:
case left
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ Pairwise (Disjoint on C)

case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, C i = ⋃ i, A i

State before:
case lem1
ι : 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
⊢ ∀ (i j : ι), i < j → Disjoint (C i) (C j)
Tactic:
intro i j hij
State after:
case lem1
ι : 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
i j : ι
hij : i < j
⊢ Disjoint (C i) (C j)

State before:
case lem1
ι : 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
i j : ι
hij : i < j
⊢ Disjoint (C i) (C j)
Tactic:
simp [disjoint_left, hC]
State after:
case lem1
ι : 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
i j : ι
hij : i < j
⊢ ∀ ⦃a : α⦄, a ∈ A i → (∀ x < i, a ∉ A x) → a ∈ A j → ∃ i < j, a ∈ A i

State before:
case lem1
ι : 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
i j : ι
hij : i < j
⊢ ∀ ⦃a : α⦄, a ∈ A i → (∀ x < i, a ∉ A x) → a ∈ A j → ∃ i < j, a ∈ A i
Tactic:
tauto
State after:
no goals

State before:
case left
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ Pairwise (Disjoint on C)
Tactic:
intro i j hij
State after:
case left
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on C) i j

State before:
case left
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
⊢ (Disjoint on C) i j
Tactic:
obtain h|h := hij.lt_or_lt
State after:
case left.inl
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
h : i < j
⊢ (Disjoint on C) i j

case left.inr
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
h : j < i
⊢ (Disjoint on C) i j

State before:
case left.inl
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
h : i < j
⊢ (Disjoint on C) i j
Tactic:
exact lem1 i j h
State after:
no goals

State before:
case left.inr
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i j : ι
hij : i ≠ j
h : j < i
⊢ (Disjoint on C) i j
Tactic:
exact (lem1 j i h).symm
State after:
no goals

State before:
case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, C i = ⋃ i, A i
Tactic:
apply subset_antisymm
State after:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, C i ⊆ ⋃ i, A i

case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, A i ⊆ ⋃ i, C i

State before:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, C i ⊆ ⋃ i, A i
Tactic:
gcongr with i
State after:
case right.a.h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i : ι
⊢ C i ⊆ A i

State before:
case right.a.h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i : ι
⊢ C i ⊆ A i
Tactic:
rw [hC]
State after:
case right.a.h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i : ι
⊢ A i \ ⋃ j, ⋃ (_ : j < i), A j ⊆ A i

State before:
case right.a.h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
i : ι
⊢ A i \ ⋃ j, ⋃ (_ : j < i), A j ⊆ A i
Tactic:
exact?
State after:
no goals

State before:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ⋃ i, A i ⊆ ⋃ i, C i
Tactic:
simp [subset_def]
State after:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ∀ (x : α) (x_1 : ι), x ∈ A x_1 → ∃ i, x ∈ C i

State before:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
⊢ ∀ (x : α) (x_1 : ι), x ∈ A x_1 → ∃ i, x ∈ C i
Tactic:
intros x i hx
State after:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
⊢ ∃ i, x ∈ C i

State before:
case right.a
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
⊢ ∃ i, x ∈ C i
Tactic:
obtain ⟨i₀, h1i₀, h2i₀⟩ := h { i : ι | x ∈ A i } ⟨i, hx⟩
State after:
case right.a.intro.intro
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ ∃ i, x ∈ C i

State before:
case right.a.intro.intro
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ ∃ i, x ∈ C i
Tactic:
use i₀
State after:
case h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ x ∈ C i₀

State before:
case h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ x ∈ C i₀
Tactic:
simp [hC]
State after:
case h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ x ∈ A i₀ ∧ ∀ x_1 < i₀, x ∉ A x_1

State before:
case h
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ x ∈ A i₀ ∧ ∀ x_1 < i₀, x ∉ A x_1
Tactic:
use h1i₀
State after:
case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ ∀ x_1 < i₀, x ∉ A x_1

State before:
case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
⊢ ∀ x_1 < i₀, x ∉ A x_1
Tactic:
intro j hj h2j
State after:
case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
j : ι
hj : j < i₀
h2j : x ∈ A j
⊢ False

State before:
case right
ι : 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
lem1 : ∀ (i j : ι), i < j → Disjoint (C i) (C j)
x : α
i : ι
hx : x ∈ A i
i₀ : ι
h1i₀ : i₀ ∈ {i | x ∈ A i}
h2i₀ : ∀ x_1 ∈ {i | x ∈ A i}, ¬x_1 < i₀
j : ι
hj : j < i₀
h2j : x ∈ A j
⊢ False
Tactic:
exact h2i₀ j h2j hj
State after:
no goals