internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ (x : A), x ∈ ⋃₀ mod A R
Tactic:
fix x : A
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ ⋃₀ mod A R
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ x ∈ ⋃₀ mod A R
Tactic:
define
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ t ∈ mod A R, x ∈ t
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ t ∈ mod A R, x ∈ t
Tactic:
apply Exists.intro (equivClass R x)
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R ∧ x ∈ equivClass R x
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R ∧ x ∈ equivClass R x
Tactic:
apply And.intro _ (Lemma_4_5_5_1 R h x)
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x ∈ mod A R
Tactic:
define
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ x_1, equivClass R x_1 = equivClass R x
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ ∃ x_1, equivClass R x_1 = equivClass R x
Tactic:
apply Exists.intro x
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x = equivClass R x
Theorem: HTPI.Theorem_4_5_4_part_1
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
x : A
⊢ equivClass R x = equivClass R x
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Theorem_4_5_4_part_2
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ pairwise_disjoint (mod A R)
Tactic:
define
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ X ∈ mod A R, ∀ Y ∈ mod A R, X ≠ Y → empty (X ∩ Y)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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)
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_4_part_2
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
⊢ ∀ X ∈ mod A R, ¬empty X
Tactic:
fix X : Set A
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ¬empty X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
⊢ X ∈ mod A R → ¬empty X
Tactic:
assume h2 : X ∈ mod A R
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬empty X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬empty X
Tactic:
define
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬¬∃ x, x ∈ X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ¬¬∃ x, x ∈ X
Tactic:
double_neg
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∃ x, x ∈ X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : X ∈ mod A R
⊢ ∃ x, x ∈ X
Tactic:
define at h2
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ ∃ x, x ∈ X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
⊢ ∃ x, x ∈ X
Tactic:
obtain (x : A) (h3 : equivClass R x = X) from h2
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x, x ∈ X
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x, x ∈ X
Tactic:
rewrite [←h3]
Proof state after:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x_1, x_1 ∈ equivClass R x
Theorem: HTPI.Theorem_4_5_4_part_3
Proof state before:
A : Type
R : BinRel A
h : equiv_rel R
X : Set A
h2 : ∃ x, equivClass R x = X
x : A
h3 : equivClass R x = X
⊢ ∃ x_1, x_1 ∈ equivClass R x
Tactic:
show ∃ (x_1 : A), x_1 ∈ equivClass R x from
  Exists.intro x (Lemma_4_5_5_1 R h x)
Proof state after:
no goals
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof state after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ ∃ R, equiv_rel R ∧ mod A R = F
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof state after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ equiv_rel R ∧ mod A R = F
Theorem: HTPI.Theorem_4_5_6
Proof 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)
Proof state after:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ mod A R = F
Theorem: HTPI.Theorem_4_5_6
Proof state before:
A : Type
F : Set (Set A)
h : partition F
R : BinRel A := EqRelFromPart F
⊢ mod A R = F
Tactic:
apply Set.ext
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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]
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof state after:
no goals
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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
Proof 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
Theorem: HTPI.Theorem_4_5_6
Proof 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)
Proof state after:
no goals
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
⊢ ¬R → P → ¬Q
Tactic:
assume h2 : ¬R
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Tactic:
assume h3 : P
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Tactic:
by_contra h4
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False
Tactic:
have h5 : Q → R := h h3
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
⊢ False
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
⊢ False
Tactic:
have h6 : R := h5 h4
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
h6 : R
⊢ False
Theorem: HTPI.Example_3_2_4_v2
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
h5 : Q → R
h6 : R
⊢ False
Tactic:
show False from h2 h6
Proof state after:
no goals
Theorem: HTPI.Example_3_2_4_v3
Proof state before:
P Q R : Prop
h : P → Q → R
⊢ ¬R → P → ¬Q
Tactic:
assume h2 : ¬R
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Theorem: HTPI.Example_3_2_4_v3
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
⊢ P → ¬Q
Tactic:
assume h3 : P
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Theorem: HTPI.Example_3_2_4_v3
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
⊢ ¬Q
Tactic:
by_contra h4
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False
Theorem: HTPI.Example_3_2_4_v3
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ False
Tactic:
contradict h2
Proof state after:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ R
Theorem: HTPI.Example_3_2_4_v3
Proof state before:
P Q R : Prop
h : P → Q → R
h2 : ¬R
h3 : P
h4 : Q
⊢ R
Tactic:
show R from h h3 h4
Proof state after:
no goals
Theorem: HTPI.Like_Example_3_2_5
Proof state before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ C
Tactic:
apply h3 _
Proof state after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Theorem: HTPI.Like_Example_3_2_5
Proof state before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
define at h2
Proof state after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : ¬(a ∈ A ∧ a ∉ B)
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Theorem: HTPI.Like_Example_3_2_5
Proof state before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : ¬(a ∈ A ∧ a ∉ B)
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
demorgan at h2
Proof state after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A ∨ a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Theorem: HTPI.Like_Example_3_2_5
Proof state before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A ∨ a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
conditional at h2
Proof state after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∈ A → a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Theorem: HTPI.Like_Example_3_2_5
Proof state before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∈ A → a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
show a ∈ B from h2 h1
Proof state after:
no goals
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
⊢ ⋃₀ F ⊆ B → F ⊆ 𝒫 B
Tactic:
assume h1 : ⋃₀ F ⊆ B
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ F ⊆ 𝒫 B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ F ⊆ 𝒫 B
Tactic:
define
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ ∀ ⦃a : Set U⦄, a ∈ F → a ∈ 𝒫 B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
⊢ ∀ ⦃a : Set U⦄, a ∈ F → a ∈ 𝒫 B
Tactic:
fix x : Set U
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
⊢ x ∈ F → x ∈ 𝒫 B