internlm/Lean-Github huggingface dataset:
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
x y z : Nat
⊢ x < y - z ↔ x + z < y
Tactic:
induction y, z with
| zero_right y => rw [Nat.sub_zero, Nat.add_zero]
| zero_left z => rw [Nat.zero_sub]; constructor <;> (intro; contradiction)
| succ_succ y z H => rw [Nat.succ_sub_succ, Nat.add_succ, Nat.succ_eq, Nat.succ_lt_succ_iff]; exact H
Proof state after:
no goals
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case zero_right
x y : Nat
⊢ x < y - 0 ↔ x + 0 < y
Tactic:
rw [Nat.sub_zero, Nat.add_zero]
Proof state after:
no goals
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case zero_left
x z : Nat
⊢ x < 0 - z ↔ x + z < 0
Tactic:
rw [Nat.zero_sub]
Proof state after:
case zero_left
x z : Nat
⊢ x < 0 ↔ x + z < 0
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case zero_left
x z : Nat
⊢ x < 0 ↔ x + z < 0
Tactic:
constructor <;> (intro; contradiction)
Proof state after:
no goals
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case zero_left.mpr
x z : Nat
⊢ x + z < 0 → x < 0
Tactic:
intro
Proof state after:
case zero_left.mpr
x z : Nat
a✝ : x + z < 0
⊢ x < 0
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case zero_left.mpr
x z : Nat
a✝ : x + z < 0
⊢ x < 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y + 1 - (z + 1) ↔ x + (z + 1) < y + 1
Tactic:
rw [Nat.succ_sub_succ, Nat.add_succ, Nat.succ_eq, Nat.succ_lt_succ_iff]
Proof state after:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y - z ↔ x + z < y
Theorem: Nat.lt_sub_iff_add_lt
Proof state before:
case succ_succ
x y z : Nat
H : x < y - z ↔ x + z < y
⊢ x < y - z ↔ x + z < y
Tactic:
exact H
Proof state after:
no goals
Theorem: Nat.sub_le_right
Proof state before:
x y : Nat
⊢ x - y ≤ x
Tactic:
rw [Nat.sub_le_iff_le_add]
Proof state after:
x y : Nat
⊢ x ≤ x + y
Theorem: Nat.sub_le_right
Proof state before:
x y : Nat
⊢ x ≤ x + y
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Nat.sub_lt_of_pos_of_pos_right
Proof state before:
x y : Nat
⊢ x > 0 → y > 0 → x - y < x
Tactic:
intro hx hy
Proof state after:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x - y < x
Theorem: Nat.sub_lt_of_pos_of_pos_right
Proof state before:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x - y < x
Tactic:
rw [Nat.sub_lt_iff_lt_add_of_pos]
Proof state after:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x < y + x

case hz
x y : Nat
hx : x > 0
hy : y > 0
⊢ x > 0
Theorem: Nat.sub_lt_of_pos_of_pos_right
Proof state before:
x y : Nat
hx : x > 0
hy : y > 0
⊢ x < y + x
Tactic:
exact Nat.lt_add_of_pos_left hy
Proof state after:
no goals
Theorem: Nat.sub_lt_of_pos_of_pos_right
Proof state before:
case hz
x y : Nat
hx : x > 0
hy : y > 0
⊢ x > 0
Tactic:
exact hx
Proof state after:
no goals
Theorem: Nat.sub_le_sub_of_le_of_ge
Proof state before:
x₁ x₂ y₁ y₂ : Nat
⊢ x₁ ≤ x₂ → y₁ ≥ y₂ → x₁ - y₁ ≤ x₂ - y₂
Tactic:
intro hx hy
Proof state after:
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₂
Theorem: Nat.sub_le_sub_of_le_of_ge
Proof state before:
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₂
Tactic:
transitivity (x₂ - y₁)
Proof state after:
case left
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₁

