Theorem: HTPI.Theorem_4_5_6 (HTPILib/Chap4.lean)

State before:
A : Type
F : Set (Set A)
h : partition F
⊢ ∃ R, equiv_rel R ∧ mod A R = F
Tactic:
set R : BinRel A := EqRelFromPart F
State after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ ∃ R, equiv_rel R ∧ mod A R = F

State before:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ ∃ R, equiv_rel R ∧ mod A R = F
Tactic:
apply Exists.intro R
State after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ equiv_rel R ∧ mod A R = F

State before:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ equiv_rel R ∧ mod A R = F
Tactic:
apply And.intro (Lemma_4_5_7 F h)
State after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ mod A R = F

State before:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ mod A R = F
Tactic:
apply Set.ext
State after:
case h
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ ∀ (x : Set A), x ∈ mod A R ↔ x ∈ F

State before:
case h
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ ∀ (x : Set A), x ∈ mod A R ↔ x ∈ F
Tactic:
fix X : Set A
State after:
case h
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ mod A R ↔ X ∈ F

State before:
case h
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ mod A R ↔ X ∈ F
Tactic:
apply Iff.intro
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ mod A R → X ∈ F

case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ F → X ∈ mod A R

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ mod A R → X ∈ F
Tactic:
assume h2 : X ∈ mod A R
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ mod A R
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ mod A R
⊢ X ∈ F
Tactic:
define at h2
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ X ∈ F
Tactic:
obtain (x : A) (h3 : equivClass R x = X) from h2
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ X ∈ F
Tactic:
have h4 : x ∈ ⋃₀ F := h.left x
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : x ∈ ⋃₀ F
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : x ∈ ⋃₀ F
⊢ X ∈ F
Tactic:
define at h4
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
⊢ X ∈ F
Tactic:
obtain (Y : Set A) (h5 : Y ∈ F ∧ x ∈ Y) from h4
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
⊢ X ∈ F
Tactic:
have h6 : equivClass R x = Y :=
  Lemma_4_5_8 F h Y h5.left x h5.right
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
h6 : equivClass R x = Y
⊢ X ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
h6 : equivClass R x = Y
⊢ X ∈ F
Tactic:
rewrite [←h3, h6]
State after:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
h6 : equivClass R x = Y
⊢ Y ∈ F

State before:
case h.mp
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
h4 : ∃ t ∈ F, x ∈ t
Y : Set A
h5 : Y ∈ F ∧ x ∈ Y
h6 : equivClass R x = Y
⊢ Y ∈ F
Tactic:
show Y ∈ F from h5.left
State after:
no goals

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
⊢ X ∈ F → X ∈ mod A R
Tactic:
assume h2 : X ∈ F
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
⊢ X ∈ mod A R

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
⊢ X ∈ mod A R
Tactic:
have h3 : ¬empty X := h.right.right X h2
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ¬empty X
⊢ X ∈ mod A R

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ¬empty X
⊢ X ∈ mod A R
Tactic:
define at h3
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ¬¬∃ x, x ∈ X
⊢ X ∈ mod A R

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ¬¬∃ x, x ∈ X
⊢ X ∈ mod A R
Tactic:
double_neg at h3
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
⊢ X ∈ mod A R

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
⊢ X ∈ mod A R
Tactic:
obtain (x : A) (h4 : x ∈ X) from h3
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
x : A
h4 : x ∈ X
⊢ X ∈ mod A R

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
x : A
h4 : x ∈ X
⊢ X ∈ mod A R
Tactic:
define
State after:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
x : A
h4 : x ∈ X
⊢ ∃ x, equivClass R x = X

State before:
case h.mpr
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
X : Set A
h2 : X ∈ F
h3 : ∃ x, x ∈ X
x : A
h4 : x ∈ X
⊢ ∃ x, equivClass R x = X
Tactic:
show ∃ (x : A), equivClass R x = X from
  Exists.intro x (Lemma_4_5_8 F h X h2 x h4)
State after:
no goals