internlm/Lean-Github huggingface dataset:
Theorem: List.countP_image_le_length
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ countP (fun b => decide (f a = b)) lb ≤ 1
Tactic:
refine countP_le_one_of_unique_nodup ?_ hnodup
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ ∀ (a_1 b : β), decide (f a = a_1) = true → decide (f a = b) = true → a_1 = b
Theorem: List.countP_image_le_length
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
⊢ ∀ (a_1 b : β), decide (f a = a_1) = true → decide (f a = b) = true → a_1 = b
Tactic:
intro b₁ b₂ hb₁ hb₂
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₁ b₂ : β
hb₁ : decide (f a = b₁) = true
hb₂ : decide (f a = b₂) = true
⊢ b₁ = b₂
Theorem: List.countP_image_le_length
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₁ b₂ : β
hb₁ : decide (f a = b₁) = true
hb₂ : decide (f a = b₂) = true
⊢ b₁ = b₂
Tactic:
cases of_decide_eq_true hb₁
Proof state after:
case cons.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₂ : β
hb₂ : decide (f a = b₂) = true
hb₁ : decide (f a = f a) = true
⊢ f a = b₂
Theorem: List.countP_image_le_length
Proof state before:
case cons.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
b₂ : β
hb₂ : decide (f a = b₂) = true
hb₁ : decide (f a = f a) = true
⊢ f a = b₂
Tactic:
cases of_decide_eq_true hb₂
Proof state after:
case cons.refl.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
hb₁ hb₂ : decide (f a = f a) = true
⊢ f a = f a
Theorem: List.countP_image_le_length
Proof state before:
case cons.refl.refl
α : Type u
β : Type v
inst✝ : DecidableEq β
lb : List β
hnodup : Nodup lb
f : α → β
a : α
la : List α
IH : countP (fun b => decide (∃ a, a ∈ la ∧ f a = b)) lb ≤ length la
hb₁ hb₂ : decide (f a = f a) = true
⊢ f a = f a
Tactic:
rfl
Proof state after:
no goals
Theorem: List.countP_mono_right
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
l l' : List α
hsub : l ⊆ l'
nodup : Nodup l
⊢ countP p l ≤ countP p l'
Tactic:
induction l generalizing l' with
| nil => exact Nat.zero_le _
| cons a l IH =>
  let .cons nodup_head (nodup_tail : l.Nodup) := nodup
  simp only [countP_cons]
  cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
  . refine IH (subset_of_cons_subset hsub) nodup_tail
  let l'' := l'.erase a
  have : l ⊆ l'' := fun b h => by
    simp only [List.mem_erase_of_ne (nodup_head b h).symm]
    specialize @hsub b
    simp only [List.mem_cons] at hsub
    exact hsub <| Or.inr h
  specialize IH this nodup_tail
  refine trans (s:=Eq) (Nat.succ_le_succ IH) ?_
  refine Eq.symm <| countP_erase_true ?_ hpa
  exact (cons_subset.mp hsub).1
Proof state after:
no goals
Theorem: List.countP_mono_right
Proof state before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
l' : List α
hsub : [] ⊆ l'
nodup : Nodup []
⊢ countP p [] ≤ countP p l'
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: List.countP_mono_right
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
⊢ countP p (a :: l) ≤ countP p l'
Tactic:
let .cons nodup_head (nodup_tail : l.Nodup) := nodup
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ countP p (a :: l) ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ countP p (a :: l) ≤ countP p l'
Tactic:
simp only [countP_cons]
Proof state after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ (countP p l + if p a = true then 1 else 0) ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
⊢ (countP p l + if p a = true then 1 else 0) ≤ countP p l'
Tactic:
cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
Proof state after:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'

case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'

