internlm/Lean-Github huggingface dataset:
Theorem: List.Index.sigma_unsigma
Proof state before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝.unappend = Sum.inr k
⊢ sigma k✝.unsigma = k✝
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝ = append (Sum.inr k)
⊢ sigma k✝.unsigma = k✝
Theorem: List.Index.sigma_unsigma
Proof state before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝ = append (Sum.inr k)
⊢ sigma k✝.unsigma = k✝
Tactic:
cases h
Proof state after:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
⊢ sigma (append (Sum.inr k)).unsigma = append (Sum.inr k)
Theorem: List.Index.sigma_unsigma
Proof state before:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
⊢ sigma (append (Sum.inr k)).unsigma = append (Sum.inr k)
Tactic:
rw [unsigma, unappend_append, sigma, ih]
Proof state after:
no goals
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
⊢ sigma i = k ↔ i = k.unsigma
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
⊢ sigma i = k → i = k.unsigma

case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
⊢ i = k.unsigma → sigma i = k
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
⊢ sigma i = k → i = k.unsigma
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
h : sigma i = k
⊢ i = k.unsigma
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
h : sigma i = k
⊢ i = k.unsigma
Tactic:
cases h
Proof state after:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ i = (sigma i).unsigma
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ i = (sigma i).unsigma
Tactic:
rw [unsigma_sigma]
Proof state after:
no goals
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
⊢ i = k.unsigma → sigma i = k
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
h : i = k.unsigma
⊢ sigma i = k
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
k : (xs.sigma f).Index
h : i = k.unsigma
⊢ sigma i = k
Tactic:
cases h
Proof state after:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ sigma k.unsigma = k
Theorem: List.Index.sigma_eq_iff_eq_unsigma
Proof state before:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
rw [sigma_unsigma]
Proof state after:
no goals
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i ↔ k = sigma i
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i → k = sigma i

case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k = sigma i → k.unsigma = i
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i → k = sigma i
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k.unsigma = i
⊢ k = sigma i
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k.unsigma = i
⊢ k = sigma i
Tactic:
cases h
Proof state after:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ k = sigma k.unsigma
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ k = sigma k.unsigma
Tactic:
rw [sigma_unsigma]
Proof state after:
no goals
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k = sigma i → k.unsigma = i
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k = sigma i
⊢ k.unsigma = i
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k = sigma i
⊢ k.unsigma = i
Tactic:
cases h
Proof state after:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Theorem: List.Index.unsigma_eq_iff_eq_sigma
Proof state before:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
rw [unsigma_sigma]
Proof state after:
no goals
Theorem: List.Index.val_sigma
Proof state before:
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).val = ⟨i.fst.val, i.snd.val⟩
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨head, j⟩ => rw [sigma, val_append_inl, val_map]
  | ⟨tail i, j⟩ => rw [sigma, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_sigma
Proof state before:
case nil
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : [].Index) × (f i.val).Index
⊢ (sigma i).val = ⟨i.fst.val, i.snd.val⟩
Tactic:
cases i
Proof state after:
case nil.mk
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (sigma ⟨fst✝, snd✝⟩).val = ⟨⟨fst✝, snd✝⟩.fst.val, ⟨fst✝, snd✝⟩.snd.val⟩
Theorem: List.Index.val_sigma
Proof state before:
case nil.mk
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (sigma ⟨fst✝, snd✝⟩).val = ⟨⟨fst✝, snd✝⟩.fst.val, ⟨fst✝, snd✝⟩.snd.val⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.val_sigma
Proof state before:
case cons
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).val = ⟨i.fst.val, i.snd.val⟩
i : (i : (x :: xs).Index) × (f i.val).Index
⊢ (sigma i).val = ⟨i.fst.val, i.snd.val⟩
Tactic:
match i with
| ⟨head, j⟩ => rw [sigma, val_append_inl, val_map]
| ⟨tail i, j⟩ => rw [sigma, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_sigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).val = ⟨i.fst.val, i.snd.val⟩
i : (i : (x :: xs).Index) × (f i.val).Index
j : (f head.val).Index
⊢ (sigma ⟨head, j⟩).val = ⟨⟨head, j⟩.fst.val, ⟨head, j⟩.snd.val⟩
Tactic:
rw [sigma, val_append_inl, val_map]
Proof state after:
no goals
Theorem: List.Index.val_sigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).val = ⟨i.fst.val, i.snd.val⟩
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ (sigma ⟨i.tail, j⟩).val = ⟨⟨i.tail, j⟩.fst.val, ⟨i.tail, j⟩.snd.val⟩
Tactic:
rw [sigma, val_append_inr, ih]
Proof state after:
no goals
Theorem: List.Index.val_unsigma
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
k : (xs.sigma f).Index
⊢ ⟨k.unsigma.fst.val, k.unsigma.snd.val⟩ = k.val
Tactic:
rw [←sigma_unsigma k, val_sigma, unsigma_sigma]
Proof state after:
no goals
Theorem: List.Index.unpi_pi
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
⊢ (pi h).unpi = h
Tactic:
funext i
Proof state after:
case h
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
i : xs.Index
⊢ (pi h).unpi i = h i
Theorem: List.Index.unpi_pi
Proof state before:
case h
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
i : xs.Index
⊢ (pi h).unpi i = h i
Tactic:
induction i with
| head => simp only [pi, unpi]; rw [unbind_bind, unmap_map]
| tail i ih => simp only [pi, unpi]; rw [unbind_bind, ih]
Proof state after:
no goals
Theorem: List.Index.unpi_pi
Proof state before:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (pi h).unpi head = h head
Tactic:
simp only [pi, unpi]
Proof state after:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ unmap
      (fun y i =>
        match i with
        | head => y
        | i.tail =>
          (unbind
                  (fun ys =>
                    List.map
                      (fun y i =>
                        match i with
                        | head => y
                        | i.tail => ys i)
                      (f x✝))
                  (bind
                    (fun ys =>
                      List.map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => ys i)
                        (f x✝))
                    ⟨pi fun i => h i.tail,
                      map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => (pi fun i => h i.tail).val i)
                        (h head)⟩)).fst.val
            i)
      (unbind
          (fun ys =>
            List.map
              (fun y i =>
                match i with
                | head => y
                | i.tail => ys i)
              (f x✝))
          (bind
            (fun ys =>
              List.map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => ys i)
                (f x✝))
            ⟨pi fun i => h i.tail,
              map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => (pi fun i => h i.tail).val i)
                (h head)⟩)).snd =
    h head
