internlm/Lean-Github huggingface dataset:
Theorem: Nat.bit0_xor_bit0
Proof state before:
x y : Nat
h✝ : x = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def]
Proof state after:
no goals
Theorem: Nat.bit0_xor_bit0
Proof state before:
x y : Nat
h✝ : ¬x = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
if y = 0 then
simp [*, xor_def]
else
simp [*, xor_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_xor_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : y = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def]
Proof state after:
no goals
Theorem: Nat.bit0_xor_bit0
Proof state before:
x y : Nat
h✝¹ : ¬x = 0
h✝ : ¬y = 0
⊢ 2 * x ^^^ 2 * y = 2 * (x ^^^ y)
Tactic:
simp [*, xor_def, bit0_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit0_xor_bit1
Proof state before:
x y : Nat
⊢ 2 * x ^^^ 2 * y + 1 = 2 * (x ^^^ y) + 1
Tactic:
simp [xor_def, bit0_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.bit1_xor_bit0
Proof state before:
x y : Nat
⊢ 2 * x + 1 ^^^ 2 * y = 2 * (x ^^^ y) + 1
Tactic:
simp [xor_def, bit1_bitwise_bit0]
Proof state after:
no goals
Theorem: Nat.bit1_xor_bit1
Proof state before:
x y : Nat
⊢ 2 * x + 1 ^^^ 2 * y + 1 = 2 * (x ^^^ y)
Tactic:
simp [xor_def, bit1_bitwise_bit1]
Proof state after:
no goals
Theorem: Nat.zero_xor
Proof state before:
x : Nat
⊢ 0 ^^^ x = x
Tactic:
simp [xor_def]
Proof state after:
no goals
Theorem: Nat.xor_zero
Proof state before:
x : Nat
⊢ x ^^^ 0 = x
Tactic:
simp [xor_def]
Proof state after:
no goals
Theorem: Nat.xor_self
Proof state before:
x : Nat
⊢ x ^^^ x = 0
Tactic:
induction x using Nat.recBit <;> simp [*]
Proof state after:
no goals
Theorem: Nat.xor_comm
Proof state before:
x y : Nat
⊢ x ^^^ y = y ^^^ x
Tactic:
induction x using Nat.recBit generalizing y <;> cases y using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.xor_assoc
Proof state before:
x y z : Nat
⊢ x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_xor_distrib_left
Proof state before:
x y z : Nat
⊢ x &&& (y ^^^ z) = x &&& y ^^^ x &&& z
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Nat.and_xor_distrib_right
Proof state before:
x y z : Nat
⊢ (x ^^^ y) &&& z = x &&& z ^^^ y &&& z
Tactic:
induction x using Nat.recBit generalizing y z <;>
  cases y using Nat.casesBitOn <;> cases z using Nat.casesBitOn <;> simp [*]
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isSome = true ↔ ∃ x, p x = true
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isSome = true → ∃ x, p x = true

case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∃ x, p x = true) → (find? p).isSome = true
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isSome = true → ∃ x, p x = true
Tactic:
match hp : find? p with
| some x =>
  intro
  exists x
  exact find?_eq_some hp
| none =>
  intro
  contradiction
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
⊢ (some x).isSome = true → ∃ x, p x = true
Tactic:
intro
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ ∃ x, p x = true
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ ∃ x, p x = true
Tactic:
exists x
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ p x = true
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isSome = true
⊢ p x = true
Tactic:
exact find?_eq_some hp
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
⊢ none.isSome = true → ∃ x, p x = true
Tactic:
intro
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isSome = true
⊢ ∃ x, p x = true
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isSome = true
⊢ ∃ x, p x = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∃ x, p x = true) → (find? p).isSome = true
Tactic:
intro
| ⟨x, hx⟩ =>
  match hp : find? p with
  | some _ =>
    rfl
  | none =>
    rw [find?_eq_none hp] at hx
    contradiction
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
⊢ (find? p).isSome = true
Tactic:
match hp : find? p with
| some _ =>
  rfl
