internlm/Lean-Github huggingface dataset:
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h :
  (if h : i = n then none
    else
      let_fun hi := ⋯;
      if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
split at h
Proof state after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : i = n
h : none = none
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : i = n
h : none = none
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
next heq =>
  absurd hik
  rw [heq]
  apply Nat.not_le_of_gt
  exact k.isLt
Proof state after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
h✝ : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
next hne =>
  have hi : i < n := Nat.lt_of_le_of_ne hi hne
  simp only at h
  split at h
  next hp =>
    contradiction
  next hp =>
    by_cases i = k.val with
    | isTrue heq =>
      rw [Bool.eq_false_iff]
      intro hk
      apply hp
      rw [←hk]
      congr
    | isFalse hik' =>
      have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
      exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ p k = false
Tactic:
absurd hik
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬i ≤ ↑k
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬i ≤ ↑k
Tactic:
rw [heq]
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬n ≤ ↑k
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ ¬n ≤ ↑k
Tactic:
apply Nat.not_le_of_gt
Proof state after:
case h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ n > ↑k
Theorem: Fin.find?.loop_none
Proof state before:
case h
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
heq : i = n
h : none = none
⊢ n > ↑k
Tactic:
exact k.isLt
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
⊢ p k = false
Tactic:
have hi : i < n := Nat.lt_of_le_of_ne hi hne
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
hi : i < n
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h :
  (let_fun hi := ⋯;
    if p ⟨i, hi⟩ = true then some ⟨i, hi⟩ else loop p (i + 1) ⋯) =
    none
hi : i < n
⊢ p k = false
Tactic:
simp only at h
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = none
hi : i < n
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
h : (if p ⟨i, ⋯⟩ = true then some ⟨i, ⋯⟩ else loop p (i + 1) ⋯) = none
hi : i < n
⊢ p k = false
Tactic:
split at h
Proof state after:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
case isTrue
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false

case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
next hp =>
  contradiction
Proof state after:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
case isFalse
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
h✝ : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
next hp =>
  by_cases i = k.val with
  | isTrue heq =>
    rw [Bool.eq_false_iff]
    intro hk
    apply hp
    rw [←hk]
    congr
  | isFalse hik' =>
    have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
    exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : p ⟨i, ⋯⟩ = true
h : False
⊢ p k = false
Tactic:
contradiction
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
⊢ p k = false
Tactic:
by_cases i = k.val with
| isTrue heq =>
  rw [Bool.eq_false_iff]
  intro hk
  apply hp
  rw [←hk]
  congr
| isFalse hik' =>
  have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
  exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k = false
Tactic:
rw [Bool.eq_false_iff]
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k ≠ true
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
⊢ p k ≠ true
Tactic:
intro hk
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ False
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ False
Tactic:
apply hp
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = true
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = true
Tactic:
rw [←hk]
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = p k
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
heq : i = ↑k
hk : p k = true
⊢ p ⟨i, ⋯⟩ = p k
Tactic:
congr
Proof state after:
no goals
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
⊢ p k = false
Tactic:
have hik : i < k.val := Nat.lt_of_le_of_ne hik hik'
Proof state after:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik✝ : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
hik : i < ↑k
⊢ p k = false
Theorem: Fin.find?.loop_none
Proof state before:
n : Nat
p : Fin n → Bool
i : Nat
hi✝ : i ≤ n
k : Fin n
hik✝ : i ≤ ↑k
hne : ¬i = n
hi : i < n
hp : ¬p ⟨i, ⋯⟩ = true
h : loop p (i + 1) ⋯ = none
hik' : ¬i = ↑k
hik : i < ↑k
⊢ p k = false
Tactic:
exact loop_none (i+1) (Nat.succ_le_of_lt hi) k (Nat.succ_le_of_lt hik) h
Proof state after:
no goals
Theorem: Fin.sum_zero
Proof state before:
n : Nat
α : Type u_1
inst✝¹ : Add α
inst✝ : OfNat α 0
f : Fin 0 → α
⊢ sum f = 0
Tactic:
simp [sum]
Proof state after:
no goals
Theorem: Fin.sum_succ
Proof state before:
n : Nat
α : Type u_1
inst✝¹ : Add α
inst✝ : OfNat α 0
f : Fin (n + 1) → α
⊢ sum f = f 0 + sum (f ∘ succ)
Tactic:
simp [sum, foldr_succ]
Proof state after:
no goals
Theorem: Fin.prod_zero
Proof state before:
n : Nat
α : Type u_1
inst✝¹ : Mul α
inst✝ : OfNat α 1
f : Fin 0 → α
⊢ prod f = 1
Tactic:
simp [prod]
Proof state after:
no goals
Theorem: Fin.prod_succ
Proof state before:
n : Nat
α : Type u_1
inst✝¹ : Mul α
inst✝ : OfNat α 1
f : Fin (n + 1) → α
⊢ prod f = f 0 * prod (f ∘ succ)
Tactic:
simp [prod, foldr_succ]
Proof state after:
no goals
Theorem: Nat.mul_pred
Proof state before:
x y : Nat
⊢ x * (y - 1) = x * y - x
Tactic:
rw [Nat.mul_sub_left_distrib, Nat.mul_one]
Proof state after:
no goals
Theorem: Nat.pred_mul
Proof state before:
x y : Nat
⊢ (x - 1) * y = x * y - y
Tactic:
rw [Nat.mul_sub_right_distrib, Nat.one_mul]
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
x y : Nat
h : autoParam (x > 0) _auto✝
⊢ y > 1 → x < y * x
Tactic:
intro hy
Proof state after:
x y : Nat
h : autoParam (x > 0) _auto✝
hy : y > 1
⊢ x < y * x
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case zero
x : Nat
h : autoParam (x > 0) _auto✝
hy : 0 > 1
⊢ x < 0 * x
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < (y + 1) * x
Tactic:
rw [Nat.succ_mul]
Proof state after:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < y * x + x
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < y * x + x
Tactic:
apply Nat.lt_add_of_pos_left
Proof state after:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < y * x
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < y * x
Tactic:
apply Nat.mul_pos
Proof state after:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0

case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0
Tactic:
exact Nat.lt_of_succ_lt_succ hy
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_of_pos_left
Proof state before:
case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
x y : Nat
h : autoParam (x > 0) _auto✝
⊢ y > 1 → x < x * y
Tactic:
intro hy
Proof state after:
x y : Nat
h : autoParam (x > 0) _auto✝
hy : y > 1
⊢ x < x * y
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case zero
x : Nat
h : autoParam (x > 0) _auto✝
hy : 0 > 1
⊢ x < x * 0
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < x * (y + 1)
Tactic:
rw [Nat.mul_succ]
Proof state after:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < x * y + x
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case succ
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x < x * y + x
Tactic:
apply Nat.lt_add_of_pos_left
Proof state after:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < x * y
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case succ.a
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ 0 < x * y
Tactic:
apply Nat.mul_pos
Proof state after:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0

case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case succ.a.ha
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ x > 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Nat.lt_mul_of_gt_one_right
Proof state before:
case succ.a.hb
x : Nat
h : autoParam (x > 0) _auto✝
y : Nat
hy : y + 1 > 1
⊢ y > 0
Tactic:
exact Nat.lt_of_succ_lt_succ hy
Proof state after:
no goals
Theorem: Set.id_map
Proof state before:
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
⊢ Set.map id s = s
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
⊢ ∀ (x : α), x ∈ Set.map id s ↔ x ∈ s
Theorem: Set.id_map
Proof state before:
case a
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
⊢ ∀ (x : α), x ∈ Set.map id s ↔ x ∈ s
Tactic:
intro x
Proof state after:
case a
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ Set.map id s ↔ x ∈ s
Theorem: Set.id_map
Proof state before:
case a
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ Set.map id s ↔ x ∈ s
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ Set.map id s → x ∈ s

case a.mpr
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ s → x ∈ Set.map id s
Theorem: Set.id_map
Proof state before:
case a.mp
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ Set.map id s → x ∈ s
Tactic:
intro ⟨_, hx, rfl⟩
Proof state after:
case a.mp
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
hx : x ∈ s
⊢ x ∈ s
Theorem: Set.id_map
Proof state before:
case a.mp
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
hx : x ∈ s
⊢ x ∈ s
Tactic:
exact hx
Proof state after:
no goals
Theorem: Set.id_map
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
⊢ x ∈ s → x ∈ Set.map id s
Tactic:
intro hx
Proof state after:
case a.mpr
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
hx : x ∈ s
⊢ x ∈ Set.map id s
Theorem: Set.id_map
Proof state before:
case a.mpr
α : Sort u_1
β : ?m.4818
γ : ?m.4821
s : Set α
x : α
hx : x ∈ s
⊢ x ∈ Set.map id s
Tactic:
refine ⟨x, hx, rfl⟩
Proof state after:
no goals
Theorem: Set.comp_map
Proof state before:
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ Set.map (g ∘ f) s = Set.map g (Set.map f s)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ Set.map (g ∘ f) s ↔ x ∈ Set.map g (Set.map f s)
Theorem: Set.comp_map
Proof state before:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ Set.map (g ∘ f) s ↔ x ∈ Set.map g (Set.map f s)
Tactic:
intro z
Proof state after:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s ↔ z ∈ Set.map g (Set.map f s)
Theorem: Set.comp_map
Proof state before:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s ↔ z ∈ Set.map g (Set.map f s)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s → z ∈ Set.map g (Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map g (Set.map f s) → z ∈ Set.map (g ∘ f) s
Theorem: Set.comp_map
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s → z ∈ Set.map g (Set.map f s)
Tactic:
intro ⟨x, hx, hxz⟩
Proof state after:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
x : α
hx : x ∈ s
hxz : (g ∘ f) x = z
⊢ z ∈ Set.map g (Set.map f s)
Theorem: Set.comp_map
Proof state before:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
x : α
hx : x ∈ s
hxz : (g ∘ f) x = z
⊢ z ∈ Set.map g (Set.map f s)
Tactic:
refine ⟨f x, ⟨x, hx, rfl⟩, hxz⟩
Proof state after:
no goals
Theorem: Set.comp_map
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map g (Set.map f s) → z ∈ Set.map (g ∘ f) s
Tactic:
intro ⟨y, ⟨x, hx, hxy⟩, hyz⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ z ∈ Set.map (g ∘ f) s
Theorem: Set.comp_map
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ z ∈ Set.map (g ∘ f) s
Tactic:
refine ⟨x, hx, ?_⟩
Proof state after:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ (g ∘ f) x = z
Theorem: Set.comp_map
Proof state before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ (g ∘ f) x = z
Tactic:
rw [←hyz, ←hxy, Function.comp_apply]
Proof state after:
no goals
Theorem: Set.map_pure
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
⊢ Set.map f (Set.pure a) = Set.pure (f a)
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
⊢ ∀ (x : β), x ∈ Set.map f (Set.pure a) ↔ x ∈ Set.pure (f a)
Theorem: Set.map_pure
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
⊢ ∀ (x : β), x ∈ Set.map f (Set.pure a) ↔ x ∈ Set.pure (f a)
Tactic:
intro y
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) ↔ y ∈ Set.pure (f a)
Theorem: Set.map_pure
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) ↔ y ∈ Set.pure (f a)
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) → y ∈ Set.pure (f a)

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.pure (f a) → y ∈ Set.map f (Set.pure a)
Theorem: Set.map_pure
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) → y ∈ Set.pure (f a)
Tactic:
intro ⟨_, rfl, h⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ y ∈ Set.pure (f a)
Theorem: Set.map_pure
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ y ∈ Set.pure (f a)
Tactic:
rw [←h]
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ f a ∈ Set.pure (f a)
Theorem: Set.map_pure
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ f a ∈ Set.pure (f a)
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.map_pure
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.pure (f a) → y ∈ Set.map f (Set.pure a)
Tactic:
intro (h : y = f a)
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : y = f a
⊢ y ∈ Set.map f (Set.pure a)
Theorem: Set.map_pure
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : y = f a
⊢ y ∈ Set.map f (Set.pure a)
Tactic:
refine ⟨a, rfl, h.symm⟩
Proof state after:
no goals
Theorem: Set.map_pureIf
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
⊢ Set.map f (Set.pureIf a p) = Set.pureIf (f a) p
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
⊢ ∀ (x : β), x ∈ Set.map f (Set.pureIf a p) ↔ x ∈ Set.pureIf (f a) p
Theorem: Set.map_pureIf
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
⊢ ∀ (x : β), x ∈ Set.map f (Set.pureIf a p) ↔ x ∈ Set.pureIf (f a) p
Tactic:
intro y
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.map f (Set.pureIf a p) ↔ y ∈ Set.pureIf (f a) p
Theorem: Set.map_pureIf
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.map f (Set.pureIf a p) ↔ y ∈ Set.pureIf (f a) p
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.map f (Set.pureIf a p) → y ∈ Set.pureIf (f a) p

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.pureIf (f a) p → y ∈ Set.map f (Set.pureIf a p)
Theorem: Set.map_pureIf
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.map f (Set.pureIf a p) → y ∈ Set.pureIf (f a) p
Tactic:
intro ⟨_, ⟨rfl, hp⟩, h⟩
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
hp : p
h : f a = y
⊢ y ∈ Set.pureIf (f a) p
Theorem: Set.map_pureIf
Proof state before:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
hp : p
h : f a = y
⊢ y ∈ Set.pureIf (f a) p
Tactic:
refine ⟨h.symm, hp⟩
Proof state after:
no goals
Theorem: Set.map_pureIf
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
⊢ y ∈ Set.pureIf (f a) p → y ∈ Set.map f (Set.pureIf a p)
Tactic:
intro ⟨h, hp⟩
Proof state after:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
h : y = f a
hp : p
⊢ y ∈ Set.map f (Set.pureIf a p)
Theorem: Set.map_pureIf
Proof state before:
case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6074
f : α → β
a : α
p : Prop
y : β
h : y = f a
hp : p
⊢ y ∈ Set.map f (Set.pureIf a p)
Tactic:
refine ⟨a, ⟨rfl, hp⟩, h.symm⟩
Proof state after:
no goals
Theorem: Set.pure_bind
Proof state before:
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
⊢ (Set.pure a).bind f = f a
Tactic:
apply Set.ext
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pure a).bind f ↔ x ∈ f a
Theorem: Set.pure_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pure a).bind f ↔ x ∈ f a
Tactic:
intro y
Proof state after:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ (Set.pure a).bind f ↔ y ∈ f a
Theorem: Set.pure_bind
Proof state before:
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ (Set.pure a).bind f ↔ y ∈ f a
Tactic:
constructor
Proof state after:
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ (Set.pure a).bind f → y ∈ f a

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ f a → y ∈ (Set.pure a).bind f