Theorem: List.Index.unpi_pi
Proof state before:
case h.head
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
x✝ : α
xs✝ : List α
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ unmap
      (fun y i =>
        match i with
        | head => y
        | i.tail =>
          (unbind
                  (fun ys =>
                    List.map
                      (fun y i =>
                        match i with
                        | head => y
                        | i.tail => ys i)
                      (f x✝))
                  (bind
                    (fun ys =>
                      List.map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => ys i)
                        (f x✝))
                    ⟨pi fun i => h i.tail,
                      map
                        (fun y i =>
                          match i with
                          | head => y
                          | i.tail => (pi fun i => h i.tail).val i)
                        (h head)⟩)).fst.val
            i)
      (unbind
          (fun ys =>
            List.map
              (fun y i =>
                match i with
                | head => y
                | i.tail => ys i)
              (f x✝))
          (bind
            (fun ys =>
              List.map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => ys i)
                (f x✝))
            ⟨pi fun i => h i.tail,
              map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => (pi fun i => h i.tail).val i)
                (h head)⟩)).snd =
    h head
Tactic:
rw [unbind_bind, unmap_map]
Proof state after:
no goals
Theorem: List.Index.unpi_pi
Proof state before:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (pi h).unpi i.tail = h i.tail
Tactic:
simp only [pi, unpi]
Proof state after:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (unbind
            (fun ys =>
              List.map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => ys i)
                (f x✝))
            (bind
              (fun ys =>
                List.map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => ys i)
                  (f x✝))
              ⟨pi fun i => h i.tail,
                map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => (pi fun i => h i.tail).val i)
                  (h head)⟩)).fst.unpi
      i =
    h i.tail
Theorem: List.Index.unpi_pi
Proof state before:
case h.tail
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs xs✝ : List α
x✝ : α
i : xs✝.Index
ih : ∀ (h : (i : xs✝.Index) → (f i.val).Index), (pi h).unpi i = h i
h : (i : (x✝ :: xs✝).Index) → (f i.val).Index
⊢ (unbind
            (fun ys =>
              List.map
                (fun y i =>
                  match i with
                  | head => y
                  | i.tail => ys i)
                (f x✝))
            (bind
              (fun ys =>
                List.map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => ys i)
                  (f x✝))
              ⟨pi fun i => h i.tail,
                map
                  (fun y i =>
                    match i with
                    | head => y
                    | i.tail => (pi fun i => h i.tail).val i)
                  (h head)⟩)).fst.unpi
      i =
    h i.tail
Tactic:
rw [unbind_bind, ih]
Proof state after:
no goals
Theorem: List.Index.pi_unpi
Proof state before:
case nil
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f []).Index
⊢ pi k.unpi = k
Tactic:
cases k
Proof state after:
case nil.head
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
⊢ pi head.unpi = head

case nil.tail
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
a✝ : [].Index
⊢ pi a✝.tail.unpi = a✝.tail
Theorem: List.Index.pi_unpi
Proof state before:
case nil.head
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
⊢ pi head.unpi = head
Tactic:
rfl
Proof state after:
no goals
Theorem: List.Index.pi_unpi
Proof state before:
case nil.tail
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
a✝ : [].Index
⊢ pi a✝.tail.unpi = a✝.tail
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.pi_unpi
Proof state before:
case cons
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k : (List.pi f (x :: xs)).Index
⊢ pi k.unpi = k
Tactic:
match h : unbind _ k with
| ⟨k₁,k₂⟩ =>
  rw [unbind_eq_iff_eq_bind] at h
  cases h
  simp only [pi, unpi]
  rw [unbind_bind, ih, map_unmap]
