internlm/Lean-Github huggingface dataset:
Theorem: Matrix.toOptionVec_eq_some_iff
Proof state before:
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
⊢ v = some a :> fun i => some (z i)
Tactic:
funext i
Proof state after:
case h
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
i : Fin (n + 1)
⊢ v i = (some a :> fun i => some (z i)) i
Theorem: Matrix.toOptionVec_eq_some_iff
Proof state before:
case h
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
i : Fin (n + 1)
⊢ v i = (some a :> fun i => some (z i)) i
Tactic:
cases i using Fin.cases <;> simp[hz, this]
Proof state after:
no goals
Theorem: Matrix.getM_pure
Proof state before:
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
β : Fin n → Type u
v : (i : Fin n) → β i
⊢ (getM fun i => pure (v i)) = pure v
Tactic:
induction' n with n ih <;> simp[empty_eq, getM]
Proof state after:
case zero
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ pure finZeroElim = pure v

case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (Seq.seq (pure fun succ i => cases (v 0) succ i) fun x => getM fun x => pure (v x.succ)) = pure v
Theorem: Matrix.getM_pure
Proof state before:
case zero
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ pure finZeroElim = pure v
Tactic:
congr
Proof state after:
case zero.e_a
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ finZeroElim = v
Theorem: Matrix.getM_pure
Proof state before:
case zero.e_a
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
⊢ finZeroElim = v
Tactic:
funext x
Proof state after:
case zero.e_a.h
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
x : Fin 0
⊢ finZeroElim x = v x
Theorem: Matrix.getM_pure
Proof state before:
case zero.e_a.h
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
β : Fin 0 → Type u
v : (i : Fin 0) → β i
x : Fin 0
⊢ finZeroElim x = v x
Tactic:
exact x.elim0
Proof state after:
no goals
Theorem: Matrix.getM_pure
Proof state before:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (Seq.seq (pure fun succ i => cases (v 0) succ i) fun x => getM fun x => pure (v x.succ)) = pure v
Tactic:
simp[vecHead, vecTail, Function.comp, seq_eq_bind, ih]
Proof state after:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (pure fun i => cases (v 0) (fun i => v i.succ) i) = pure v
Theorem: Matrix.getM_pure
Proof state before:
case succ
α✝ : Type ?u.58801
m : Type u → Type v
inst✝¹ : Monad m
α : Type w
β✝ : Type u
inst✝ : LawfulMonad m
n : ℕ
ih : ∀ {β : Fin n → Type u} (v : (i : Fin n) → β i), (getM fun i => pure (v i)) = pure v
β : Fin (n + 1) → Type u
v : (i : Fin (n + 1)) → β i
⊢ (pure fun i => cases (v 0) (fun i => v i.succ) i) = pure v
Tactic:
exact congr_arg _ (funext $ Fin.cases rfl (fun i => rfl))
Proof state after:
no goals
Theorem: Matrix.appendr_nil
Proof state before:
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
⊢ appendr ![] w = w
Tactic:
funext i
Proof state after:
case h
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
i : Fin (m + 0)
⊢ appendr ![] w i = w i
Theorem: Matrix.appendr_nil
Proof state before:
case h
α✝ : Type ?u.62658
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m : ℕ
w : Fin m → α
i : Fin (m + 0)
⊢ appendr ![] w i = w i
Tactic:
simp [appendr]
Proof state after:
no goals
Theorem: Matrix.appendr_cons
Proof state before:
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
⊢ appendr (x :> v) w = x :> appendr v w
Tactic:
funext i
Proof state after:
case h
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
i : Fin (m + n.succ)
⊢ appendr (x :> v) w i = (x :> appendr v w) i
Theorem: Matrix.appendr_cons
Proof state before:
case h
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
i : Fin (m + n.succ)
⊢ appendr (x :> v) w i = (x :> appendr v w) i
Tactic:
simp [appendr]
Proof state after:
no goals
Theorem: DMatrix.eq_vecCons
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
s : (i : Fin (n + 1)) → α i
⊢ s 0 = (s 0 ::> fun i => s i.succ) 0
Tactic:
simp
Proof state after:
no goals
Theorem: DMatrix.eq_vecCons
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
s : (i : Fin (n + 1)) → α i
⊢ ∀ (i : Fin n), s i.succ = (s 0 ::> fun i => s i.succ) i.succ
Tactic:
simp
Proof state after:
no goals
Theorem: DMatrix.vecCons_ext
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
⊢ a₁ ::> s₁ = a₂ ::> s₂ → a₁ = a₂ ∧ s₁ = s₂
Tactic:
intros h
Proof state after:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Theorem: DMatrix.vecCons_ext
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂ ∧ s₁ = s₂
Tactic:
constructor
Proof state after:
case left
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂

