internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
⊢ x ∈ F → x ∈ 𝒫 B
Tactic:
assume h2 : x ∈ F
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ x ∈ 𝒫 B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ x ∈ 𝒫 B
Tactic:
define
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ ∀ ⦃a : U⦄, a ∈ x → a ∈ B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
⊢ ∀ ⦃a : U⦄, a ∈ x → a ∈ B
Tactic:
fix y : U
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
⊢ y ∈ x → y ∈ B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
⊢ y ∈ x → y ∈ B
Tactic:
assume h3 : y ∈ x
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ⋃₀ F ⊆ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Tactic:
define at h1
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ B
Tactic:
apply h1 _
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ ⋃₀ F
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ y ∈ ⋃₀ F
Tactic:
define
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ ∃ t ∈ F, y ∈ t
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ ∃ t ∈ F, y ∈ t
Tactic:
apply Exists.intro x _
Proof state after:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ x ∈ F ∧ y ∈ x
Theorem: HTPI.Example_3_3_5
Proof state before:
U : Type
B : Set U
F : Set (Set U)
h1 : ∀ ⦃a : U⦄, a ∈ ⋃₀ F → a ∈ B
x : Set U
h2 : x ∈ F
y : U
h3 : y ∈ x
⊢ x ∈ F ∧ y ∈ x
Tactic:
show x ∈ F ∧ y ∈ x from And.intro h2 h3
Proof state after:
no goals
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ A ∩ C ⊆ B \ D
Tactic:
define
Proof state after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ ∀ ⦃a : U⦄, a ∈ A ∩ C → a ∈ B \ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
⊢ ∀ ⦃a : U⦄, a ∈ A ∩ C → a ∈ B \ D
Tactic:
fix x : U
Proof state after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
⊢ x ∈ A ∩ C → x ∈ B \ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
⊢ x ∈ A ∩ C → x ∈ B \ D
Tactic:
assume h3 : x ∈ A ∩ C
Proof state after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∩ C
⊢ x ∈ B \ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∩ C
⊢ x ∈ B \ D
Tactic:
define at h3
Proof state after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B \ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B \ D
Tactic:
define
Proof state after:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B ∧ x ∉ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B ∧ x ∉ D
Tactic:
apply And.intro
Proof state after:
case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B

case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
case left
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∈ B
Tactic:
show x ∈ B from h1 h3.left
Proof state after:
no goals
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
⊢ x ∉ D
Tactic:
contradict h2 with h4
Proof state after:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ ∃ c, c ∈ C ∩ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ ∃ c, c ∈ C ∩ D
Tactic:
apply Exists.intro x
Proof state after:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ x ∈ C ∩ D
Theorem: HTPI.Like_Example_3_4_1
Proof state before:
case right
U : Type
A B C D : Set U
h1 : A ⊆ B
h2 : ¬∃ c, c ∈ C ∩ D
x : U
h3 : x ∈ A ∧ x ∈ C
h4 : x ∈ D
⊢ x ∈ C ∩ D
Tactic:
show x ∈ C ∩ D from And.intro h3.right h4
Proof state after:
no goals
Theorem: HTPI.Example_3_4_5
Proof state before:
U : Type
A B C : Set U
⊢ A ∩ (B \ C) = (A ∩ B) \ C
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
A B C : Set U
⊢ ∀ (x : U), x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Theorem: HTPI.Example_3_4_5
Proof state before:
case h
U : Type
A B C : Set U
⊢ ∀ (x : U), x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Tactic:
fix x : U
Proof state after:
case h
U : Type
A B C : Set U
x : U
⊢ x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Theorem: HTPI.Example_3_4_5
Proof state before:
case h
U : Type
A B C : Set U
x : U
⊢ x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C
Tactic:
show x ∈ A ∩ (B \ C) ↔ x ∈ (A ∩ B) \ C from
  calc x ∈ A ∩ (B \ C)
    _ ↔ x ∈ A ∧ (x ∈ B ∧ x ∉ C) := Iff.refl _
    _ ↔ (x ∈ A ∧ x ∈ B) ∧ x ∉ C := and_assoc.symm
    _ ↔ x ∈ (A ∩ B) \ C := Iff.refl _