| none =>
  rw [find?_eq_none hp] at hx
  contradiction
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
val✝ : α
hp : find? p = some val✝
⊢ (some val✝).isSome = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : p x = true
hp : find? p = none
⊢ none.isSome = true
Tactic:
rw [find?_eq_none hp] at hx
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : false = true
hp : find? p = none
⊢ none.isSome = true
Theorem: Find.find_is_some_iff_exists_true
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x✝ : ∃ x, p x = true
x : α
hx : false = true
hp : find? p = none
⊢ none.isSome = true
Tactic:
contradiction
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true ↔ ∀ (x : α), p x = false
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true → ∀ (x : α), p x = false

case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∀ (x : α), p x = false) → (find? p).isNone = true
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
case mp
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (find? p).isNone = true → ∀ (x : α), p x = false
Tactic:
match hp : find? p with
| some x =>
  intro _
  contradiction
| none =>
  intro _ x
  exact find?_eq_none hp
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
⊢ (some x).isNone = true → ∀ (x : α), p x = false
Tactic:
intro _
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isNone = true
⊢ ∀ (x : α), p x = false
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
x : α
hp : find? p = some x
a✝ : (some x).isNone = true
⊢ ∀ (x : α), p x = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
⊢ none.isNone = true → ∀ (x : α), p x = false
Tactic:
intro _ x
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isNone = true
x : α
⊢ p x = false
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
hp : find? p = none
a✝ : none.isNone = true
x : α
⊢ p x = false
Tactic:
exact find?_eq_none hp
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
⊢ (∀ (x : α), p x = false) → (find? p).isNone = true
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
⊢ (find? p).isNone = true
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
case mpr
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
⊢ (find? p).isNone = true
Tactic:
match hp : find? p with
| some x =>
  absurd find?_eq_some hp
  rw [h]
  intro
  contradiction
| none =>
  rfl
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ (some x).isNone = true
Tactic:
absurd find?_eq_some hp
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬p x = true
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬p x = true
Tactic:
rw [h]
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬false = true
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
⊢ ¬false = true
Tactic:
intro
Proof state after:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
a✝ : false = true
⊢ False
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
x : α
hp : find? p = some x
a✝ : false = true
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Find.find_is_none_iff_forall_false
Proof state before:
α : Type u_1
inst✝ : Find α
p : α → Bool
h : ∀ (x : α), p x = false
hp : find? p = none
⊢ none.isNone = true
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
x y z : Nat
⊢ 0 < x → x * y ≤ x * z → y ≤ z
Tactic:
intro hx hxyz
Proof state after:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
⊢ y ≤ z
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
⊢ y ≤ z
Tactic:
if h : z < y then
  absurd hxyz
  apply Nat.not_le_of_gt
  exact Nat.mul_lt_mul_of_pos_left h hx
else
  exact Nat.le_of_not_gt h
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ y ≤ z
Tactic:
absurd hxyz
Proof state after:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ ¬x * y ≤ x * z
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ ¬x * y ≤ x * z
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ x * y > x * z
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
case h
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : z < y
⊢ x * y > x * z
Tactic:
exact Nat.mul_lt_mul_of_pos_left h hx
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_left
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : x * y ≤ x * z
h : ¬z < y
⊢ y ≤ z
Tactic:
exact Nat.le_of_not_gt h
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
x y z : Nat
⊢ 0 < x → y * x ≤ z * x → y ≤ z
Tactic:
intro hx hxyz
Proof state after:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
⊢ y ≤ z
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
⊢ y ≤ z
Tactic:
if h : z < y then
  absurd hxyz
  apply Nat.not_le_of_gt
  exact Nat.mul_lt_mul_of_pos_right h hx