case right
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ s₁ = s₂
Theorem: DMatrix.vecCons_ext
Proof state before:
case left
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ a₁ = a₂
Tactic:
exact congrFun h 0
Proof state after:
no goals
Theorem: DMatrix.vecCons_ext
Proof state before:
case right
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
⊢ s₁ = s₂
Tactic:
exact funext (fun i => by simpa using congrFun h i.succ)
Proof state after:
no goals
Theorem: DMatrix.vecCons_ext
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ ::> s₁ = a₂ ::> s₂
i : Fin n
⊢ s₁ i = s₂ i
Tactic:
simpa using congrFun h i.succ
Proof state after:
no goals
Theorem: DMatrix.vecCons_ext
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
⊢ a₁ = a₂ ∧ s₁ = s₂ → a₁ ::> s₁ = a₂ ::> s₂
Tactic:
intros h
Proof state after:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ ::> s₁ = a₂ ::> s₂
Theorem: DMatrix.vecCons_ext
Proof state before:
n : ℕ
α : Fin (n + 1) → Type u_1
a₁ a₂ : α 0
s₁ s₂ : (i : Fin n) → α i.succ
h : a₁ = a₂ ∧ s₁ = s₂
⊢ a₁ ::> s₁ = a₂ ::> s₂
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Option.toList_eq_iff
Proof state before:
α : Type u_1
o : Option α
a : α
⊢ o.toList = [a] ↔ o = some a
Tactic:
rcases o <;> simp
Proof state after:
no goals
Theorem: Nat.unvector_le
Proof state before:
n e : ℕ
i : Fin n
⊢ unvector e i ≤ e
Tactic:
induction' n with n ih generalizing e <;> simp[*, unvector]
Proof state after:
case zero
n e : ℕ
i : Fin 0
⊢ ![] ≤ e

case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e
Theorem: Nat.unvector_le
Proof state before:
case zero
n e : ℕ
i : Fin 0
⊢ ![] ≤ e
Tactic:
have := i.isLt
Proof state after:
case zero
n e : ℕ
i : Fin 0
this : ↑i < 0
⊢ ![] ≤ e
Theorem: Nat.unvector_le
Proof state before:
case zero
n e : ℕ
i : Fin 0
this : ↑i < 0
⊢ ![] ≤ e
Tactic:
contradiction
Proof state after:
no goals
Theorem: Nat.unvector_le
Proof state before:
case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e
Tactic:
exact Fin.cases (by simpa using Nat.unpair_left_le _) (fun i => le_trans (ih e.unpair.2 i) (Nat.unpair_right_le _)) i
Proof state after:
no goals
Theorem: Nat.unvector_le
Proof state before:
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) 0 ≤ e
Tactic:
simpa using Nat.unpair_left_le _
Proof state after:
no goals
Theorem: Nat.unvector_vecToNat
Proof state before:
n : ℕ
v : Fin n → ℕ
⊢ unvector (vecToNat v) = v
Tactic:
induction n <;> simp[*, Nat.unvector, vecToNat, Matrix.empty_eq]
Proof state after:
case succ
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
⊢ v 0 :> v ∘ Fin.succ = v
Theorem: Nat.unvector_vecToNat
Proof state before:
case succ
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
⊢ v 0 :> v ∘ Fin.succ = v
Tactic:
exact funext (fun i => i.cases (by simp[Matrix.empty_eq]) (by simp[Matrix.empty_eq]))
Proof state after:
no goals
Theorem: Nat.unvector_vecToNat
Proof state before:
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
i : Fin n✝.succ
⊢ (v 0 :> v ∘ Fin.succ) 0 = v 0
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: Nat.unvector_vecToNat
Proof state before:
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
i : Fin n✝.succ
⊢ ∀ (i : Fin n✝), (v 0 :> v ∘ Fin.succ) i.succ = v i.succ
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: Nat.one_le_of_bodd
Proof state before:
n✝ n : ℕ
h : n.bodd = true
⊢ 1 ≤ n
Tactic:
induction n <;> simp[←Nat.add_one] at h ⊢
Proof state after:
no goals
Theorem: Nat.pair_le_pair_of_le
Proof state before:
n a₁ a₂ b₁ b₂ : ℕ
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl) <;> rcases lt_or_eq_of_le hb with (hb | rfl)
Proof state after:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂

case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂

