internlm/Lean-Github huggingface dataset:
Theorem: HFSet.induction'
Proof state before:
case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y
Tactic:
rcases isAtom_eq_true_iff.mp H with ⟨a, rfl⟩
Proof state after:
case true.intro
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
a : atoms
ih : ∀ (z : HFSet atoms), z ∈ atom a → motive z
H : isAtom (atom a) = true
⊢ motive (atom a)
Theorem: HFSet.induction'
Proof state before:
case true.intro
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
a : atoms
ih : ∀ (z : HFSet atoms), z ∈ atom a → motive z
H : isAtom (atom a) = true
⊢ motive (atom a)
Tactic:
exact h₁ a
Proof state after:
no goals
Theorem: HFSet.induction'
Proof state before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y
Tactic:
classical
simpa [H] using h₂ y.toFinset (by simpa)
Proof state after:
no goals
Theorem: HFSet.induction'
Proof state before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y
Tactic:
simpa [H] using h₂ y.toFinset (by simpa)
Proof state after:
no goals
Theorem: HFSet.induction'
Proof state before:
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ ∀ (y_1 : HFSet atoms), y_1 ∈ toFinset y → motive y_1
Tactic:
simpa
Proof state after:
no goals
Theorem: Finset.map_id
Proof state before:
atoms : Type ?u.52518
α : Type u_1
x : Finset α
⊢ Finset.map
      { toFun := fun z => z,
        inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
      x =
    x
Tactic:
ext y
Proof state after:
case a
atoms : Type ?u.52518
α : Type u_1
x : Finset α
y : α
⊢ y ∈
      Finset.map
        { toFun := fun z => z,
          inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
        x ↔
    y ∈ x
Theorem: Finset.map_id
Proof state before:
case a
atoms : Type ?u.52518
α : Type u_1
x : Finset α
y : α
⊢ y ∈
      Finset.map
        { toFun := fun z => z,
          inj' := (_ : ∀ (a b : α), (fun z => z) a = (fun z => z) b → (fun z => z) a = (fun z => z) b) }
        x ↔
    y ∈ x
Tactic:
simp
Proof state after:
no goals
Theorem: HFSet.normalize_eq
Proof state before:
atoms : Type u_1
inst✝ : DecidableEq atoms
⊢ normalize = fun s => { val := s, property := (_ : s = s) }
Tactic:
ext s : 2
Proof state after:
case h.a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
⊢ ↑(normalize s) = ↑{ val := s, property := (_ : s = s) }
Theorem: HFSet.normalize_eq
Proof state before:
case h.a
atoms : Type u_1
inst✝ : DecidableEq atoms
s : HFSet atoms
⊢ ↑(normalize s) = ↑{ val := s, property := (_ : s = s) }
Tactic:
exact (normalize s).prop
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ 3 ∣ 0 ^ 3 + 2 * 0

case Induction_Step

⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Base_Case

⊢ 3 ∣ 0 ^ 3 + 2 * 0
Tactic:
define
Proof state after:
case Base_Case

⊢ ∃ c, 0 ^ 3 + 2 * 0 = 3 * c
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Base_Case

⊢ ∃ c, 0 ^ 3 + 2 * 0 = 3 * c
Tactic:
apply Exists.intro 0
Proof state after:
case Base_Case

⊢ 0 ^ 3 + 2 * 0 = 3 * 0
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Base_Case

⊢ 0 ^ 3 + 2 * 0 = 3 * 0
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step

⊢ ∀ (n : ℕ), 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
⊢ 3 ∣ n ^ 3 + 2 * n → 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
assume ih : 3 ∣ n ^ 3 + 2 * n
Proof state after:
case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
define at ih
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
obtain (k : Nat) (h1 : n ^ 3 + 2 * n = 3 * k) from ih
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 ∣ (n + 1) ^ 3 + 2 * (n + 1)
Tactic:
define
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ ∃ c, (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ ∃ c, (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
Tactic:
apply Exists.intro (k + n ^ 2 + n + 1)
Proof state after:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1)
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
case Induction_Step
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1)
Tactic:
show (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1) from
  calc (n + 1) ^ 3 + 2 * (n + 1)
    _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
    _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
    _ = 3 * (k + n ^ 2 + n + 1) := by ring
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ (n + 1) ^ 3 + 2 * (n + 1) = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 = 3 * k + 3 * n ^ 2 + 3 * n + 3
Tactic:
rw [h1]
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_2
Proof state before:
n : ℕ
ih : ∃ c, n ^ 3 + 2 * n = 3 * c
k : ℕ
h1 : n ^ 3 + 2 * n = 3 * k
⊢ 3 * k + 3 * n ^ 2 + 3 * n + 3 = 3 * (k + n ^ 2 + n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
⊢ ∀ (n : ℕ), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ (Sum i from 0 to 0, 2 ^ i) + 1 = 2 ^ (0 + 1)

case Induction_Step

⊢ ∀ (n : ℕ), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) → (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
case Base_Case

⊢ (Sum i from 0 to 0, 2 ^ i) + 1 = 2 ^ (0 + 1)
Tactic:
rewrite [sum_base]
Proof state after:
case Base_Case

⊢ 2 ^ 0 + 1 = 2 ^ (0 + 1)
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
case Base_Case

⊢ 2 ^ 0 + 1 = 2 ^ (0 + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
case Induction_Step

⊢ ∀ (n : ℕ), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) → (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) → (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
case Induction_Step
n : ℕ
⊢ (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) → (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Tactic:
assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
Proof state after:
case Induction_Step
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
case Induction_Step
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)
Tactic:
show (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1) from
  calc (Sum i from 0 to n + 1, 2 ^ i) + 1
    _ = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1 := by
          rw [sum_from_zero_step]
    _ = (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1) := by ring
    _ = 2 ^ (n + 1) + 2 ^ (n + 1) := by rw [ih]
    _ = 2 ^ (n + 1 + 1) := by ring
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ (Sum i from 0 to n + 1, 2 ^ i) + 1 = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1
Tactic:
rw [sum_from_zero_step]
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1 = (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1) = 2 ^ (n + 1) + 2 ^ (n + 1)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: HTPI.Like_Example_6_1_1
Proof state before:
n : ℕ
ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
⊢ 2 ^ (n + 1) + 2 ^ (n + 1) = 2 ^ (n + 1 + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ 2 ^ 5 > 5 ^ 2

case Induction_Step

⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Theorem: HTPI.Example_6_1_3
Proof state before:
case Base_Case

⊢ 2 ^ 5 > 5 ^ 2
Tactic:
decide
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
case Induction_Step

⊢ ∀ n ≥ 5, 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ n ≥ 5 → 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Theorem: HTPI.Example_6_1_3
Proof state before:
case Induction_Step
n : ℕ
⊢ n ≥ 5 → 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
assume h1 : n ≥ 5
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
⊢ 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Theorem: HTPI.Example_6_1_3
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
⊢ 2 ^ n > n ^ 2 → 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
assume ih : 2 ^ n > n ^ 2
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Theorem: HTPI.Example_6_1_3
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
have h2 : n * n ≥ 5 * n := Nat.mul_le_mul_right n h1
Proof state after:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Theorem: HTPI.Example_6_1_3
Proof state before:
case Induction_Step
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) > (n + 1) ^ 2
Tactic:
show 2 ^ (n + 1) > (n + 1) ^ 2 from
  calc 2 ^ (n + 1)
    _ = 2 * 2 ^ n := by ring
    _ > 2 * n ^ 2 := by linarith
    _ ≥ n ^ 2 + 5 * n := by linarith
    _ > n ^ 2 + 2 * n + 1 := by linarith
    _ = (n + 1) ^ 2 := by ring
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 ^ (n + 1) = 2 * 2 ^ n
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 * 2 ^ n > 2 * n ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ 2 * n ^ 2 ≥ n ^ 2 + 5 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ n ^ 2 + 5 * n > n ^ 2 + 2 * n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: HTPI.Example_6_1_3
Proof state before:
n : ℕ
h1 : n ≥ 5
ih : 2 ^ n > n ^ 2
h2 : n * n ≥ 5 * n
⊢ n ^ 2 + 2 * n + 1 = (n + 1) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Example_6_1_1
Proof state before:
⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
Tactic:
by_induc
Proof state after:
case Base_Case

⊢ Sum i from 0 to 0, 2 ^ i = 2 ^ (0 + 1) - 1

case Induction_Step

⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Theorem: HTPI.Example_6_1_1
Proof state before:
case Base_Case

⊢ Sum i from 0 to 0, 2 ^ i = 2 ^ (0 + 1) - 1
Tactic:
rewrite [sum_base]
Proof state after:
case Base_Case

⊢ 2 ^ 0 = 2 ^ (0 + 1) - 1
Theorem: HTPI.Example_6_1_1
Proof state before:
case Base_Case

⊢ 2 ^ 0 = 2 ^ (0 + 1) - 1
Tactic:
rfl
Proof state after:
no goals
Theorem: HTPI.Example_6_1_1
Proof state before:
case Induction_Step

⊢ ∀ (n : ℕ), Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
fix n : Nat
Proof state after:
case Induction_Step
n : ℕ
⊢ Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Theorem: HTPI.Example_6_1_1
Proof state before:
case Induction_Step
n : ℕ
⊢ Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1 → Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
assume ih : Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int)
Proof state after:
case Induction_Step
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Theorem: HTPI.Example_6_1_1
Proof state before:
case Induction_Step
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = 2 ^ (n + 1 + 1) - 1
Tactic:
show Sum i from 0 to n + 1, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1 + 1) - (1 : Int) from
  calc Sum i from 0 to n + 1, (2 : Int) ^ i
    _ = (Sum i from 0 to n, (2 : Int) ^ i)
        + (2 : Int) ^ (n + 1) := by rw [sum_from_zero_step]
    _ = (2 : Int) ^ (n + 1) - (1 : Int)
        + (2 : Int) ^ (n + 1) := by rw [ih]
    _ = (2 : Int) ^ (n + 1 + 1) - (1 : Int) := by ring
Proof state after:
no goals
Theorem: HTPI.Example_6_1_1
Proof state before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ Sum i from 0 to n + 1, 2 ^ i = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1)
Tactic:
rw [sum_from_zero_step]
Proof state after:
no goals
Theorem: HTPI.Example_6_1_1
Proof state before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) = 2 ^ (n + 1) - 1 + 2 ^ (n + 1)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: HTPI.Example_6_1_1
Proof state before:
n : ℕ
ih : Sum i from 0 to n, 2 ^ i = 2 ^ (n + 1) - 1
⊢ 2 ^ (n + 1) - 1 + 2 ^ (n + 1) = 2 ^ (n + 1 + 1) - 1
Tactic:
ring
Proof state after:
no goals
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : minimalElt R c (B \ {b})
h4 : R b c
⊢ minimalElt R b B
Tactic:
define at h3
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ minimalElt R b B
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ minimalElt R b B
Tactic:
define
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
apply And.intro h2
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
⊢ ¬∃ x ∈ B, R x b ∧ x ≠ b
Tactic:
contradict h3.right with h5
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Tactic:
obtain (x : A) (h6 : x ∈ B ∧ R x b ∧ x ≠ b) from h5
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ ∃ x ∈ B \ {b}, R x c ∧ x ≠ c
Tactic:
apply Exists.intro x
Proof state after:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b} ∧ R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b} ∧ R x c ∧ x ≠ c
Tactic:
apply And.intro
Proof state after:
case left
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b}