else
  exact Nat.le_of_not_gt h
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : z < y
⊢ y ≤ z
Tactic:
absurd hxyz
Proof state after:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : z < y
⊢ ¬y * x ≤ z * x
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : z < y
⊢ ¬y * x ≤ z * x
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : z < y
⊢ y * x > z * x
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
case h
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : z < y
⊢ y * x > z * x
Tactic:
exact Nat.mul_lt_mul_of_pos_right h hx
Proof state after:
no goals
Theorem: Nat.le_of_mul_le_mul_of_pos_right
Proof state before:
x y z : Nat
hx : 0 < x
hxyz : y * x ≤ z * x
h : ¬z < y
⊢ y ≤ z
Tactic:
exact Nat.le_of_not_gt h
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_lt_left
Proof state before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
⊢ a ^ (n + 1) < b ^ (n + 1)
Tactic:
have hpos : 0 < b ^ n := Nat.pos_pow_of_pos n (Nat.zero_lt_of_lt h)
Proof state after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ (n + 1) < b ^ (n + 1)
Theorem: Nat.pow_lt_pow_of_lt_left
Proof state before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ (n + 1) < b ^ (n + 1)
Tactic:
simp [Nat.pow_succ]
Proof state after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n * a < b ^ n * b
Theorem: Nat.pow_lt_pow_of_lt_left
Proof state before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n * a < b ^ n * b
Tactic:
apply Nat.mul_lt_mul_of_le_of_lt _ h hpos
Proof state after:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n ≤ b ^ n
Theorem: Nat.pow_lt_pow_of_lt_left
Proof state before:
a b : Nat
h : a < b
n : Nat
x✝ : 0 < n + 1
hpos : 0 < b ^ n
⊢ a ^ n ≤ b ^ n
Tactic:
exact Nat.pow_le_pow_of_le_left (Nat.le_of_lt h) n
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
m n a : Nat
⊢ 1 < a → m < n → a ^ m < a ^ n
Tactic:
intro ha h
Proof state after:
m n a : Nat
ha : 1 < a
h : m < n
⊢ a ^ m < a ^ n
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
m n a : Nat
ha : 1 < a
h : m < n
⊢ a ^ m < a ^ n
Tactic:
induction m, n using Nat.recDiag with try contradiction
| zero_succ n =>
have hpos := Nat.pos_pow_of_pos n (Nat.le_of_lt ha)
apply Nat.lt_of_le_of_lt hpos
have : a ^ n * 1 < a ^ n * a := Nat.mul_lt_mul_of_pos_left ha hpos
rwa [Nat.mul_one] at this
| succ_succ m n ih =>
apply Nat.mul_lt_mul_of_pos_right _ (Nat.le_of_lt ha)
exact ih (Nat.lt_of_succ_lt_succ h)
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case succ_zero
a : Nat
ha : 1 < a
m✝ : Nat
a✝ : m✝ < 0 → a ^ m✝ < a ^ 0
h : m✝ + 1 < 0
⊢ a ^ (m✝ + 1) < a ^ 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
⊢ a ^ 0 < a ^ (n + 1)
Tactic:
have hpos := Nat.pos_pow_of_pos n (Nat.le_of_lt ha)
Proof state after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ 0 < a ^ (n + 1)
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ 0 < a ^ (n + 1)
Tactic:
apply Nat.lt_of_le_of_lt hpos
Proof state after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ n < a ^ (n + 1)
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
⊢ a ^ n < a ^ (n + 1)
Tactic:
have : a ^ n * 1 < a ^ n * a := Nat.mul_lt_mul_of_pos_left ha hpos
Proof state after:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
this : a ^ n * 1 < a ^ n * a
⊢ a ^ n < a ^ (n + 1)
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case zero_succ
a : Nat
ha : 1 < a
n : Nat
a✝ : 0 < n → a ^ 0 < a ^ n
h : 0 < n + 1
hpos : 0 < a ^ n
this : a ^ n * 1 < a ^ n * a
⊢ a ^ n < a ^ (n + 1)
Tactic:
rwa [Nat.mul_one] at this
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
case succ_succ
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a ^ (m + 1) < a ^ (n + 1)
Tactic:
apply Nat.mul_lt_mul_of_pos_right _ (Nat.le_of_lt ha)
Proof state after:
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a.pow m < a.pow n
Theorem: Nat.pow_lt_pow_of_lt_right
Proof state before:
a : Nat
ha : 1 < a
m n : Nat
ih : m < n → a ^ m < a ^ n
h : m + 1 < n + 1
⊢ a.pow m < a.pow n
Tactic:
exact ih (Nat.lt_of_succ_lt_succ h)
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case zero
x y : Nat
h : x < y
⊢ 0 > 0 → x ^ 0 < y ^ 0
Tactic:
intro
Proof state after:
case zero
x y : Nat
h : x < y
a✝ : 0 > 0
⊢ x ^ 0 < y ^ 0
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case zero
x y : Nat
h : x < y
a✝ : 0 > 0
⊢ x ^ 0 < y ^ 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ
x y : Nat
h : x < y
z : Nat
⊢ z + 1 > 0 → x ^ (z + 1) < y ^ (z + 1)
Tactic:
intro
Proof state after:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ (z + 1) < y ^ (z + 1)
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ (z + 1) < y ^ (z + 1)
Tactic:
rw [Nat.pow_succ, Nat.pow_succ]
Proof state after:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z * x < y ^ z * y
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z * x < y ^ z * y
Tactic:
apply Nat.mul_lt_mul_of_le_of_lt
Proof state after:
case succ.hac
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z ≤ y ^ z

