internlm/Lean-Github huggingface dataset:
Theorem: Nat.zero_pow_of_nonzero
Proof state before:
case zero
a✝ : 0 ≠ 0
⊢ 0 ^ 0 = 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.zero_pow_of_nonzero
Proof state before:
case succ
x : Nat
⊢ x + 1 ≠ 0 → 0 ^ (x + 1) = 0
Tactic:
intro
Proof state after:
case succ
x : Nat
a✝ : x + 1 ≠ 0
⊢ 0 ^ (x + 1) = 0
Theorem: Nat.zero_pow_of_nonzero
Proof state before:
case succ
x : Nat
a✝ : x + 1 ≠ 0
⊢ 0 ^ (x + 1) = 0
Tactic:
rw [Nat.zero_pow_succ]
Proof state after:
no goals
Theorem: Nat.pow_assoc
Proof state before:
x y z : Nat
⊢ (x ^ y) ^ z = x ^ (y * z)
Tactic:
induction z with
| zero => rw [Nat.pow_zero, Nat.mul_zero, Nat.pow_zero]
| succ z H => rw [Nat.pow_succ, Nat.mul_succ, Nat.pow_add, H]
Proof state after:
no goals
Theorem: Nat.pow_assoc
Proof state before:
case zero
x y : Nat
⊢ (x ^ y) ^ 0 = x ^ (y * 0)
Tactic:
rw [Nat.pow_zero, Nat.mul_zero, Nat.pow_zero]
Proof state after:
no goals
Theorem: Nat.pow_assoc
Proof state before:
case succ
x y z : Nat
H : (x ^ y) ^ z = x ^ (y * z)
⊢ (x ^ y) ^ (z + 1) = x ^ (y * (z + 1))
Tactic:
rw [Nat.pow_succ, Nat.mul_succ, Nat.pow_add, H]
Proof state after:
no goals
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case zero_right
x : Nat
⊢ 0 > 0 → x ≤ x ^ 0
Tactic:
intro
Proof state after:
case zero_right
x : Nat
a✝ : 0 > 0
⊢ x ≤ x ^ 0
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case zero_right
x : Nat
a✝ : 0 > 0
⊢ x ≤ x ^ 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case zero_left
y : Nat
⊢ y > 0 → 0 ≤ 0 ^ y
Tactic:
intro
Proof state after:
case zero_left
y : Nat
a✝ : y > 0
⊢ 0 ≤ 0 ^ y
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case zero_left
y : Nat
a✝ : y > 0
⊢ 0 ≤ 0 ^ y
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ
x y : Nat
a✝ : y > 0 → x ≤ x ^ y
⊢ y + 1 > 0 → x + 1 ≤ (x + 1) ^ (y + 1)
Tactic:
intro
Proof state after:
case succ_succ
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 ≤ (x + 1) ^ (y + 1)
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 ≤ (x + 1) ^ (y + 1)
Tactic:
transitivity (1 * (x + 1)) using Eq, LE.le
Proof state after:
case succ_succ.left
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 = 1 * (x + 1)

case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.left
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ x + 1 = 1 * (x + 1)
Tactic:
rw [Nat.one_mul]
Proof state after:
no goals
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ (y + 1)
Tactic:
rw [Nat.pow_succ]
Proof state after:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ y * (x + 1)
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.right
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 * (x + 1) ≤ (x + 1) ^ y * (x + 1)
Tactic:
apply Nat.mul_le_mul_right
Proof state after:
case succ_succ.right.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 ≤ (x + 1) ^ y
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.right.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 1 ≤ (x + 1) ^ y
Tactic:
apply Nat.succ_le_of_lt
Proof state after:
case succ_succ.right.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < (x + 1) ^ y
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.right.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < (x + 1) ^ y
Tactic:
apply Nat.pos_pow_of_pos
Proof state after:
case succ_succ.right.h.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < x + 1
Theorem: Nat.le_pow_right_of_pos
Proof state before:
case succ_succ.right.h.h.h
x y : Nat
a✝¹ : y > 0 → x ≤ x ^ y
a✝ : y + 1 > 0
⊢ 0 < x + 1
Tactic:
apply Nat.zero_lt_succ
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_right
z x : Nat
h : x < 0
⊢ z > 1 → z ^ x < z ^ 0
Tactic:
intro
Proof state after:
case zero_right
z x : Nat
h : x < 0
a✝ : z > 1
⊢ z ^ x < z ^ 0
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_right
z x : Nat
h : x < 0
a✝ : z > 1
⊢ z ^ x < z ^ 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_left
z y : Nat
h : 0 < y
⊢ z > 1 → z ^ 0 < z ^ y
Tactic:
intro hz
Proof state after:
case zero_left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z ^ y
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z ^ y
Tactic:
transitivity z using LT.lt, LE.le
Proof state after:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z