Proof state after:
no goals
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
⊢ A \ (B \ C) ⊆ A \ B ∪ C
Tactic:
fix x : U
Proof state after:
U : Type
A B C : Set U
x : U
⊢ x ∈ A \ (B \ C) → x ∈ A \ B ∪ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
⊢ x ∈ A \ (B \ C) → x ∈ A \ B ∪ C
Tactic:
assume h1 : x ∈ A \ (B \ C)
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∪ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∪ C
Tactic:
define
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A \ (B \ C)
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
define at h1
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
have h2 : x ∉ B \ C := h1.right
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B \ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
define at h2
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : ¬(x ∈ B ∧ x ∉ C)
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : ¬(x ∈ B ∧ x ∉ C)
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
demorgan at h2
Proof state after:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B ∨ x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B ∨ x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
by_cases on h2
Proof state after:
case Case_1
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B ∨ x ∈ C

case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
case Case_1
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
apply Or.inl
Proof state after:
case Case_1.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B
Theorem: HTPI.Example_3_5_2
Proof state before:
case Case_1.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∉ B
⊢ x ∈ A \ B
Tactic:
show x ∈ A \ B from And.intro h1.left h2
Proof state after:
no goals
Theorem: HTPI.Example_3_5_2
Proof state before:
case Case_2
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ A \ B ∨ x ∈ C
Tactic:
apply Or.inr
Proof state after:
case Case_2.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ C
Theorem: HTPI.Example_3_5_2
Proof state before:
case Case_2.h
U : Type
A B C : Set U
x : U
h1 : x ∈ A ∧ x ∉ B \ C
h2 : x ∈ C
⊢ x ∈ C
Tactic:
show x ∈ C from h2
Proof state after:
no goals
Theorem: HTPI.empty_union
Proof state before:
U : Type
B : Set U
⊢ ∅ ∪ B = B
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
B : Set U
⊢ ∀ (x : U), x ∈ ∅ ∪ B ↔ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h
U : Type
B : Set U
⊢ ∀ (x : U), x ∈ ∅ ∪ B ↔ x ∈ B
Tactic:
fix x : U
Proof state after:
case h
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B ↔ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B ↔ x ∈ B
Tactic:
apply Iff.intro
Proof state after:
case h.mp
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B → x ∈ B

case h.mpr
U : Type
B : Set U
x : U
⊢ x ∈ B → x ∈ ∅ ∪ B
Theorem: HTPI.empty_union
Proof state before:
case h.mp
U : Type
B : Set U
x : U
⊢ x ∈ ∅ ∪ B → x ∈ B
Tactic:
assume h1 : x ∈ ∅ ∪ B
Proof state after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∪ B
⊢ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∪ B
⊢ x ∈ B
Tactic:
define at h1
Proof state after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∈ B
Tactic:
have h2 : x ∉ ∅ := by
  by_contra h3
  define at h3  show False from h3
  done
Proof state after:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h2 : x ∉ ∅
⊢ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h.mp
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h2 : x ∉ ∅
⊢ x ∈ B
Tactic:
disj_syll h1 h2
Proof state after:
case h.mp
U : Type
B : Set U
x : U
h2 : x ∉ ∅
h1 : x ∈ B
⊢ x ∈ B
Theorem: HTPI.empty_union
Proof state before:
case h.mp
U : Type
B : Set U
x : U
h2 : x ∉ ∅
h1 : x ∈ B
⊢ x ∈ B
Tactic:
show x ∈ B from h1
Proof state after:
no goals
Theorem: HTPI.empty_union
Proof state before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
⊢ x ∉ ∅
Tactic:
by_contra h3
Proof state after:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : x ∈ ∅
⊢ False
Theorem: HTPI.empty_union
Proof state before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : x ∈ ∅
⊢ False
Tactic:
define at h3
Proof state after:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : False
⊢ False
Theorem: HTPI.empty_union
Proof state before:
U : Type
B : Set U
x : U
h1 : x ∈ ∅ ∨ x ∈ B
h3 : False
⊢ False
Tactic:
show False from h3
Proof state after:
no goals
Theorem: HTPI.empty_union
Proof state before:
case h.mpr
U : Type
B : Set U
x : U
⊢ x ∈ B → x ∈ ∅ ∪ B
Tactic:
assume h1 : x ∈ B
Proof state after:
case h.mpr
U : Type
B : Set U
x : U
h1 : x ∈ B
⊢ x ∈ ∅ ∪ B
Theorem: HTPI.empty_union
Proof state before:
case h.mpr
U : Type
B : Set U
x : U
h1 : x ∈ B
⊢ x ∈ ∅ ∪ B
Tactic:
show x ∈ ∅ ∪ B from Or.inr h1
Proof state after:
no goals
Theorem: HTPI.union_comm
Proof state before:
U : Type
X Y : Set U
⊢ X ∪ Y = Y ∪ X
Tactic:
apply Set.ext
Proof state after:
case h
U : Type
X Y : Set U
⊢ ∀ (x : U), x ∈ X ∪ Y ↔ x ∈ Y ∪ X
Theorem: HTPI.union_comm
Proof state before:
case h
U : Type
X Y : Set U
⊢ ∀ (x : U), x ∈ X ∪ Y ↔ x ∈ Y ∪ X
Tactic:
fix x : U
Proof state after:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X
Theorem: HTPI.union_comm
Proof state before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∪ Y ↔ x ∈ Y ∪ X
Tactic:
define : x ∈ X ∪ Y
Proof state after:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∪ X
Theorem: HTPI.union_comm
Proof state before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∪ X
Tactic:
define : x ∈ Y ∪ X
Proof state after:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X
Theorem: HTPI.union_comm
Proof state before:
case h
U : Type
X Y : Set U
x : U
⊢ x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X
Tactic:
show x ∈ X ∨ x ∈ Y ↔ x ∈ Y ∨ x ∈ X from or_comm
Proof state after:
no goals
Theorem: HTPI.Example_3_6_2
Proof state before:
U : Type
⊢ ∃! A, ∀ (B : Set U), A ∪ B = B
Tactic:
exists_unique
Proof state after:
case Existence
U : Type
⊢ ∃ A, ∀ (B : Set U), A ∪ B = B

