internlm/Lean-Github huggingface dataset:
Theorem: exercise4_1
Proof state before:
n : ℕ
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Tactic:
have : ∀ n, (∑ i in range (n + 1), i : ℚ) = n * (n + 1) / 2
Proof state after:
case this
n : ℕ
⊢ ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2

n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Theorem: exercise4_1
Proof state before:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (∑ i in range (n + 1), ↑i) ^ 2
Tactic:
rw [this]
Proof state after:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
Theorem: exercise4_1
Proof state before:
n : ℕ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
Tactic:
induction n with
| zero => simp
| succ n ih =>
  rw [sum_range_succ, ih]
  push_cast
  ring
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
case this
n : ℕ
⊢ ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
Tactic:
intro n
Proof state after:
case this
n✝ n : ℕ
⊢ ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
Theorem: exercise4_1
Proof state before:
case this
n✝ n : ℕ
⊢ ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
Tactic:
induction n with
| zero => simp
| succ n ih =>
rw [sum_range_succ, ih]
push_cast
ring
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
case this.zero
n : ℕ
⊢ ∑ i in range (0 + 1), ↑i = ↑0 * (↑0 + 1) / 2
Tactic:
simp
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (n + 1 + 1), ↑i = ↑(n + 1) * (↑(n + 1) + 1) / 2
Tactic:
rw [sum_range_succ, ih]
Proof state after:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + ↑(n + 1) = ↑(n + 1) * (↑(n + 1) + 1) / 2
Theorem: exercise4_1
Proof state before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + ↑(n + 1) = ↑(n + 1) * (↑(n + 1) + 1) / 2
Tactic:
push_cast
Proof state after:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + (↑n + 1) = (↑n + 1) * (↑n + 1 + 1) / 2
Theorem: exercise4_1
Proof state before:
case this.succ
n✝ n : ℕ
ih : ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ↑n * (↑n + 1) / 2 + (↑n + 1) = (↑n + 1) * (↑n + 1 + 1) / 2
Tactic:
ring
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
case zero
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
⊢ ∑ i in range (0 + 1), ↑(i ^ 3) = (↑0 * (↑0 + 1) / 2) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: exercise4_1
Proof state before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ ∑ i in range (n + 1 + 1), ↑(i ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2
Tactic:
rw [sum_range_succ, ih]
Proof state after:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + ↑((n + 1) ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2
Theorem: exercise4_1
Proof state before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + ↑((n + 1) ^ 3) = (↑(n + 1) * (↑(n + 1) + 1) / 2) ^ 2
Tactic:
push_cast
Proof state after:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + (↑n + 1) ^ 3 = ((↑n + 1) * (↑n + 1 + 1) / 2) ^ 2
Theorem: exercise4_1
Proof state before:
case succ
this : ∀ (n : ℕ), ∑ i in range (n + 1), ↑i = ↑n * (↑n + 1) / 2
n : ℕ
ih : ∑ i in range (n + 1), ↑(i ^ 3) = (↑n * (↑n + 1) / 2) ^ 2
⊢ (↑n * (↑n + 1) / 2) ^ 2 + (↑n + 1) ^ 3 = ((↑n + 1) * (↑n + 1 + 1) / 2) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: exercise4_2
Proof 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)
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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)
Theorem: exercise4_2
Proof 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]
Proof 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
Theorem: exercise4_2
Proof 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
Proof state after:
no goals
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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
Proof state after:
no goals
Theorem: exercise4_2
Proof 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
Proof state after:
no goals
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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]
Proof 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
Theorem: exercise4_2
Proof 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?
Proof state after:
no goals
Theorem: exercise4_2
Proof 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]
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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⟩
Proof 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
Theorem: exercise4_2
Proof 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₀
Proof 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₀
Theorem: exercise4_2
Proof 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]
Proof 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
Theorem: exercise4_2
Proof 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₀
Proof 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
Theorem: exercise4_2
Proof 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
Proof 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
Theorem: exercise4_2
Proof 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
Proof state after:
no goals
Theorem: exercise4_3
Proof state before:
x y z : PosReal
⊢ x * y * z = x * (y * z)
Tactic:
ext
Proof state after:
case h
x y z : PosReal
⊢ ↑(x * y * z) = ↑(x * (y * z))
Theorem: exercise4_3
Proof state before:
case h
x y z : PosReal
⊢ ↑(x * y * z) = ↑(x * (y * z))
Tactic:
apply mul_assoc
Proof state after:
no goals
Theorem: exercise4_3
Proof state before:
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: exercise4_3
Proof state before:
x : PosReal
⊢ 1 * x = x
Tactic:
ext
Proof state after:
case h
x : PosReal
⊢ ↑(1 * x) = ↑x
Theorem: exercise4_3
Proof state before:
case h
x : PosReal
⊢ ↑(1 * x) = ↑x
Tactic:
apply one_mul
Proof state after:
no goals
Theorem: exercise4_3
Proof state before:
x : PosReal
⊢ x * 1 = x
Tactic:
ext
Proof state after:
case h
x : PosReal
⊢ ↑(x * 1) = ↑x
Theorem: exercise4_3
Proof state before:
case h
x : PosReal
⊢ ↑(x * 1) = ↑x
Tactic:
apply mul_one
Proof state after:
no goals
Theorem: exercise4_3
Proof state before:
x : PosReal
⊢ x⁻¹ * x = 1
Tactic:
ext
Proof state after:
case h
x : PosReal
⊢ ↑(x⁻¹ * x) = ↑1
Theorem: exercise4_3
Proof state before:
case h
x : PosReal
⊢ ↑(x⁻¹ * x) = ↑1
Tactic:
apply inv_mul_cancel
Proof state after:
case h.h
x : PosReal
⊢ ↑x ≠ 0
Theorem: exercise4_3
Proof state before:
case h.h
x : PosReal
⊢ ↑x ≠ 0
Tactic:
exact x.2.ne'
Proof state after:
no goals
Theorem: exercise4_4
Proof state before:
n : ℕ
⊢ ¬Nat.Prime n ↔ n = 0 ∨ n = 1 ∨ ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
rw [← or_assoc, ← Nat.le_one_iff_eq_zero_or_eq_one, ← not_lt, ← imp_iff_not_or, Nat.prime_def_lt']
Proof state after:
n : ℕ
⊢ ¬(2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m < n → ¬m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Theorem: exercise4_4
Proof state before:
n : ℕ
⊢ ¬(2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m < n → ¬m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
push_neg
Proof state after:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Theorem: exercise4_4
Proof state before:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a b, 2 ≤ a ∧ 2 ≤ b ∧ n = a * b
Tactic:
simp
Proof state after:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Theorem: exercise4_4
Proof state before:
n : ℕ
⊢ (2 ≤ n → ∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ 1 < n → ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
apply imp_congr
Proof state after:
case h₁
n : ℕ
⊢ 2 ≤ n ↔ 1 < n

case h₂
n : ℕ
⊢ (∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Theorem: exercise4_4
Proof state before:
case h₂
n : ℕ
⊢ (∃ m, 2 ≤ m ∧ m < n ∧ m ∣ n) ↔ ∃ a, 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
apply exists_congr
Proof state after:
case h₂.h
n : ℕ
⊢ ∀ (a : ℕ), 2 ≤ a ∧ a < n ∧ a ∣ n ↔ 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Theorem: exercise4_4
Proof state before:
case h₂.h
n : ℕ
⊢ ∀ (a : ℕ), 2 ≤ a ∧ a < n ∧ a ∣ n ↔ 2 ≤ a ∧ ∃ x, 2 ≤ x ∧ n = a * x
Tactic:
intro k
Proof state after:
case h₂.h
n k : ℕ
⊢ 2 ≤ k ∧ k < n ∧ k ∣ n ↔ 2 ≤ k ∧ ∃ x, 2 ≤ x ∧ n = k * x
Theorem: exercise4_4
Proof state before:
case h₂.h
n k : ℕ
⊢ 2 ≤ k ∧ k < n ∧ k ∣ n ↔ 2 ≤ k ∧ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
apply and_congr_right
Proof state after:
case h₂.h.h
n k : ℕ
⊢ 2 ≤ k → (k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x)
Theorem: exercise4_4
Proof state before:
case h₂.h.h
n k : ℕ
⊢ 2 ≤ k → (k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x)
Tactic:
intro hk
Proof state after:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x
Theorem: exercise4_4
Proof state before:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ k < n ∧ k ∣ n ↔ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
rw [dvd_def, ← exists_and_left]
Proof state after:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ (∃ x, k < n ∧ n = k * x) ↔ ∃ x, 2 ≤ x ∧ n = k * x
Theorem: exercise4_4
Proof state before:
case h₂.h.h
n k : ℕ
hk : 2 ≤ k
⊢ (∃ x, k < n ∧ n = k * x) ↔ ∃ x, 2 ≤ x ∧ n = k * x
Tactic:
apply exists_congr
Proof state after:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
⊢ ∀ (a : ℕ), k < n ∧ n = k * a ↔ 2 ≤ a ∧ n = k * a
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
⊢ ∀ (a : ℕ), k < n ∧ n = k * a ↔ 2 ≤ a ∧ n = k * a
Tactic:
intro l
Proof state after:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < n ∧ n = k * l ↔ 2 ≤ l ∧ n = k * l
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < n ∧ n = k * l ↔ 2 ≤ l ∧ n = k * l
Tactic:
apply and_congr_left
Proof state after:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ n = k * l → (k < n ↔ 2 ≤ l)
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ n = k * l → (k < n ↔ 2 ≤ l)
Tactic:
intro h
Proof state after:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
h : n = k * l
⊢ k < n ↔ 2 ≤ l
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h.h
n k : ℕ
hk : 2 ≤ k
l : ℕ
h : n = k * l
⊢ k < n ↔ 2 ≤ l
Tactic:
subst h
Proof state after:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 2 ≤ l
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 2 ≤ l
Tactic:
rw [succ_le]
Proof state after:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 1 < l
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h.h
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ k < k * l ↔ 1 < l
Tactic:
apply lt_mul_iff_one_lt_right
Proof state after:
case h₂.h.h.h.h.a0
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ 0 < k
Theorem: exercise4_4
Proof state before:
case h₂.h.h.h.h.a0
k : ℕ
hk : 2 ≤ k
l : ℕ
⊢ 0 < k
Tactic:
linarith
Proof state after:
no goals
Theorem: exercise4_4
Proof state before:
case h₁
n : ℕ
⊢ 2 ≤ n ↔ 1 < n
Tactic:
rw?
Proof state after:
no goals