case zero_left.right
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ≤ z ^ y
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ^ 0 < z
Tactic:
rw [Nat.pow_zero]
Proof state after:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ 1 < z
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_left.left
z y : Nat
h : 0 < y
hz : z > 1
⊢ 1 < z
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case zero_left.right
z y : Nat
h : 0 < y
hz : z > 1
⊢ z ≤ z ^ y
Tactic:
exact Nat.le_pow_right _ _
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
⊢ z > 1 → z ^ (x + 1) < z ^ (y + 1)
Tactic:
intro hz
Proof state after:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ (x + 1) < z ^ (y + 1)
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ (x + 1) < z ^ (y + 1)
Tactic:
rw [Nat.pow_succ, Nat.pow_succ]
Proof state after:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x * z < z ^ y * z
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x * z < z ^ y * z
Tactic:
apply Nat.mul_lt_mul_of_pos_right
Proof state after:
case succ_succ.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x < z ^ y

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z ^ x < z ^ y

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Tactic:
apply H
Proof state after:
case succ_succ.h.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ x < y

case succ_succ.h.a
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 1

case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.h.h
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ x < y
Tactic:
exact Nat.lt_of_succ_lt_succ h
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.h.a
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 1
Tactic:
exact hz
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.hk
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ z > 0
Tactic:
transitivity 1 using LT.lt
Proof state after:
case succ_succ.hk.left
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 0 < 1

case succ_succ.hk.right
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 1 < z
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.hk.left
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 0 < 1
Tactic:
exact Nat.zero_lt_one
Proof state after:
no goals
Theorem: Nat.pow_lt_pow_of_gt_one_left
Proof state before:
case succ_succ.hk.right
z x y : Nat
H : x < y → z > 1 → z ^ x < z ^ y
h : x + 1 < y + 1
hz : z > 1
⊢ 1 < z
Tactic:
exact hz
Proof state after:
no goals
Theorem: ListN.append_nil
Proof state before:
α : Type u_1
n : Nat
xs : ListN α n
⊢ xs.append nil ≅ xs
Tactic:
cases xs
Proof state after:
case mk
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ { toList := toList✝, length_eq := length_eq✝ }.append nil ≅ { toList := toList✝, length_eq := length_eq✝ }
Theorem: ListN.append_nil
Proof state before:
case mk
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ { toList := toList✝, length_eq := length_eq✝ }.append nil ≅ { toList := toList✝, length_eq := length_eq✝ }
Tactic:
apply ListN.heq
Proof state after:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ α = α

case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ 0 + n = n

case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ ({ toList := toList✝, length_eq := length_eq✝ }.append nil).toList ≅
    { toList := toList✝, length_eq := length_eq✝ }.toList
Theorem: ListN.append_nil
Proof state before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ α = α
Tactic:
rfl
Proof state after:
no goals
Theorem: ListN.append_nil
Proof state before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ 0 + n = n
Tactic:
rw [Nat.zero_add]
Proof state after:
no goals
Theorem: ListN.append_nil
Proof state before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ ({ toList := toList✝, length_eq := length_eq✝ }.append nil).toList ≅
    { toList := toList✝, length_eq := length_eq✝ }.toList