case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (lt_trans (Nat.pair_lt_pair_left b₁ ha) (Nat.pair_lt_pair_right a₂ hb)) }
Proof state after:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (Nat.pair_lt_pair_left b₁ ha) }
Proof state after:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ exact le_of_lt (Nat.pair_lt_pair_right a₁ hb) }
Proof state after:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
{ rfl }
Proof state after:
no goals
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
Tactic:
exact le_of_lt (lt_trans (Nat.pair_lt_pair_left b₁ ha) (Nat.pair_lt_pair_right a₂ hb))
Proof state after:
no goals
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁
Tactic:
exact le_of_lt (Nat.pair_lt_pair_left b₁ ha)
Proof state after:
no goals
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂
Tactic:
exact le_of_lt (Nat.pair_lt_pair_right a₁ hb)
Proof state after:
no goals
Theorem: Nat.pair_le_pair_of_le
Proof state before:
case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Fintype.elem_le_sup
Proof state before:
ι : Type u_2
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ι → α
i : ι
⊢ i ∈ Finset.univ
Tactic:
simp
Proof state after:
no goals
Theorem: Fintype.sup_le_iff
Proof state before:
ι : Type u_2
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ι → α
a : α
⊢ sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
Tactic:
simp[sup]
Proof state after:
no goals
Theorem: Fintype.finsup_eq_0_of_empty
Proof state before:
ι : Type u_1
inst✝³ : Fintype ι
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ sup f = ⊥
Tactic:
simp[sup]
Proof state after:
no goals
Theorem: Empty.eq_elim
Proof state before:
α : Sort u
f : Empty → α
⊢ ∀ (x : Empty), f x = x.elim
Tactic:
rintro ⟨⟩
Proof state after:
no goals
Theorem: Function.funEqOn.of_subset
Proof state before:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
⊢ funEqOn q f g
Tactic:
intro a ha
Proof state after:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
a : α
ha : q a
⊢ f a = g a
Theorem: Function.funEqOn.of_subset
Proof state before:
α : Type u
β : Type v
p q : α → Prop
f g : α → β
e : funEqOn p f g
h : ∀ (a : α), q a → p a
a : α
ha : q a
⊢ f a = g a
Tactic:
exact e a (h a ha)
Proof state after:
no goals
Theorem: Quotient.liftVec_mk
Proof state before:
α : Type u
s : Setoid α
β : Sort v
n : ℕ
f : (Fin n → α) → β
h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin n → α
⊢ liftVec f h (Quotient.mk s ∘ v) = f v
Tactic:
induction' n with n ih <;> simp[liftVec, empty_eq, Quotient.liftOn_mk]
Proof state after:
case succ
α : Type u
s : Setoid α
β : Sort v
n : ℕ
ih :
  ∀ (f : (Fin n → α) → β) (h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin n → α),
    liftVec f h (Quotient.mk s ∘ v) = f v
f : (Fin (n + 1) → α) → β
h : ∀ (v₁ v₂ : Fin (n + 1) → α), (∀ (n : Fin (n + 1)), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin (n + 1) → α
⊢ liftVec (fun v_1 => f (vecHead v :> v_1)) ⋯ (Quotient.mk s ∘ vecTail v) = f v
Theorem: Quotient.liftVec_mk
Proof state before:
case succ
α : Type u
s : Setoid α
β : Sort v
n : ℕ
ih :
  ∀ (f : (Fin n → α) → β) (h : ∀ (v₁ v₂ : Fin n → α), (∀ (n : Fin n), v₁ n ≈ v₂ n) → f v₁ = f v₂) (v : Fin n → α),
    liftVec f h (Quotient.mk s ∘ v) = f v
f : (Fin (n + 1) → α) → β
h : ∀ (v₁ v₂ : Fin (n + 1) → α), (∀ (n : Fin (n + 1)), v₁ n ≈ v₂ n) → f v₁ = f v₂
v : Fin (n + 1) → α
⊢ liftVec (fun v_1 => f (vecHead v :> v_1)) ⋯ (Quotient.mk s ∘ vecTail v) = f v
Tactic:
simpa using ih (fun v' => f (vecHead v :> v'))
  (fun v₁ v₂ hv => h (vecHead v :> v₁) (vecHead v :> v₂) (Fin.cases (refl _) hv)) (vecTail v)
Proof state after:
no goals
Theorem: List.lt_upper
Proof state before:
l : List ℕ
n : ℕ
h : n ∈ l
⊢ n < l.upper
Tactic:
induction' l with n ns ih <;> simp at h ⊢
Proof state after:
case cons
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Theorem: List.lt_upper
Proof state before:
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
case cons =>
  rcases h with (rfl | h); { exact Or.inl (Nat.lt_succ_self _) }
  exact Or.inr (ih h)