case right
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₂ - y₁ ≤ x₂ - y₂
Theorem: Nat.sub_le_sub_of_le_of_ge
Proof state before:
case left
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₁
Tactic:
exact Nat.sub_le_sub_right hx _
Proof state after:
no goals
Theorem: Nat.sub_le_sub_of_le_of_ge
Proof state before:
case right
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₂ - y₁ ≤ x₂ - y₂
Tactic:
exact Nat.sub_le_sub_left hy _
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
x y z : Nat
⊢ x < y → z < y → x - z < y - z
Tactic:
intro hx hz
Proof state after:
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z < y - z
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z < y - z
Tactic:
apply Nat.lt_sub_of_add_lt
Proof state after:
case h
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z + z < y
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
case h
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z + z < y
Tactic:
cases Nat.le_total x z with
| inl h => rw [Nat.sub_eq_zero_of_le h, Nat.zero_add]; exact hz
| inr h => rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]; exact hx
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ x - z + z < y
Tactic:
rw [Nat.sub_eq_zero_of_le h, Nat.zero_add]
Proof state after:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ z < y
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ z < y
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x - z + z < y
Tactic:
rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]
Proof state after:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x < y
Theorem: Nat.sub_lt_sub_of_lt_left
Proof state before:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x < y
Tactic:
exact hx
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
x y z : Nat
hx : x > y
hz : y < z
⊢ z - x < z - y
Tactic:
apply Nat.sub_lt_of_pos_of_lt_add
Proof state after:
case hpos
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y > 0

case a
x y z : Nat
hx : x > y
hz : y < z
⊢ z < z - y + x
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case hpos
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y > 0
Tactic:
apply Nat.sub_pos_of_lt
Proof state after:
case hpos.h
x y z : Nat
hx : x > y
hz : y < z
⊢ y < z
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case hpos.h
x y z : Nat
hx : x > y
hz : y < z
⊢ y < z
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case a
x y z : Nat
hx : x > y
hz : y < z
⊢ z < z - y + x
Tactic:
transitivity (y + (z - y)) using LE.le, LT.lt
Proof state after:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ y + (z - y)

