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

State before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ pairwise_disjoint (mod A R)
Tactic:
define
State after:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ X ∈ mod A R, ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ X ∈ mod A R, ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)
Tactic:
fix X : Set A
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)
Tactic:
assume h2 : X ∈ mod A R
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)
Tactic:
fix Y : Set A
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
Y : Set A
⊢ Y ∈ mod A R → X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
Y : Set A
⊢ Y ∈ mod A R → X ≠ Y → empty (X ∩ Y)
Tactic:
assume h3 : Y ∈ mod A R
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
Y : Set A
h3 : Y ∈ mod A R
⊢ X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
Y : Set A
h3 : Y ∈ mod A R
⊢ X ≠ Y → empty (X ∩ Y)
Tactic:
define at h2
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : Y ∈ mod A R
⊢ X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : Y ∈ mod A R
⊢ X ≠ Y → empty (X ∩ Y)
Tactic:
define at h3
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
⊢ X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
⊢ X ≠ Y → empty (X ∩ Y)
Tactic:
obtain (x : A) (h4 : equivClass R x = X) from h2
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
⊢ X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
⊢ X ≠ Y → empty (X ∩ Y)
Tactic:
obtain (y : A) (h5 : equivClass R y = Y) from h3
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
⊢ X ≠ Y → empty (X ∩ Y)

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
⊢ X ≠ Y → empty (X ∩ Y)
Tactic:
contrapos
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
⊢ (∃ x, x ∈ X ∩ Y) → X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
⊢ (∃ x, x ∈ X ∩ Y) → X = Y
Tactic:
assume h6 : ∃ (x : A), x ∈ X ∩ Y
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
⊢ X = Y
Tactic:
obtain (z : A) (h7 : z ∈ X ∩ Y) from h6
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ X ∩ Y
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ X ∩ Y
⊢ X = Y
Tactic:
define at h7
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ X ∧ z ∈ Y
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ X ∧ z ∈ Y
⊢ X = Y
Tactic:
rewrite [←h4, ←h5] at h7
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
⊢ X = Y
Tactic:
have h8 : equivClass R z = equivClass R x :=
  (Lemma_4_5_5_2 R h x z).ltr h7.left
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
h8 : equivClass R z = equivClass R x
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
h8 : equivClass R z = equivClass R x
⊢ X = Y
Tactic:
have h9 : equivClass R z = equivClass R y :=
  (Lemma_4_5_5_2 R h y z).ltr h7.right
State after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
h8 : equivClass R z = equivClass R x
h9 : equivClass R z = equivClass R y
⊢ X = Y

State before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
Y : Set A
h3 : ∃ x, equivClass R x = Y
x : A
h4 : equivClass R x = X
y : A
h5 : equivClass R y = Y
h6 : ∃ x, x ∈ X ∩ Y
z : A
h7 : z ∈ equivClass R x ∧ z ∈ equivClass R y
h8 : equivClass R z = equivClass R x
h9 : equivClass R z = equivClass R y
⊢ X = Y
Tactic:
show X = Y from
  calc X
    _ = equivClass R x := h4.symm
    _ = equivClass R z := h8.symm
    _ = equivClass R y := h9
    _ = Y              := h5
State after:
no goals