internlm/Lean-Github huggingface dataset:
Theorem: ordered_insert_is_ordered
Proof state before:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (insert' a (x :: xs))
Tactic:
rw [insert']
Proof state after:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (if a ≤ x then a :: x :: xs else x :: insert' a xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case cons
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
⊢ List.Pairwise LE.le (if a ≤ x then a :: x :: xs else x :: insert' a xs)
Tactic:
split_ifs with h
Proof state after:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (a :: x :: xs)

case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ List.Pairwise LE.le (x :: insert' a xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (a :: x :: xs)
Tactic:
rw [List.pairwise_cons]
Proof state after:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ (∀ a' ∈ x :: xs, a ≤ a') ∧ List.Pairwise LE.le (x :: xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ (∀ a' ∈ x :: xs, a ≤ a') ∧ List.Pairwise LE.le (x :: xs)
Tactic:
constructor
Proof state after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ ∀ a' ∈ x :: xs, a ≤ a'

case pos.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (x :: xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ ∀ a' ∈ x :: xs, a ≤ a'
Tactic:
intro y hy
Proof state after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y ∈ x :: xs
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y ∈ x :: xs
⊢ a ≤ y
Tactic:
rw [List.mem_cons] at hy
Proof state after:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y = x ∨ y ∈ xs
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hy : y = x ∨ y ∈ xs
⊢ a ≤ y
Tactic:
rcases hy with (heq | hmem)
Proof state after:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ y

case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ y
Tactic:
rw [heq]
Proof state after:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ x
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
heq : y = x
⊢ a ≤ x
Tactic:
exact h
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Tactic:
rw [List.pairwise_cons] at ordered
Proof state after:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
⊢ a ≤ y
Tactic:
have hle := ordered.1 y hmem
Proof state after:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
hle : x ≤ y
⊢ a ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : a ≤ x
y : α
hmem : y ∈ xs
hle : x ≤ y
⊢ a ≤ y
Tactic:
exact ge_trans hle h
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case pos.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (x :: xs)
Tactic:
exact ordered
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ List.Pairwise LE.le (x :: insert' a xs)
Tactic:
rw [List.pairwise_cons]
Proof state after:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Tactic:
rw [List.pairwise_cons] at ordered
Proof state after:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case neg
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ (∀ a' ∈ insert' a xs, x ≤ a') ∧ List.Pairwise LE.le (insert' a xs)
Tactic:
constructor
Proof state after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ ∀ a' ∈ insert' a xs, x ≤ a'

case neg.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ List.Pairwise LE.le (insert' a xs)
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ ∀ a' ∈ insert' a xs, x ≤ a'
Tactic:
intros y hy
Proof state after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y ∈ insert' a xs
⊢ x ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y ∈ insert' a xs
⊢ x ≤ y
Tactic:
rw [insert_mem] at hy
Proof state after:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y = a ∨ y ∈ xs
⊢ x ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y = a ∨ y ∈ xs
⊢ x ≤ y
Tactic:
rcases hy with (heq | hmem)
Proof state after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ y

case neg.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hmem : y ∈ xs
⊢ x ≤ y
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ y
Tactic:
rw [heq]
Proof state after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ a
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
heq : y = a
⊢ x ≤ a
Tactic:
rw [not_le] at h
Proof state after:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : x < a
y : α
heq : y = a
⊢ x ≤ a
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left.inl
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : x < a
y : α
heq : y = a
⊢ x ≤ a
Tactic:
exact le_of_lt h
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.left.inr
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hmem : y ∈ xs
⊢ x ≤ y
Tactic:
exact ordered.1 y hmem
Proof state after:
no goals
Theorem: ordered_insert_is_ordered
Proof state before:
case neg.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
⊢ List.Pairwise LE.le (insert' a xs)
Tactic:
exact ih ordered.2
Proof state after:
no goals
Theorem: equiv_if_evens
Proof state before:
x y : ℤ
⊢ Even x → Even y → equiv_rel x y
Tactic:
intros ex ey
Proof state after:
x y : ℤ
ex : Even x
ey : Even y
⊢ equiv_rel x y
Theorem: equiv_if_evens
Proof state before:
x y : ℤ
ex : Even x
ey : Even y
⊢ equiv_rel x y
Tactic:
simp [equiv_rel, Even] at *
Proof state after:
x y : ℤ
ex : ∃ r, x = r + r
ey : ∃ r, y = r + r
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_evens
Proof state before:
x y : ℤ
ex : ∃ r, x = r + r
ey : ∃ r, y = r + r
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ex with ⟨a, ha⟩
Proof state after:
case intro
x y : ℤ
ey : ∃ r, y = r + r
a : ℤ
ha : x = a + a
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_evens
Proof state before:
case intro
x y : ℤ
ey : ∃ r, y = r + r
a : ℤ
ha : x = a + a
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ey with ⟨b, hb⟩
Proof state after:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_evens
Proof state before:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rw [ha, hb]
Proof state after:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r
Theorem: equiv_if_evens
Proof state before:
case intro.intro
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ ∃ r, (a + a) ^ 2 + (b + b) ^ 2 = r + r
Tactic:
use (2 * a ^ 2 + 2 * b ^ 2)
Proof state after:
case h
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ (a + a) ^ 2 + (b + b) ^ 2 = 2 * a ^ 2 + 2 * b ^ 2 + (2 * a ^ 2 + 2 * b ^ 2)
Theorem: equiv_if_evens
Proof state before:
case h
x y a : ℤ
ha : x = a + a
b : ℤ
hb : y = b + b
⊢ (a + a) ^ 2 + (b + b) ^ 2 = 2 * a ^ 2 + 2 * b ^ 2 + (2 * a ^ 2 + 2 * b ^ 2)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: equiv_if_odds
Proof state before:
x y : ℤ
⊢ Odd x → Odd y → equiv_rel x y
Tactic:
intros ex ey
Proof state after:
x y : ℤ
ex : Odd x
ey : Odd y
⊢ equiv_rel x y
Theorem: equiv_if_odds
Proof state before:
x y : ℤ
ex : Odd x
ey : Odd y
⊢ equiv_rel x y
Tactic:
simp [equiv_rel, Odd, Even] at *
Proof state after:
x y : ℤ
ex : ∃ k, x = 2 * k + 1
ey : ∃ k, y = 2 * k + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_odds
Proof state before:
x y : ℤ
ex : ∃ k, x = 2 * k + 1
ey : ∃ k, y = 2 * k + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ex with ⟨a, ha⟩
Proof state after:
case intro
x y : ℤ
ey : ∃ k, y = 2 * k + 1
a : ℤ
ha : x = 2 * a + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_odds
Proof state before:
case intro
x y : ℤ
ey : ∃ k, y = 2 * k + 1
a : ℤ
ha : x = 2 * a + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rcases ey with ⟨b, hb⟩
Proof state after:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Theorem: equiv_if_odds
Proof state before:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
Tactic:
rw [ha, hb]
Proof state after:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, (2 * a + 1) ^ 2 + (2 * b + 1) ^ 2 = r + r
Theorem: equiv_if_odds
Proof state before:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, (2 * a + 1) ^ 2 + (2 * b + 1) ^ 2 = r + r
Tactic:
ring_nf
Proof state after:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = r * 2
Theorem: equiv_if_odds
Proof state before:
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = r * 2
Tactic:
use (1 + 2 * a + 2 * a ^ 2 + 2 * b + 2 * b ^ 2)
Proof state after:
case h
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = (1 + 2 * a + 2 * a ^ 2 + 2 * b + 2 * b ^ 2) * 2
Theorem: equiv_if_odds
Proof state before:
case h
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ 2 + a * 4 + a ^ 2 * 4 + b * 4 + b ^ 2 * 4 = (1 + 2 * a + 2 * a ^ 2 + 2 * b + 2 * b ^ 2) * 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: nequiv_if_diff_parity
Proof state before:
x y : ℤ
⊢ Odd x → Even y → ¬equiv_rel x y
Tactic:
intros ex ey equiv
Proof state after:
x y : ℤ
ex : Odd x
ey : Even y
equiv : equiv_rel x y
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
x y : ℤ
ex : Odd x
ey : Even y
equiv : equiv_rel x y
⊢ False
Tactic:
simp [equiv_rel, Odd, Even] at *
Proof state after:
x y : ℤ
ex : ∃ k, x = 2 * k + 1
ey : ∃ r, y = r + r
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
x y : ℤ
ex : ∃ k, x = 2 * k + 1
ey : ∃ r, y = r + r
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
⊢ False
Tactic:
rcases ex with ⟨a, ha⟩
Proof state after:
case intro
x y : ℤ
ey : ∃ r, y = r + r
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
a : ℤ
ha : x = 2 * a + 1
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro
x y : ℤ
ey : ∃ r, y = r + r
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
a : ℤ
ha : x = 2 * a + 1
⊢ False
Tactic:
rcases ey with ⟨b, hb⟩
Proof state after:
case intro.intro
x y : ℤ
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro
x y : ℤ
equiv : ∃ r, x ^ 2 + y ^ 2 = r + r
a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
⊢ False
Tactic:
rcases equiv with ⟨e, he⟩
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : x ^ 2 + y ^ 2 = e + e
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : x ^ 2 + y ^ 2 = e + e
⊢ False
Tactic:
rw [ha, hb] at he
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : (2 * a + 1) ^ 2 + (b + b) ^ 2 = e + e
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : (2 * a + 1) ^ 2 + (b + b) ^ 2 = e + e
⊢ False
Tactic:
ring_nf at he
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = e * 2
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = e * 2
⊢ False
Tactic:
symm at he
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : e * 2 = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : e * 2 = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
rw [mul_comm] at he
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
have two_dvd := dvd_of_mul_right_eq e he
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ False
Tactic:
have hring :
  1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
  = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1 := by
  ring_nf
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Tactic:
rw [hring] at two_dvd
Proof state after:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Theorem: nequiv_if_diff_parity
Proof state before:
case intro.intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
hring : 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
⊢ False
Tactic:
exact Int.two_not_dvd_two_mul_add_one _ two_dvd
Proof state after:
no goals
Theorem: nequiv_if_diff_parity
Proof state before:
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = b + b
e : ℤ
he : 2 * e = 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
two_dvd : 2 ∣ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4
⊢ 1 + a * 4 + a ^ 2 * 4 + b ^ 2 * 4 = 2 * (2 * a + 2 * a ^ 2 + 2 * b ^ 2) + 1
Tactic:
ring_nf
Proof state after:
no goals
Theorem: nequiv_if_diff_parity'
Proof state before:
x y : ℤ
⊢ Even x → Odd y → ¬equiv_rel x y
Tactic:
intros ex ey equiv
Proof state after:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
⊢ False
Theorem: nequiv_if_diff_parity'
Proof state before:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
⊢ False
Tactic:
have nequiv := nequiv_if_diff_parity ey ex
Proof state after:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
nequiv : ¬equiv_rel y x
⊢ False
Theorem: nequiv_if_diff_parity'
Proof state before:
x y : ℤ
ex : Even x
ey : Odd y
equiv : equiv_rel x y
nequiv : ¬equiv_rel y x
⊢ False
Tactic:
exact nequiv (equiv_inst.symm equiv)
Proof state after:
no goals
Theorem: lin_rel_is_not_function
Proof state before:
⊢ ¬is_function lin_rel
Tactic:
intro is_fn
Proof state after:
is_fn : is_function lin_rel
⊢ False