case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ y + (z - y) < z - y + x
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ y + (z - y)
Tactic:
rw [Nat.add_sub_comm]
Proof state after:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ z + (y - z)
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case a.left
x y z : Nat
hx : x > y
hz : y < z
⊢ z ≤ z + (y - z)
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ y + (z - y) < z - y + x
Tactic:
rw [Nat.add_comm]
Proof state after:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y + y < z - y + x
Theorem: Nat.sub_lt_sub_of_gt_of_lt_right
Proof state before:
case a.right
x y z : Nat
hx : x > y
hz : y < z
⊢ z - y + y < z - y + x
Tactic:
exact Nat.add_lt_add_left hx ..
Proof state after:
no goals
Theorem: HEq.eqRec_heq
Proof state before:
α : Sort u_1
a : α
β : (a' : α) → a = a' → Sort u_2
a' : α
h : a = a'
x : β a ⋯
⊢ h ▸ x ≅ x
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
a : α
β : (a' : α) → a = a' → Sort u_2
x : β a ⋯
⊢ ⋯ ▸ x ≅ x
Theorem: HEq.eqRec_heq
Proof state before:
case refl
α : Sort u_1
a : α
β : (a' : α) → a = a' → Sort u_2
x : β a ⋯
⊢ ⋯ ▸ x ≅ x
Tactic:
exact HEq.rfl
Proof state after:
no goals
Theorem: HEq.eqNdrec_heq
Proof state before:
α : Sort u_1
β : α → Sort u_2
a a' : α
h : a = a'
x : β a
⊢ h ▸ x ≅ x
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : α → Sort u_2
a : α
x : β a
⊢ ⋯ ▸ x ≅ x
Theorem: HEq.eqNdrec_heq
Proof state before:
case refl
α : Sort u_1
β : α → Sort u_2
a : α
x : β a
⊢ ⋯ ▸ x ≅ x
Tactic:
exact HEq.rfl
Proof state after:
no goals
Theorem: HEq.eqRec_heq_iff_heq
Proof state before:
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
a' : α
h : a = a'
x : β a ⋯
y : γ
⊢ h ▸ x ≅ y ↔ x ≅ y
Tactic:
cases h
Proof state after:
case refl
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
x : β a ⋯
y : γ
⊢ ⋯ ▸ x ≅ y ↔ x ≅ y
Theorem: HEq.eqRec_heq_iff_heq
Proof state before:
case refl
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
x : β a ⋯
y : γ
⊢ ⋯ ▸ x ≅ y ↔ x ≅ y
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: HEq.heq_eqRec_iff_heq
Proof state before:
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
a' : α
h : a = a'
x : β a ⋯
y : γ
⊢ y ≅ h ▸ x ↔ y ≅ x
Tactic:
cases h
Proof state after:
case refl
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
x : β a ⋯
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x
Theorem: HEq.heq_eqRec_iff_heq
Proof state before:
case refl
γ : Sort u_1
α : Sort u_2
a : α
β : (a' : α) → a = a' → Sort u_1
x : β a ⋯
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: HEq.eqNdrec_heq_iff_heq
Proof state before:
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a a' : α
h : a = a'
x : β a
y : γ
⊢ h ▸ x ≅ y ↔ x ≅ y
Tactic:
cases h
Proof state after:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ ⋯ ▸ x ≅ y ↔ x ≅ y
Theorem: HEq.eqNdrec_heq_iff_heq
Proof state before:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ ⋯ ▸ x ≅ y ↔ x ≅ y
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: HEq.heq_eqNdrec_iff_heq
Proof state before:
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a a' : α
h : a = a'
x : β a
y : γ
⊢ y ≅ h ▸ x ↔ y ≅ x
Tactic:
cases h
Proof state after:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x
Theorem: HEq.heq_eqNdrec_iff_heq
Proof state before:
case refl
γ : Sort u_1
α : Sort u_2
β : α → Sort u_1
a : α
x : β a
y : γ
⊢ y ≅ ⋯ ▸ x ↔ y ≅ x
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: HEq.cast_heq_iff_heq
Proof state before:
α β γ : Sort u_1
h : α = β
x : α
y : γ
⊢ cast h x ≅ y ↔ x ≅ y
Tactic:
cases h
Proof state after:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ cast ⋯ x ≅ y ↔ x ≅ y
Theorem: HEq.cast_heq_iff_heq
Proof state before:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ cast ⋯ x ≅ y ↔ x ≅ y
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: HEq.heq_cast_iff_heq
Proof state before:
α β γ : Sort u_1
h : α = β
x : α
y : γ
⊢ y ≅ cast h x ↔ y ≅ x
Tactic:
cases h
Proof state after:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ y ≅ cast ⋯ x ↔ y ≅ x
Theorem: HEq.heq_cast_iff_heq
Proof state before:
case refl
α γ : Sort u_1
x : α
y : γ
⊢ y ≅ cast ⋯ x ↔ y ≅ x
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Nat.tri_mono
Proof state before:
case zero_zero

⊢ 0 ≤ 0 → tri 0 ≤ tri 0
Tactic:
intro
Proof state after:
case zero_zero
a✝ : 0 ≤ 0
⊢ tri 0 ≤ tri 0
Theorem: Nat.tri_mono
Proof state before:
case zero_zero
a✝ : 0 ≤ 0
⊢ tri 0 ≤ tri 0
Tactic:
reflexivity
Proof state after:
no goals
Theorem: Nat.tri_mono
Proof state before:
case zero_succ
n : Nat
a✝ : 0 ≤ n → tri 0 ≤ n.tri
⊢ 0 ≤ n + 1 → tri 0 ≤ (n + 1).tri
Tactic:
intro
Proof state after:
case zero_succ
n : Nat
a✝¹ : 0 ≤ n → tri 0 ≤ n.tri
a✝ : 0 ≤ n + 1
⊢ tri 0 ≤ (n + 1).tri
Theorem: Nat.tri_mono
Proof state before:
case zero_succ
n : Nat
a✝¹ : 0 ≤ n → tri 0 ≤ n.tri
a✝ : 0 ≤ n + 1
⊢ tri 0 ≤ (n + 1).tri
Tactic:
exact Nat.zero_le ..
Proof state after:
no goals
Theorem: Nat.tri_mono
Proof state before:
case succ_zero
m : Nat
a✝ : m ≤ 0 → m.tri ≤ tri 0
⊢ m + 1 ≤ 0 → (m + 1).tri ≤ tri 0
Tactic:
intro
Proof state after:
case succ_zero
m : Nat
a✝¹ : m ≤ 0 → m.tri ≤ tri 0
a✝ : m + 1 ≤ 0
⊢ (m + 1).tri ≤ tri 0
Theorem: Nat.tri_mono
Proof state before:
case succ_zero
m : Nat
a✝¹ : m ≤ 0 → m.tri ≤ tri 0
a✝ : m + 1 ≤ 0
⊢ (m + 1).tri ≤ tri 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.tri_mono
Proof state before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
⊢ m + 1 ≤ n + 1 → (m + 1).tri ≤ (n + 1).tri
Tactic:
intro h
Proof state after:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ (m + 1).tri ≤ (n + 1).tri
Theorem: Nat.tri_mono
Proof state before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ (m + 1).tri ≤ (n + 1).tri
Tactic:
rw [tri_succ, tri_succ]
Proof state after:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m + 1 ≤ n.tri + n + 1
Theorem: Nat.tri_mono
Proof state before:
case succ_succ
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m + 1 ≤ n.tri + n + 1
Tactic:
apply Nat.add_le_add_right
Proof state after:
case succ_succ.h
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m ≤ n.tri + n
Theorem: Nat.tri_mono
Proof state before:
case succ_succ.h
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri + m ≤ n.tri + n
Tactic:
apply Nat.add_le_add
Proof state after:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri ≤ n.tri

case succ_succ.h.h₂
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Theorem: Nat.tri_mono
Proof state before:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m.tri ≤ n.tri
Tactic:
apply H
Proof state after:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Theorem: Nat.tri_mono
Proof state before:
case succ_succ.h.h₁
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Tactic:
exact Nat.le_of_succ_le_succ h
Proof state after:
no goals
Theorem: Nat.tri_mono
Proof state before:
case succ_succ.h.h₂
m n : Nat
H : m ≤ n → m.tri ≤ n.tri
h : m + 1 ≤ n + 1
⊢ m ≤ n
Tactic:
exact Nat.le_of_succ_le_succ h
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
⊢ 2 * n.tri = n * (n + 1)
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  calc
  _ = 2 * (tri n + (n + 1)) := by rfl
  _ = 2 * tri n + 2 * (n + 1) := by rw [Nat.mul_add]
  _ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
  _ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
  _ = (n + 1) * (n + 1 + 1) := by rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
case zero

⊢ 2 * tri 0 = 0 * (0 + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
case succ
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n + 1).tri = (n + 1) * (n + 1 + 1)
Tactic:
calc
_ = 2 * (tri n + (n + 1)) := by rfl
_ = 2 * tri n + 2 * (n + 1) := by rw [Nat.mul_add]
_ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
_ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
_ = (n + 1) * (n + 1 + 1) := by rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n + 1).tri = 2 * (n.tri + (n + 1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n.tri + (n + 1)) = 2 * n.tri + 2 * (n + 1)
Tactic:
rw [Nat.mul_add]
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * n.tri + 2 * (n + 1) = n * (n + 1) + 2 * (n + 1)
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ n * (n + 1) + 2 * (n + 1) = (n + 2) * (n + 1)
Tactic:
rw [Nat.add_mul]
Proof state after:
no goals
Theorem: Nat.two_tri_eq
Proof state before:
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ (n + 2) * (n + 1) = (n + 1) * (n + 1 + 1)
Tactic:
rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: Nat.tri_add_self_lt_tri_of_lt
Proof state before:
m n : Nat
⊢ m < n → m.tri + m < n.tri
Tactic:
intro h
Proof state after:
m n : Nat
h : m < n
⊢ m.tri + m < n.tri
Theorem: Nat.tri_add_self_lt_tri_of_lt
Proof state before:
m n : Nat
h : m < n
⊢ m.tri + m < n.tri
Tactic:
transitivity (tri (m+1)) using LT.lt, LE.le
Proof state after:
case left
m n : Nat
h : m < n
⊢ m.tri + m < (m + 1).tri

case right
m n : Nat
h : m < n
⊢ (m + 1).tri ≤ n.tri
Theorem: Nat.tri_add_self_lt_tri_of_lt
Proof state before:
case left
m n : Nat
h : m < n
⊢ m.tri + m < (m + 1).tri
Tactic:
exact Nat.lt_succ_self ..
Proof state after:
no goals
Theorem: Nat.tri_add_self_lt_tri_of_lt
Proof state before:
case right
m n : Nat
h : m < n
⊢ (m + 1).tri ≤ n.tri
Tactic:
apply Nat.tri_mono
Proof state after:
case right.a
m n : Nat
h : m < n
⊢ m + 1 ≤ n
Theorem: Nat.tri_add_self_lt_tri_of_lt
Proof state before:
case right.a
m n : Nat
h : m < n
⊢ m + 1 ≤ n
Tactic:
exact Nat.succ_le_of_lt h
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
⊢ m₁ ≤ n₁ → m₂ ≤ n₂ → n₁.tri + m₁ = n₂.tri + m₂ → n₁ = n₂
Tactic:
intro h₁ h₂ h
Proof state after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
⊢ n₁ = n₂
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ = n₂
Tactic:
antisymmetry using LE.le
Proof state after:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ ≤ n₂

case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₂ ≤ n₁
Theorem: Nat.tri_add_inj
Proof state before:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₁ ≤ n₂
Tactic:
exact hle
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
case a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hle : n₁ ≤ n₂
hge : n₁ ≥ n₂
⊢ n₂ ≤ n₁
Tactic:
exact hge
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ = n₂
Tactic:
absurd h
Proof state after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Tactic:
apply Nat.ne_of_lt
Proof state after:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ < n₂.tri + m₂
Theorem: Nat.tri_add_inj
Proof state before:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ < n₂.tri + m₂
Tactic:
transitivity (tri n₁ + n₁) using LE.le, LT.lt
Proof state after:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ ≤ n₁.tri + n₁

case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri + m₂
Theorem: Nat.tri_add_inj
Proof state before:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + m₁ ≤ n₁.tri + n₁
Tactic:
apply Nat.add_le_add_left
Proof state after:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ m₁ ≤ n₁
Theorem: Nat.tri_add_inj
Proof state before:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ m₁ ≤ n₁
Tactic:
exact h₁
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri + m₂
Tactic:
transitivity (tri n₂) using LT.lt, LE.le
Proof state after:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri

case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₂.tri ≤ n₂.tri + m₂
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁.tri + n₁ < n₂.tri
Tactic:
apply Nat.tri_add_self_lt_tri_of_lt
Proof state after:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ < n₂
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₁ < n₂
Tactic:
exact Nat.lt_of_not_ge hlt
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
x✝ : Decidable (n₁ ≤ n₂)
hlt : ¬n₁ ≥ n₂
⊢ n₂.tri ≤ n₂.tri + m₂
Tactic:
exact Nat.le_add_right ..
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁ = n₂
Tactic:
absurd h
Proof state after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ ¬n₁.tri + m₁ = n₂.tri + m₂
Tactic:
symmetry using (.≠.)
Proof state after:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≠ n₁.tri + m₁
Theorem: Nat.tri_add_inj
Proof state before:
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≠ n₁.tri + m₁
Tactic:
apply Nat.ne_of_lt
Proof state after:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ < n₁.tri + m₁
Theorem: Nat.tri_add_inj
Proof state before:
case h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ < n₁.tri + m₁
Tactic:
transitivity (tri n₂ + n₂) using LE.le, LT.lt
Proof state after:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≤ n₂.tri + n₂

case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri + m₁
Theorem: Nat.tri_add_inj
Proof state before:
case h.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + m₂ ≤ n₂.tri + n₂
Tactic:
apply Nat.add_le_add_left
Proof state after:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ m₂ ≤ n₂
Theorem: Nat.tri_add_inj
Proof state before:
case h.left.h
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ m₂ ≤ n₂
Tactic:
exact h₂
Proof state after:
no goals
Theorem: Nat.tri_add_inj
Proof state before:
case h.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri + m₁
Tactic:
transitivity (tri n₁) using LT.lt, LE.le
Proof state after:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri

case h.right.right
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₁.tri ≤ n₁.tri + m₁
Theorem: Nat.tri_add_inj
Proof state before:
case h.right.left
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂.tri + n₂ < n₁.tri
Tactic:
apply Nat.tri_add_self_lt_tri_of_lt
Proof state after:
case h.right.left.a
m₁ n₁ m₂ n₂ : Nat
h₁ : m₁ ≤ n₁
h₂ : m₂ ≤ n₂
h : n₁.tri + m₁ = n₂.tri + m₂
hgt : ¬n₁ ≤ n₂
x✝ : Decidable (n₁ ≥ n₂)
⊢ n₂ < n₁