case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U), (∀ (B : Set U), A_1 ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → A_1 = A_2
Theorem: HTPI.Example_3_6_2
Proof state before:
case Existence
U : Type
⊢ ∃ A, ∀ (B : Set U), A ∪ B = B
Tactic:
apply Exists.intro ∅
Proof state after:
case Existence
U : Type
⊢ ∀ (B : Set U), ∅ ∪ B = B
Theorem: HTPI.Example_3_6_2
Proof state before:
case Existence
U : Type
⊢ ∀ (B : Set U), ∅ ∪ B = B
Tactic:
show ∀ (B : Set U), ∅ ∪ B = B from empty_union
Proof state after:
no goals
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
⊢ ∀ (A_1 A_2 : Set U), (∀ (B : Set U), A_1 ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → A_1 = A_2
Tactic:
fix C : Set U
Proof state after:
case Uniqueness
U : Type
C : Set U
⊢ ∀ (A_2 : Set U), (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → C = A_2
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C : Set U
⊢ ∀ (A_2 : Set U), (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), A_2 ∪ B = B) → C = A_2
Tactic:
fix D : Set U
Proof state after:
case Uniqueness
U : Type
C D : Set U
⊢ (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), D ∪ B = B) → C = D
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C D : Set U
⊢ (∀ (B : Set U), C ∪ B = B) → (∀ (B : Set U), D ∪ B = B) → C = D
Tactic:
assume h1 : ∀ (B : Set U), C ∪ B = B
Proof state after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
⊢ (∀ (B : Set U), D ∪ B = B) → C = D
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
⊢ (∀ (B : Set U), D ∪ B = B) → C = D
Tactic:
assume h2 : ∀ (B : Set U), D ∪ B = B
Proof state after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
⊢ C = D
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
⊢ C = D
Tactic:
have h3 : C ∪ D = D := h1 D
Proof state after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
⊢ C = D
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
⊢ C = D
Tactic:
have h4 : D ∪ C = C := h2 C
Proof state after:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
h4 : D ∪ C = C
⊢ C = D
Theorem: HTPI.Example_3_6_2
Proof state before:
case Uniqueness
U : Type
C D : Set U
h1 : ∀ (B : Set U), C ∪ B = B
h2 : ∀ (B : Set U), D ∪ B = B
h3 : C ∪ D = D
h4 : D ∪ C = C
⊢ C = D
Tactic:
show C = D from
  calc C
    _ = D ∪ C := h4.symm
    _ = C ∪ D := union_comm D C
    _ = D := h3
Proof state after:
no goals
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (b : U) (h4 : b ∈ A ∩ B) from h1
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (c : U) (h5 : c ∈ A ∩ C) from h2
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
⊢ ∃ x, x ∈ B ∩ C
Tactic:
obtain (a : U) (h6 : a ∈ A) (h7 : ∀ (y z : U),
  y ∈ A → z ∈ A → y = z)  from h3
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∩ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
define at h4
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∩ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
define at h5
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
⊢ ∃ x, x ∈ B ∩ C
Tactic:
have h8 : b = c := h7 b c h4.left h5.left
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b : U
h4 : b ∈ A ∧ b ∈ B
c : U
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Tactic:
rewrite [h8] at h4
Proof state after:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b c : U
h4 : c ∈ A ∧ c ∈ B
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Theorem: HTPI.Example_3_6_4
Proof state before:
U : Type
A B C : Set U
h1 : ∃ x, x ∈ A ∩ B
h2 : ∃ x, x ∈ A ∩ C
h3 : ∃! x, x ∈ A
b c : U
h4 : c ∈ A ∧ c ∈ B
h5 : c ∈ A ∧ c ∈ C
a : U
h6 : a ∈ A
h7 : ∀ (x_1 x_2 : U), x_1 ∈ A → x_2 ∈ A → x_1 = x_2
h8 : b = c
⊢ ∃ x, x ∈ B ∩ C
Tactic:
show ∃ (x : U), x ∈ B ∩ C from
  Exists.intro c (And.intro h4.right h5.right)
Proof state after:
no goals
Theorem: HTPI.Theorem_3_3_7
Proof state before:
⊢ ∀ (a b c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix a : Int
Proof state after:
a : ℤ
⊢ ∀ (b c : ℤ), a ∣ b → b ∣ c → a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a : ℤ
⊢ ∀ (b c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix b : Int
Proof state after:
a b : ℤ
⊢ ∀ (c : ℤ), a ∣ b → b ∣ c → a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b : ℤ
⊢ ∀ (c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix c : Int
Proof state after:
a b c : ℤ
⊢ a ∣ b → b ∣ c → a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
⊢ a ∣ b → b ∣ c → a ∣ c
Tactic:
assume h1 : a ∣ b
Proof state after:
a b c : ℤ
h1 : a ∣ b
⊢ b ∣ c → a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : a ∣ b
⊢ b ∣ c → a ∣ c
Tactic:
assume h2 : b ∣ c
Proof state after:
a b c : ℤ
h1 : a ∣ b
h2 : b ∣ c
⊢ a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : a ∣ b
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h1
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h2
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c
Tactic:
define
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (m : Int) (h3 : b = a * m) from h1
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (n : Int) (h4 : c = b * n) from h2
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1
Tactic:
rewrite [h3] at h4
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ ∃ c_1, c = a * c_1
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ ∃ c_1, c = a * c_1
Tactic:
apply Exists.intro (m * n)
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ c = a * (m * n)
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * m * n
⊢ c = a * (m * n)
Tactic:
rewrite [mul_assoc a m n] at h4
Proof state after:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * (m * n)
⊢ c = a * (m * n)
Theorem: HTPI.Theorem_3_3_7
Proof state before:
a b c : ℤ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℤ
h3 : b = a * m
n : ℤ
h4 : c = a * (m * n)
⊢ c = a * (m * n)
Tactic:
show c = a * (m * n) from h4
Proof state after:
no goals
Theorem: HTPI.Theorem_3_4_7
Proof state before:
⊢ ∀ (n : ℤ), 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n
Tactic:
fix n : Int
Proof state after:
n : ℤ
⊢ 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
n : ℤ
⊢ 6 ∣ n ↔ 2 ∣ n ∧ 3 ∣ n
Tactic:
apply Iff.intro
Proof state after:
case mp
n : ℤ
⊢ 6 ∣ n → 2 ∣ n ∧ 3 ∣ n

case mpr
n : ℤ
⊢ 2 ∣ n ∧ 3 ∣ n → 6 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp
n : ℤ
⊢ 6 ∣ n → 2 ∣ n ∧ 3 ∣ n
Tactic:
assume h1 : 6 ∣ n
Proof state after:
case mp
n : ℤ
h1 : 6 ∣ n
⊢ 2 ∣ n ∧ 3 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp
n : ℤ
h1 : 6 ∣ n
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
define at h1
Proof state after:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
⊢ 2 ∣ n ∧ 3 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
obtain (k : Int) (h2 : n = 6 * k) from h1
Proof state after:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n ∧ 3 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n ∧ 3 ∣ n
Tactic:
apply And.intro
Proof state after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n

case mp.right
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 3 ∣ n
Theorem: HTPI.Theorem_3_4_7
Proof state before:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ 2 ∣ n
Tactic:
define
Proof state after:
case mp.left
n : ℤ
h1 : ∃ c, n = 6 * c
k : ℤ
h2 : n = 6 * k
⊢ ∃ c, n = 2 * c