case succ.hbd
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y

case succ.hc
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y ^ z
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hac
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ^ z ≤ y ^ z
Tactic:
apply Nat.pow_le_pow_left
Proof state after:
case succ.hac.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ≤ y
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hac.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x ≤ y
Tactic:
apply Nat.le_of_lt
Proof state after:
case succ.hac.h.a
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hac.h.a
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hbd
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ x < y
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hc
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y ^ z
Tactic:
apply Nat.pos_pow_of_pos
Proof state after:
case succ.hc.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hc.h
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 < y
Tactic:
apply Nat.lt_of_le_of_lt
Proof state after:
case succ.hc.h.h₁
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 ≤ ?succ.hc.h.m

case succ.hc.h.h₂
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ ?succ.hc.h.m < y

case succ.hc.h.m
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ Nat
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hc.h.h₁
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ 0 ≤ ?succ.hc.h.m
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_pos_right
Proof state before:
case succ.hc.h.h₂
x y : Nat
h : x < y
z : Nat
a✝ : z + 1 > 0
⊢ ?succ.hc.h.m < y
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
m n : Nat
h : m * 0 = 1
⊢ 0 = 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
m n : Nat
h : m * 1 = 1
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
m n n✝ : Nat
h : m * (n✝ + 2) = 1
⊢ n✝ + 2 = 1
Tactic:
cases m
Proof state after:
case zero
n n✝ : Nat
h : 0 * (n✝ + 2) = 1
⊢ n✝ + 2 = 1