Proof state after:
no goals
Theorem: List.lt_upper
Proof state before:
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ = n ∨ n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
rcases h with (rfl | h)
Proof state after:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper

case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Theorem: List.lt_upper
Proof state before:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper

case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
{ exact Or.inl (Nat.lt_succ_self _) }
Proof state after:
case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Theorem: List.lt_upper
Proof state before:
case inr
n✝ n : ℕ
ns : List ℕ
ih : n✝ ∈ ns → n✝ < ns.upper
h : n✝ ∈ ns
⊢ n✝ < n + 1 ∨ n✝ < ns.upper
Tactic:
exact Or.inr (ih h)
Proof state after:
no goals
Theorem: List.lt_upper
Proof state before:
case inl
n : ℕ
ns : List ℕ
ih : n ∈ ns → n < ns.upper
⊢ n < n + 1 ∨ n < ns.upper
Tactic:
exact Or.inl (Nat.lt_succ_self _)
Proof state after:
no goals
Theorem: List.toFinset_map
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : α → β
l : List α
⊢ (map f l).toFinset = Finset.image f l.toFinset
Tactic:
induction l <;> simp[*]
Proof state after:
no goals
Theorem: List.toFinset_mono
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
⊢ l.toFinset ⊆ l'.toFinset
Tactic:
intro a
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l.toFinset → a ∈ l'.toFinset
Theorem: List.toFinset_mono
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l.toFinset → a ∈ l'.toFinset
Tactic:
simp
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l → a ∈ l'
Theorem: List.toFinset_mono
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
⊢ a ∈ l → a ∈ l'
Tactic:
intro ha
Proof state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
ha : a ∈ l
⊢ a ∈ l'
Theorem: List.toFinset_mono
Proof state before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
l l' : List α
h : l ⊆ l'
a : α
ha : a ∈ l
⊢ a ∈ l'
Tactic:
exact h ha
Proof state after:
no goals
Theorem: List.le_sup
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
⊢ a ∈ l → a ≤ l.sup
Tactic:
induction' l with a l ih <;> simp[*]
Proof state after:
case cons
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
⊢ a✝ = a ∨ a✝ ∈ l → a✝ ≤ a ⊔ l.sup
Theorem: List.le_sup
Proof state before:
case cons
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
⊢ a✝ = a ∨ a✝ ∈ l → a✝ ≤ a ⊔ l.sup
Tactic:
rintro (rfl | h)
Proof state after:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup

case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Theorem: List.le_sup
Proof state before:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup

case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
{ simp }
Proof state after:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Theorem: List.le_sup
Proof state before:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
{ exact le_sup_of_le_right $ ih h }
Proof state after:
no goals
Theorem: List.le_sup
Proof state before:
case cons.inl
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a : α
l : List α
ih : a ∈ l → a ≤ l.sup
⊢ a ≤ a ⊔ l.sup
Tactic:
simp
Proof state after:
no goals
Theorem: List.le_sup
Proof state before:
case cons.inr
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a✝ a : α
l : List α
ih : a✝ ∈ l → a✝ ≤ l.sup
h : a✝ ∈ l
⊢ a✝ ≤ a ⊔ l.sup
Tactic:
exact le_sup_of_le_right $ ih h
Proof state after:
no goals
Theorem: List.getI_map_range
Proof state before:
α✝ : Type u
inst✝⁴ : DecidableEq α✝
β : Type v
inst✝³ : DecidableEq β
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
i n : ℕ
inst✝ : Inhabited α
f : ℕ → α
h : i < n
⊢ (map f (range n)).getI i = f i
Tactic:
simpa using List.getI_eq_get ((List.range n).map f) (n := i) (by simpa using h)
Proof state after:
no goals
Theorem: List.getI_map_range
Proof state before:
α✝ : Type u
inst✝⁴ : DecidableEq α✝
β : Type v
inst✝³ : DecidableEq β
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
i n : ℕ
inst✝ : Inhabited α
f : ℕ → α
h : i < n
⊢ i < (map f (range n)).length
Tactic:
simpa using h
Proof state after:
no goals
Theorem: List.sup_ofFn
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : Fin n → α
⊢ (ofFn f).sup = Finset.univ.sup f
Tactic:
induction' n with n ih <;> simp
Proof state after:
case succ
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : DecidableEq β
α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
ih : ∀ (f : Fin n → α), (ofFn f).sup = Finset.univ.sup f
f : Fin (n + 1) → α
⊢ f 0 ⊔ (ofFn fun i => f i.succ).sup = Finset.univ.sup f