case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Tactic:
. refine IH (subset_of_cons_subset hsub) nodup_tail
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
⊢ countP p l + 1 ≤ countP p l'
Tactic:
let l'' := l'.erase a
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
⊢ countP p l + 1 ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
⊢ countP p l + 1 ≤ countP p l'
Tactic:
have : l ⊆ l'' := fun b h => by
  simp only [List.mem_erase_of_ne (nodup_head b h).symm]
  specialize @hsub b
  simp only [List.mem_cons] at hsub
  exact hsub <| Or.inr h
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
⊢ countP p l + 1 ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
⊢ countP p l + 1 ≤ countP p l'
Tactic:
specialize IH this nodup_tail
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ countP p l + 1 ≤ countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ countP p l + 1 ≤ countP p l'
Tactic:
refine trans (s:=Eq) (Nat.succ_le_succ IH) ?_
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ Nat.succ (countP p l'') = countP p l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ Nat.succ (countP p l'') = countP p l'
Tactic:
refine Eq.symm <| countP_erase_true ?_ hpa
Proof state after:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ a ∈ l'
Theorem: List.countP_mono_right
Proof state before:
case cons.true
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
this : l ⊆ l''
IH : countP p l ≤ countP p l''
⊢ a ∈ l'
Tactic:
exact (cons_subset.mp hsub).1
Proof state after:
no goals
Theorem: List.countP_mono_right
Proof state before:
case cons.false
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = false
⊢ countP p l ≤ countP p l'
Tactic:
refine IH (subset_of_cons_subset hsub) nodup_tail
Proof state after:
no goals
Theorem: List.countP_mono_right
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l''
Tactic:
simp only [List.mem_erase_of_ne (nodup_head b h).symm]
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l'
Theorem: List.countP_mono_right
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
hsub : a :: l ⊆ l'
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
⊢ b ∈ l'
Tactic:
specialize @hsub b
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b ∈ a :: l → b ∈ l'
⊢ b ∈ l'
Theorem: List.countP_mono_right
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b ∈ a :: l → b ∈ l'
⊢ b ∈ l'
Tactic:
simp only [List.mem_cons] at hsub
Proof state after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b = a ∨ b ∈ l → b ∈ l'
⊢ b ∈ l'
Theorem: List.countP_mono_right
Proof state before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
l : List α
IH : ∀ {l' : List α}, l ⊆ l' → Nodup l → countP p l ≤ countP p l'
l' : List α
nodup : Nodup (a :: l)
nodup_head : ∀ (a' : α), a' ∈ l → a ≠ a'
nodup_tail : Nodup l
hpa : p a = true
l'' : List α := List.erase l' a
b : α
h : b ∈ l
hsub : b = a ∨ b ∈ l → b ∈ l'
⊢ b ∈ l'
Tactic:
exact hsub <| Or.inr h
Proof state after:
no goals
Theorem: List.length_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (ofFn f) = n
Tactic:
dsimp [ofFn]
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.toList (Array.ofFn f)) = n
Theorem: List.length_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.toList (Array.ofFn f)) = n
Tactic:
rewrite [Array.toList_eq]
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.ofFn f).data = n
Theorem: List.length_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ length (Array.ofFn f).data = n
Tactic:
show (Array.ofFn f).size = n
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ Array.size (Array.ofFn f) = n
Theorem: List.length_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
⊢ Array.size (Array.ofFn f) = n
Tactic:
exact Array.size_ofFn f
Proof state after:
no goals
Theorem: List.get_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (Fin.cast (_ : length (ofFn f) = n) i)
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (ofFn f)
⊢ get (ofFn f) { val := i, isLt := hi } = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Theorem: List.get_ofFn
Proof state before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (ofFn f)
⊢ get (ofFn f) { val := i, isLt := hi } = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
dsimp [ofFn] at hi ⊢
Proof state after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ get (Array.toList (Array.ofFn f)) { val := i, isLt := hi } =
    f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Theorem: List.get_ofFn
Proof state before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ get (Array.toList (Array.ofFn f)) { val := i, isLt := hi } =
    f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