Proof state after:
no goals
Theorem: List.Index.pi_unpi
Proof state before:
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k : (List.pi f (x :: xs)).Index
k₁ : (List.pi f xs).Index
k₂ :
  (List.map
      (fun y i =>
        match i with
        | head => y
        | i.tail => k₁.val i)
      (f x)).Index
h :
  unbind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      k =
    ⟨k₁, k₂⟩
⊢ pi k.unpi = k
Tactic:
rw [unbind_eq_iff_eq_bind] at h
Proof state after:
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k : (List.pi f (x :: xs)).Index
k₁ : (List.pi f xs).Index
k₂ :
  (List.map
      (fun y i =>
        match i with
        | head => y
        | i.tail => k₁.val i)
      (f x)).Index
h :
  k =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
⊢ pi k.unpi = k
Theorem: List.Index.pi_unpi
Proof state before:
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k : (List.pi f (x :: xs)).Index
k₁ : (List.pi f xs).Index
k₂ :
  (List.map
      (fun y i =>
        match i with
        | head => y
        | i.tail => k₁.val i)
      (f x)).Index
h :
  k =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
⊢ pi k.unpi = k
Tactic:
cases h
Proof state after:
case refl
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs✝ : List α
x : α
xs : List α
ih : ∀ (k : (List.pi f xs).Index), pi k.unpi = k
k₁ : (List.pi f xs).Index
k₂ :
  (List.map
      (fun y i =>
        match i with
        | head => y
        | i.tail => k₁.val i)
      (f x)).Index
⊢ pi
      (bind
          (fun ys =>
            List.map
              (fun y i =>
                match i with
                | head => y
                | i.tail => ys i)
              (f x))
          ⟨k₁, k₂⟩).unpi =
    bind
      (fun ys =>
        List.map
          (fun y i =>
            match i with
            | head => y
            | i.tail => ys i)
          (f x))
      ⟨k₁, k₂⟩
Theorem: List.Index.pi_eq_iff_eq_unpi
Proof state before:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
⊢ pi h = k ↔ h = k.unpi
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
⊢ pi h = k → h = k.unpi

case mpr
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
⊢ h = k.unpi → pi h = k
Theorem: List.Index.pi_eq_iff_eq_unpi
Proof state before:
case mp
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
⊢ pi h = k → h = k.unpi
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h✝ : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
h : pi h✝ = k
⊢ h✝ = k.unpi
Theorem: List.Index.pi_eq_iff_eq_unpi
Proof state before:
case mp
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h✝ : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
h : pi h✝ = k
⊢ h✝ = k.unpi
Tactic:
rw [←h, unpi_pi]
Proof state after:
no goals
Theorem: List.Index.pi_eq_iff_eq_unpi
Proof state before:
case mpr
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
⊢ h = k.unpi → pi h = k
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h✝ : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
h : h✝ = k.unpi
⊢ pi h✝ = k
Theorem: List.Index.pi_eq_iff_eq_unpi
Proof state before:
case mpr
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
xs : List α
h✝ : (i : xs.Index) → (f i.val).Index
k : (List.pi f xs).Index
h : h✝ = k.unpi
⊢ pi h✝ = k
Tactic:
rw [h, pi_unpi]
Proof state after:
no goals
Theorem: List.Index.unpi_eq_iff_eq_pi
Proof state before:
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h : (i : xs.Index) → (f i.val).Index
⊢ k.unpi = h ↔ k = pi h
Tactic:
constructor
Proof state after:
case mp
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h : (i : xs.Index) → (f i.val).Index
⊢ k.unpi = h → k = pi h

case mpr
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h : (i : xs.Index) → (f i.val).Index
⊢ k = pi h → k.unpi = h
Theorem: List.Index.unpi_eq_iff_eq_pi
Proof state before:
case mp
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h : (i : xs.Index) → (f i.val).Index
⊢ k.unpi = h → k = pi h
Tactic:
intro h
Proof state after:
case mp
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h✝ : (i : xs.Index) → (f i.val).Index
h : k.unpi = h✝
⊢ k = pi h✝
Theorem: List.Index.unpi_eq_iff_eq_pi
Proof state before:
case mp
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h✝ : (i : xs.Index) → (f i.val).Index
h : k.unpi = h✝
⊢ k = pi h✝
Tactic:
rw [←h, pi_unpi]
Proof state after:
no goals
Theorem: List.Index.unpi_eq_iff_eq_pi
Proof state before:
case mpr
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h : (i : xs.Index) → (f i.val).Index
⊢ k = pi h → k.unpi = h
Tactic:
intro h
Proof state after:
case mpr
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h✝ : (i : xs.Index) → (f i.val).Index
h : k = pi h✝
⊢ k.unpi = h✝
Theorem: List.Index.unpi_eq_iff_eq_pi
Proof state before:
case mpr
α : Type u_2
β : α → Type u_1
f : (x : α) → List (β x)
xs : List α
k : (List.pi f xs).Index
h✝ : (i : xs.Index) → (f i.val).Index
h : k = pi h✝
⊢ k.unpi = h✝
Tactic:
rw [h, unpi_pi]
Proof state after:
no goals