Tactic:
simp only [ListN.append]
Proof state after:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ toList✝ ++ [] ≅ toList✝
Theorem: ListN.append_nil
Proof state before:
case mk.a
α : Type u_1
n : Nat
toList✝ : List α
length_eq✝ : toList✝.length = n
⊢ toList✝ ++ [] ≅ toList✝
Tactic:
rw [List.append_nil]
Proof state after:
no goals
Theorem: Finite.get_find
Proof state before:
α : Type u_1
inst : Finite α
x : α
⊢ Finite.get α (find x) = x
Tactic:
rw [←find_eq_iff_get_eq]
Proof state after:
no goals
Theorem: Finite.find_get
Proof state before:
α : Type u_1
inst : Finite α
i : Fin (Finite.size α)
⊢ find (Finite.get α i) = i
Tactic:
rw [find_eq_iff_get_eq]
Proof state after:
no goals
Theorem: Finite.forall_eq_true_of_all_eq_true
Proof state before:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.all p = true → ∀ (x : α), p x = true
Tactic:
intro h x
Proof state after:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
⊢ p x = true
Theorem: Finite.forall_eq_true_of_all_eq_true
Proof state before:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
⊢ p x = true
Tactic:
have hall := Fin.forall_eq_true_of_all_eq_true h
Proof state after:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
hall : ∀ (i : Fin toArray.size), p (Finite.get α i) = true
⊢ p x = true
Theorem: Finite.forall_eq_true_of_all_eq_true
Proof state before:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
hall : ∀ (i : Fin toArray.size), p (Finite.get α i) = true
⊢ p x = true
Tactic:
rw [←hall (Finite.find x)]
Proof state after:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
hall : ∀ (i : Fin toArray.size), p (Finite.get α i) = true
⊢ p x = p (Finite.get α (find x))
Theorem: Finite.forall_eq_true_of_all_eq_true
Proof state before:
α✝ : Type ?u.1375
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = true
x : α
hall : ∀ (i : Fin toArray.size), p (Finite.get α i) = true
⊢ p x = p (Finite.get α (find x))
Tactic:
rw [Finite.get_find]
Proof state after:
no goals
Theorem: Finite.exists_eq_false_of_all_eq_false
Proof state before:
α✝ : Type ?u.1482
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.all p = false → ∃ x, p x = false
Tactic:
intro h
Proof state after:
α✝ : Type ?u.1482
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = false
⊢ ∃ x, p x = false
Theorem: Finite.exists_eq_false_of_all_eq_false
Proof state before:
α✝ : Type ?u.1482
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.all p = false
⊢ ∃ x, p x = false
Tactic:
match Fin.exists_eq_false_of_all_eq_false h with
| ⟨i, h⟩ => exists (Finite.get α i)
Proof state after:
no goals
Theorem: Finite.exists_eq_false_of_all_eq_false
Proof state before:
α✝ : Type ?u.1482
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h✝ : Finite.all p = false
i : Fin toArray.size
h : p (Finite.get α i) = false
⊢ ∃ x, p x = false
Tactic:
exists (Finite.get α i)
Proof state after:
no goals
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∀ (x : α), p x) = Finite.all fun x => decide (p x)
Tactic:
match h : Finite.all fun x => decide (p x) with
| false =>
  apply decide_eq_false
  match exists_eq_false_of_all_eq_false h with
  | ⟨x, hx⟩ =>
    intro h
    rw [decide_eq_true (h x)] at hx
    contradiction
| true =>
  apply decide_eq_true
  intro x
  apply of_decide_eq_true
  apply forall_eq_true_of_all_eq_true h
Proof state after:
no goals
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ decide (∀ (x : α), p x) = false
Tactic:
apply decide_eq_false
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ ¬∀ (x : α), p x
Theorem: Finite.decide_forall
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ ¬∀ (x : α), p x
Tactic:
match exists_eq_false_of_all_eq_false h with
| ⟨x, hx⟩ =>
  intro h
  rw [decide_eq_true (h x)] at hx
  contradiction