simp only [get_of_eq (Array.toList_eq _), ← Array.getElem_eq_data_get]
Proof state after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Theorem: List.get_ofFn
Proof state before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi : i < length (Array.toList (Array.ofFn f))
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi })
Tactic:
conv at hi => rewrite [Array.toList_eq]
Proof state after:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi✝ : i < length (Array.toList (Array.ofFn f))
hi : i < length (Array.ofFn f).data
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ })
Theorem: List.get_ofFn
Proof state before:
case mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
i : Nat
hi✝ : i < length (Array.toList (Array.ofFn f))
hi : i < length (Array.ofFn f).data
⊢ (Array.ofFn f)[i] = f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ })
Tactic:
exact Array.getElem_ofFn f i hi
Proof state after:
no goals
Theorem: List.mem_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ ∃ i, f i = a
Tactic:
rewrite [List.mem_iff_get]
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, get (ofFn f) n_1 = a) ↔ ∃ i, f i = a
Theorem: List.mem_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, get (ofFn f) n_1 = a) ↔ ∃ i, f i = a
Tactic:
simp only [get_ofFn]
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) ↔ ∃ i, f i = a
Theorem: List.mem_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) ↔ ∃ i, f i = a
Tactic:
constructor
Proof state after:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a

case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Theorem: List.mem_ofFn
Proof state before:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a

case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
. rintro ⟨⟨i,hi⟩,ha⟩
  simp only [length_ofFn] at hi
  exact ⟨⟨i,hi⟩, ha⟩
Proof state after:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Theorem: List.mem_ofFn
Proof state before:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
. rintro ⟨⟨i,hi⟩,ha⟩
  exists ⟨i, by rewrite [length_ofFn]; exact hi⟩
Proof state after:
no goals
Theorem: List.mem_ofFn
Proof state before:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a
Tactic:
rintro ⟨⟨i,hi⟩,ha⟩
Proof state after:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi }) = a
⊢ ∃ i, f i = a
Theorem: List.mem_ofFn
Proof state before:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi }) = a
⊢ ∃ i, f i = a
Tactic:
simp only [length_ofFn] at hi
Proof state after:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi✝ : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ }) = a
hi : i < n
⊢ ∃ i, f i = a
Theorem: List.mem_ofFn
Proof state before:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi✝ : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ }) = a
hi : i < n
⊢ ∃ i, f i = a
Tactic:
exact ⟨⟨i,hi⟩, ha⟩
Proof state after:
no goals
Theorem: List.mem_ofFn
Proof state before:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
rintro ⟨⟨i,hi⟩,ha⟩
Proof state after:
case mpr.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Theorem: List.mem_ofFn
Proof state before:
case mpr.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
exists ⟨i, by rewrite [length_ofFn]; exact hi⟩
Proof state after:
no goals
Theorem: List.mem_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < length (ofFn f)
Tactic:
rewrite [length_ofFn]
Proof state after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < n
Theorem: List.mem_ofFn
Proof state before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < n
Tactic:
exact hi
Proof state after:
no goals
Theorem: Permutation.sign_one
Proof state before:
m n : Nat
⊢ sign 1 = false
Tactic:
dsimp [sign]
Proof state after:
m n : Nat
⊢ (inversionNum 1 % 2 == 1) = false
Theorem: Permutation.sign_one
Proof state before:
m n : Nat
⊢ (inversionNum 1 % 2 == 1) = false
Tactic:
rewrite [inversionNum_one]
Proof state after:
m n : Nat
⊢ (0 % 2 == 1) = false
Theorem: Permutation.sign_one
Proof state before:
m n : Nat
⊢ (0 % 2 == 1) = false
Tactic:
decide
Proof state after:
no goals
Theorem: Permutation.sign_mul
Proof state before:
m n : Nat
x y : Permutation n
this :
  (fun x => x % 2) (inversionNum x + inversionNum y) =
    (fun x => x % 2)
      (inversionNum (x * y) +
        2 * BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑y[↑t.fst] > ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] < ↑(x * y)[↑t.snd])
⊢ sign (x * y) = (sign x != sign y)
Tactic:
conv at this =>
  dsimp; rw [Nat.add_mul_mod_self_left, Nat.add_mod]
Proof state after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ sign (x * y) = (sign x != sign y)
Theorem: Permutation.sign_mul
Proof state before:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ sign (x * y) = (sign x != sign y)
Tactic:
dsimp [sign]
Proof state after:
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ (inversionNum (x * y) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))