case succ
n n✝¹ n✝ : Nat
h : (n✝ + 1) * (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
case zero
n n✝ : Nat
h : 0 * (n✝ + 2) = 1
⊢ n✝ + 2 = 1
Tactic:
rw [Nat.zero_mul] at h
Proof state after:
case zero
n n✝ : Nat
h : 0 = 1
⊢ n✝ + 2 = 1
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
case zero
n n✝ : Nat
h : 0 = 1
⊢ n✝ + 2 = 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
case succ
n n✝¹ n✝ : Nat
h : (n✝ + 1) * (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Tactic:
rw [Nat.succ_mul] at h
Proof state after:
case succ
n n✝¹ n✝ : Nat
h : n✝ * (n✝¹ + 2) + (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
case succ
n n✝¹ n✝ : Nat
h : n✝ * (n✝¹ + 2) + (n✝¹ + 2) = 1
⊢ n✝¹ + 2 = 1
Tactic:
injection h
Proof state after:
case succ
n n✝¹ n✝ : Nat
n_eq✝ : (n✝ * (n✝¹ + 2)).add (n✝¹ + 1) = 0
⊢ n✝¹ + 2 = 1
Theorem: Nat.eq_one_of_mul_eq_one_left
Proof state before:
case succ
n n✝¹ n✝ : Nat
n_eq✝ : (n✝ * (n✝¹ + 2)).add (n✝¹ + 1) = 0
⊢ n✝¹ + 2 = 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.eq_one_of_mul_eq_one_right
Proof state before:
m n : Nat
h : m * n = 1
⊢ m = 1
Tactic:
rw [Nat.mul_comm] at h
Proof state after:
m n : Nat
h : n * m = 1
⊢ m = 1
Theorem: Nat.eq_one_of_mul_eq_one_right
Proof state before:
m n : Nat
h : n * m = 1
⊢ m = 1
Tactic:
exact eq_one_of_mul_eq_one_left h
Proof state after:
no goals
Theorem: Nat.mul_eq_one
Proof state before:
m n : Nat
⊢ m * n = 1 ↔ m = 1 ∧ n = 1
Tactic:
constructor
Proof state after:
case mp
m n : Nat
⊢ m * n = 1 → m = 1 ∧ n = 1

case mpr
m n : Nat
⊢ m = 1 ∧ n = 1 → m * n = 1
Theorem: Nat.mul_eq_one
Proof state before:
case mp
m n : Nat
⊢ m * n = 1 → m = 1 ∧ n = 1
Tactic:
intro h
Proof state after:
case mp
m n : Nat
h : m * n = 1
⊢ m = 1 ∧ n = 1
Theorem: Nat.mul_eq_one
Proof state before:
case mp
m n : Nat
h : m * n = 1
⊢ m = 1 ∧ n = 1
Tactic:
rw [eq_one_of_mul_eq_one_right h, eq_one_of_mul_eq_one_left h]
Proof state after:
case mp
m n : Nat
h : m * n = 1
⊢ 1 = 1 ∧ 1 = 1
Theorem: Nat.mul_eq_one
Proof state before:
case mp
m n : Nat
h : m * n = 1
⊢ 1 = 1 ∧ 1 = 1
Tactic:
trivial
Proof state after:
no goals
Theorem: Nat.mul_eq_one
Proof state before:
case mpr
m n : Nat
⊢ m = 1 ∧ n = 1 → m * n = 1
Tactic:
intro ⟨hm, hn⟩
Proof state after:
case mpr
m n : Nat
hm : m = 1
hn : n = 1
⊢ m * n = 1
Theorem: Nat.mul_eq_one
Proof state before:
case mpr
m n : Nat
hm : m = 1
hn : n = 1
⊢ m * n = 1
Tactic:
rw [hm, hn]
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
case zero
m : Nat
⊢ m ^ 0 = 0 ↔ m = 0 ∧ 0 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.pow_eq_zero
Proof state before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ (n + 1) = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
rw [Nat.pow_succ]
Proof state after:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n * m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Theorem: Nat.pow_eq_zero
Proof state before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n * m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
rw [Nat.mul_eq_zero]
Proof state after:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Theorem: Nat.pow_eq_zero
Proof state before:
case succ
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 ↔ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
Proof state after:
case succ.mp
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m ^ n = 0 ∨ m = 0 → m = 0 ∧ n + 1 ≠ 0

case succ.mpr
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
⊢ m = 0 ∧ n + 1 ≠ 0 → m ^ n = 0 ∨ m = 0
Theorem: Nat.pow_eq_zero
Proof state before:
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0 ∧ n + 1 ≠ 0
Tactic:
constructor
Proof state after:
case left
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ m = 0

case right
m n : Nat
ih : m ^ n = 0 ↔ m = 0 ∧ n ≠ 0
x✝ : m ^ n = 0 ∨ m = 0
h : m ^ n = 0
⊢ n + 1 ≠ 0