Proof state after:
no goals
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
⊢ ¬∀ (x : α), p x
Tactic:
intro h
Proof state after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
h : ∀ (x : α), p x
⊢ False
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : decide (p x) = false
h : ∀ (x : α), p x
⊢ False
Tactic:
rw [decide_eq_true (h x)] at hx
Proof state after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : true = false
h : ∀ (x : α), p x
⊢ False
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h✝ : (Finite.all fun x => decide (p x)) = false
x : α
hx : true = false
h : ∀ (x : α), p x
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Finite.decide_forall
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ decide (∀ (x : α), p x) = true
Tactic:
apply decide_eq_true
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ ∀ (x : α), p x
Theorem: Finite.decide_forall
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ ∀ (x : α), p x
Tactic:
intro x
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ p x
Theorem: Finite.decide_forall
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ p x
Tactic:
apply of_decide_eq_true
Proof state after:
case a.a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ decide (p x) = true
Theorem: Finite.decide_forall
Proof state before:
case a.a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
x : α
⊢ decide (p x) = true
Tactic:
apply forall_eq_true_of_all_eq_true h
Proof state after:
no goals
Theorem: Finite.exists_eq_true_of_any_eq_true
Proof state before:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.any p = true → ∃ x, p x = true
Tactic:
intro h
Proof state after:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = true
⊢ ∃ x, p x = true
Theorem: Finite.exists_eq_true_of_any_eq_true
Proof state before:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = true
⊢ ∃ x, p x = true
Tactic:
match Fin.exists_eq_true_of_any_eq_true h with
| ⟨i, h⟩ => exists (Finite.get α i)
Proof state after:
no goals
Theorem: Finite.exists_eq_true_of_any_eq_true
Proof state before:
α✝ : Type ?u.2597
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h✝ : Finite.any p = true
i : Fin toArray.size
h : p (Finite.get α i) = true
⊢ ∃ x, p x = true
Tactic:
exists (Finite.get α i)
Proof state after:
no goals
Theorem: Finite.forall_eq_false_of_any_eq_false
Proof state before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
⊢ Finite.any p = false → ∀ (x : α), p x = false
Tactic:
intro h x
Proof state after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
⊢ p x = false
Theorem: Finite.forall_eq_false_of_any_eq_false
Proof state before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
⊢ p x = false
Tactic:
have hany := Fin.forall_eq_false_of_any_eq_false h
Proof state after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = false
Theorem: Finite.forall_eq_false_of_any_eq_false
Proof state before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = false
Tactic:
rw [←hany (Finite.find x)]
Proof state after:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = p (Finite.get α (find x))
Theorem: Finite.forall_eq_false_of_any_eq_false
Proof state before:
α✝ : Type ?u.2776
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h : Finite.any p = false
x : α
hany : ∀ (i : Fin toArray.size), p (Finite.get α i) = false
⊢ p x = p (Finite.get α (find x))
Tactic:
rw [Finite.get_find]
Proof state after:
no goals
Theorem: Finite.decide_exists
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
⊢ decide (∃ x, p x) = Finite.any fun x => decide (p x)
Tactic:
match h : Finite.any fun x => decide (p x) with
| true =>
  apply decide_eq_true
  match exists_eq_true_of_any_eq_true h with
  | ⟨x, hx⟩ =>
    exists x
    exact of_decide_eq_true hx
| false =>
  apply decide_eq_false
  intro ⟨x, hx⟩
  absurd forall_eq_false_of_any_eq_false h x
  rw [decide_eq_true hx]
  trivial
Proof state after:
no goals
Theorem: Finite.decide_exists
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
⊢ decide (∃ x, p x) = true
Tactic:
apply decide_eq_true
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
⊢ ∃ x, p x
Theorem: Finite.decide_exists
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
⊢ ∃ x, p x
Tactic:
match exists_eq_true_of_any_eq_true h with
| ⟨x, hx⟩ =>
  exists x
  exact of_decide_eq_true hx
Proof state after:
no goals
Theorem: Finite.decide_exists
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ ∃ x, p x
Tactic:
exists x
Proof state after:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ p x
Theorem: Finite.decide_exists
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = true
x : α
hx : decide (p x) = true
⊢ p x
Tactic:
exact of_decide_eq_true hx
Proof state after:
no goals
Theorem: Finite.decide_exists
Proof state before:
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
⊢ decide (∃ x, p x) = false
Tactic:
apply decide_eq_false
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
⊢ ¬∃ x, p x
Theorem: Finite.decide_exists
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
⊢ ¬∃ x, p x
Tactic:
intro ⟨x, hx⟩
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ False
Theorem: Finite.decide_exists
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ False
Tactic:
absurd forall_eq_false_of_any_eq_false h x
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬decide (p x) = false
Theorem: Finite.decide_exists
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬decide (p x) = false
Tactic:
rw [decide_eq_true hx]
Proof state after:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬true = false
Theorem: Finite.decide_exists
Proof state before:
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬true = false
Tactic:
trivial
Proof state after:
no goals
Theorem: Array.get_set_of_eq
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
⊢ ↑i = j → (as.set i x)[j] = x
Tactic:
intro h
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
⊢ (as.set i x)[j] = x
Theorem: Array.get_set_of_eq
Proof state before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
⊢ (as.set i x)[j] = x
Tactic:
have hj' : j < as.size := as.size_set i x ▸ hj
Proof state after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i = j
hj' : j < as.size
⊢ (as.set i x)[j] = x