case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case left
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ x ∈ B \ {b}
Tactic:
show x ∈ B \ {b} from And.intro h6.left h6.right.right
Proof state after:
no goals
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
⊢ R x c ∧ x ≠ c
Tactic:
have Rtrans : transitive R := h1.right.left
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
⊢ R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
⊢ R x c ∧ x ≠ c
Tactic:
have h7 : R x c := Rtrans x b c h6.right.left h4
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ R x c ∧ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ R x c ∧ x ≠ c
Tactic:
apply And.intro h7
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ x ≠ c
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
⊢ x ≠ c
Tactic:
by_contra h8
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : x ∈ B ∧ R x b ∧ x ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Tactic:
rewrite [h8] at h6
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
⊢ False
Tactic:
have Rantisymm : antisymmetric R := h1.right.right
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
⊢ False
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
⊢ False
Tactic:
have h9 : c = b := Rantisymm c b h6.right.left h4
Proof state after:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
h9 : c = b
⊢ False
Theorem: HTPI.Lemma_6_2_1_1
Proof state before:
case right
A : Type
R : BinRel A
B : Set A
b c : A
h1 : partial_order R
h2 : b ∈ B
h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
h4 : R b c
h5 : ∃ x ∈ B, R x b ∧ x ≠ b
x : A
h6 : c ∈ B ∧ R c b ∧ c ≠ b
Rtrans : transitive R
h7 : R x c
h8 : x = c
Rantisymm : antisymmetric R
h9 : c = b
⊢ False
Tactic:
show False from h6.right.right h9
Proof state after:
no goals