internlm/Lean-Github huggingface dataset:
Theorem: Equiv.rev_fwd
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
x : α
⊢ e.rev (e.fwd x) = x
Tactic:
rw [←Equiv.fwd_eq_iff_rev_eq]
Proof state after:
no goals
Theorem: Equiv.ext
Proof state before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
⊢ e₁ = e₂
Tactic:
have h' : e₁.rev = e₂.rev := by funext; rw [← fwd_eq_iff_rev_eq, h, fwd_rev]
Proof state after:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
h' : e₁.rev = e₂.rev
⊢ e₁ = e₂
Theorem: Equiv.ext
Proof state before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
h' : e₁.rev = e₂.rev
⊢ e₁ = e₂
Tactic:
match e₁, e₂ with | ⟨_,_,_⟩, ⟨_,_,_⟩ => cases h; cases h'; rfl
Proof state after:
no goals
Theorem: Equiv.ext
Proof state before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
⊢ e₁.rev = e₂.rev
Tactic:
funext
Proof state after:
case h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
x✝ : β
⊢ e₁.rev x✝ = e₂.rev x✝
Theorem: Equiv.ext
Proof state before:
case h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : e₁.fwd = e₂.fwd
x✝ : β
⊢ e₁.rev x✝ = e₂.rev x✝
Tactic:
rw [← fwd_eq_iff_rev_eq, h, fwd_rev]
Proof state after:
no goals
Theorem: Equiv.ext
Proof state before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝¹ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝¹ x = y ↔ rev✝¹ y = x
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h :
  { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.fwd =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.fwd
h' :
  { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝¹, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
cases h
Proof state after:
case refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝¹ y = x
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h' :
  { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Theorem: Equiv.ext
Proof state before:
case refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝¹ : β → α
fwd_eq_iff_rev_eq✝¹ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝¹ y = x
rev✝ : β → α
fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
h' :
  { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ }.rev =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }.rev
⊢ { fwd := fwd✝, rev := rev✝¹, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
cases h'
Proof state after:
case refl.refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝¹ fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
⊢ { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Theorem: Equiv.ext
Proof state before:
case refl.refl
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
fwd✝ : α → β
rev✝ : β → α
fwd_eq_iff_rev_eq✝¹ fwd_eq_iff_rev_eq✝ : ∀ {x : α} {y : β}, fwd✝ x = y ↔ rev✝ y = x
⊢ { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝¹ } =
    { fwd := fwd✝, rev := rev✝, fwd_eq_iff_rev_eq := fwd_eq_iff_rev_eq✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.ext'
Proof state before:
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
⊢ e₁ = e₂
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
x✝ : α
⊢ e₁.fwd x✝ = e₂.fwd x✝
Theorem: Equiv.ext'
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e₁ e₂ : Equiv α β
h : ∀ (x : α), e₁.fwd x = e₂.fwd x
x✝ : α
⊢ e₁.fwd x✝ = e₂.fwd x✝
Tactic:
exact h ..
Proof state after:
no goals
Theorem: Equiv.comp_assoc
Proof state before:
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
⊢ (g.comp f).comp e = g.comp (f.comp e)
Tactic:
ext
Proof state after:
case h.h
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
x✝ : α
⊢ ((g.comp f).comp e).fwd x✝ = (g.comp (f.comp e)).fwd x✝
Theorem: Equiv.comp_assoc
Proof state before:
case h.h
γ : Sort u_1
δ : Sort u_2
β : Sort u_3
α : Sort u_4
g : Equiv γ δ
f : Equiv β γ
e : Equiv α β
x✝ : α
⊢ ((g.comp f).comp e).fwd x✝ = (g.comp (f.comp e)).fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.comp_id_right
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
⊢ e.comp Equiv.id = e
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.comp Equiv.id).fwd x✝ = e.fwd x✝
Theorem: Equiv.comp_id_right
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.comp Equiv.id).fwd x✝ = e.fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.comp_id_left
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
⊢ e.comp Equiv.id = e
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.comp Equiv.id).fwd x✝ = e.fwd x✝
Theorem: Equiv.comp_id_left
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.comp Equiv.id).fwd x✝ = e.fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.comp_inv_right
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
⊢ e.comp e.inv = Equiv.id
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : β
⊢ (e.comp e.inv).fwd x✝ = Equiv.id.fwd x✝
Theorem: Equiv.comp_inv_right
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : β
⊢ (e.comp e.inv).fwd x✝ = Equiv.id.fwd x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.comp_inv_left
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
⊢ e.inv.comp e = Equiv.id
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.inv.comp e).fwd x✝ = Equiv.id.fwd x✝
Theorem: Equiv.comp_inv_left
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ (e.inv.comp e).fwd x✝ = Equiv.id.fwd x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.inv_id
Proof state before:
α : Sort u_1
⊢ Equiv.id.inv = Equiv.id
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
x✝ : α
⊢ Equiv.id.inv.fwd x✝ = Equiv.id.fwd x✝
Theorem: Equiv.inv_id
Proof state before:
case h.h
α : Sort u_1
x✝ : α
⊢ Equiv.id.inv.fwd x✝ = Equiv.id.fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.inv_inv
Proof state before:
α : Sort u_1
β : Sort u_2
e : Equiv α β
⊢ e.inv.inv = e
Tactic:
ext
Proof state after:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ e.inv.inv.fwd x✝ = e.fwd x✝
Theorem: Equiv.inv_inv
Proof state before:
case h.h
α : Sort u_1
β : Sort u_2
e : Equiv α β
x✝ : α
⊢ e.inv.inv.fwd x✝ = e.fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Equiv.inv_comp
Proof state before:
β : Sort u_1
γ : Sort u_2
α : Sort u_3
f : Equiv β γ
e : Equiv α β
⊢ (f.comp e).inv = e.inv.comp f.inv
Tactic:
ext
Proof state after:
case h.h
β : Sort u_1
γ : Sort u_2
α : Sort u_3
f : Equiv β γ
e : Equiv α β
x✝ : γ
⊢ (f.comp e).inv.fwd x✝ = (e.inv.comp f.inv).fwd x✝
Theorem: Equiv.inv_comp
Proof state before:
case h.h
β : Sort u_1
γ : Sort u_2
α : Sort u_3
f : Equiv β γ
e : Equiv α β
x✝ : γ
⊢ (f.comp e).inv.fwd x✝ = (e.inv.comp f.inv).fwd x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.recPush_push
Proof state before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)
Tactic:
let _ : Inhabited α := ⟨(xs.push x)[0]⟩
Proof state after:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)
Theorem: Array.recPush_push
Proof state before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush empty push (xs.push x) = push xs x (recPush empty push xs)
Tactic:
rw [recPush]
Proof state after:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = push xs x (recPush empty push xs)
Theorem: Array.recPush_push
Proof state before:
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = push xs x (recPush empty push xs)
Tactic:
trans (recPush.aux empty push (xs.push x) (xs.size + 1) (size_push xs x))
Proof state after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = recPush.aux empty push (xs.push x) (xs.size + 1) ⋯

case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.size + 1) ⋯ = push xs x (recPush empty push xs)
Theorem: Array.recPush_push
Proof state before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.push x).size ⋯ = recPush.aux empty push (xs.push x) (xs.size + 1) ⋯
Tactic:
congr
Proof state after:
case a.e_n
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).size = xs.size + 1
Theorem: Array.recPush_push
Proof state before:
case a.e_n
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).size = xs.size + 1
Tactic:
exact size_push ..
Proof state after:
no goals
Theorem: Array.recPush_push
Proof state before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ recPush.aux empty push (xs.push x) (xs.size + 1) ⋯ = push xs x (recPush empty push xs)
Tactic:
rw [recPush.aux]
Proof state after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (let_fun this := ⋯;
    let_fun x_1 := { default := (xs.push x)[0] };
    ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯)) =
    push xs x (recPush empty push xs)
Theorem: Array.recPush_push
Proof state before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (let_fun this := ⋯;
    let_fun x_1 := { default := (xs.push x)[0] };
    ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯)) =
    push xs x (recPush empty push xs)
Tactic:
simp
Proof state after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯) =
    push xs x (recPush empty push xs)
Theorem: Array.recPush_push
Proof state before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ ⋯ ▸ push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯) =
    push xs x (recPush empty push xs)
Tactic:
elim_cast
Proof state after:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq (push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯))
    (push xs x (recPush empty push xs))
Theorem: Array.recPush_push
Proof state before:
case a
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq (push (xs.push x).pop (xs.push x).back (recPush.aux empty push (xs.push x).pop xs.size ⋯))
    (push xs x (recPush empty push xs))
Tactic:
congr
Proof state after:
case a.e_1
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs

case a.e_2
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).back = x

case a.e_3.e_5.h
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs

case a.e_3.e_7
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq ⋯ ⋯
Theorem: Array.recPush_push
Proof state before:
case a.e_1
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs
Tactic:
exact pop_push ..
Proof state after:
no goals
Theorem: Array.recPush_push
Proof state before:
case a.e_2
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).back = x
Tactic:
exact back_push ..
Proof state after:
no goals
Theorem: Array.recPush_push
Proof state before:
case a.e_3.e_5.h
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ (xs.push x).pop = xs
Tactic:
exact pop_push ..
Proof state after:
no goals
Theorem: Array.recPush_push
Proof state before:
case a.e_3.e_7
α : Type u_1
motive : Array α → Sort u_2
empty : motive #[]
push : (xs : Array α) → (x : α) → motive xs → motive (xs.push x)
xs : Array α
x : α
x✝ : Inhabited α := { default := (xs.push x)[0] }
⊢ HEq ⋯ ⋯
Tactic:
exact proof_irrel_heq ..
Proof state after:
no goals
Theorem: List.Index.unjoin_join
Proof state before:
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
induction xss with
| nil => cases i; contradiction
| cons xs xss ih =>
  match i with
  | ⟨head, _⟩ => simp only [join, unjoin, unappend_append]
  | ⟨tail _, _⟩ => simp only [join, unjoin, unappend_append]; rw [ih]
Proof state after:
no goals
Theorem: List.Index.unjoin_join
Proof state before:
case nil
α✝ : Type u_1
i : (i : [].Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
cases i
Proof state after:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).unjoin = ⟨fst✝, snd✝⟩
Theorem: List.Index.unjoin_join
Proof state before:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).unjoin = ⟨fst✝, snd✝⟩
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.unjoin_join
Proof state before:
case cons
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
match i with
| ⟨head, _⟩ => simp only [join, unjoin, unappend_append]
| ⟨tail _, _⟩ => simp only [join, unjoin, unappend_append]; rw [ih]
Proof state after:
no goals
Theorem: List.Index.unjoin_join
Proof state before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
snd✝ : head.val.Index
⊢ (join ⟨head, snd✝⟩).unjoin = ⟨head, snd✝⟩
Tactic:
simp only [join, unjoin, unappend_append]
Proof state after:
no goals
Theorem: List.Index.unjoin_join
Proof state before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ (join ⟨a✝.tail, snd✝⟩).unjoin = ⟨a✝.tail, snd✝⟩
Tactic:
simp only [join, unjoin, unappend_append]
Proof state after:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ ⟨(join ⟨a✝, snd✝⟩).unjoin.fst.tail, (join ⟨a✝, snd✝⟩).unjoin.snd⟩ = ⟨a✝.tail, snd✝⟩
Theorem: List.Index.unjoin_join
Proof state before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ ⟨(join ⟨a✝, snd✝⟩).unjoin.fst.tail, (join ⟨a✝, snd✝⟩).unjoin.snd⟩ = ⟨a✝.tail, snd✝⟩
Tactic:
rw [ih]
Proof state after:
no goals
Theorem: List.Index.join_unjoin
Proof state before:
α : Type u_1
xss : List (List α)
k : xss.join.Index
⊢ join k.unjoin = k
Tactic:
induction xss with
| nil => contradiction
| cons xs xss ih =>
  match h : unappend k with
  | .inl j => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join]
  | .inr k => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join, ih]
Proof state after:
no goals
Theorem: List.Index.join_unjoin
Proof state before:
case nil
α : Type u_1
k : [].join.Index
⊢ join k.unjoin = k
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.Index.join_unjoin
Proof state before:
case cons
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
⊢ join k.unjoin = k
Tactic:
match h : unappend k with
| .inl j => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join]
| .inr k => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join, ih]
Proof state after:
no goals
Theorem: List.Index.join_unjoin
Proof state before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k.unappend = Sum.inl j
⊢ join k.unjoin = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k = append (Sum.inl j)
⊢ join k.unjoin = k
Theorem: List.Index.join_unjoin
Proof state before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k = append (Sum.inl j)
⊢ join k.unjoin = k
Tactic:
rw [h, unjoin, unappend_append, join]
Proof state after:
no goals
Theorem: List.Index.join_unjoin
Proof state before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝.unappend = Sum.inr k
⊢ join k✝.unjoin = k✝
Tactic:
rw [unappend_eq_iff_eq_append] at h
Proof state after:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝ = append (Sum.inr k)
⊢ join k✝.unjoin = k✝
Theorem: List.Index.join_unjoin
Proof state before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝ = append (Sum.inr k)
⊢ join k✝.unjoin = k✝
Tactic:
rw [h, unjoin, unappend_append, join, ih]
Proof state after:
no goals
Theorem: List.Index.join_eq_iff_eq_unjoin
Proof state before:
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
⊢ join i = k ↔ i = k.unjoin
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
⊢ join i = k → i = k.unjoin

case mpr
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
⊢ i = k.unjoin → join i = k
Theorem: List.Index.join_eq_iff_eq_unjoin
Proof state before:
case mp
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
⊢ join i = k → i = k.unjoin
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
h : join i = k
⊢ i = k.unjoin
Theorem: List.Index.join_eq_iff_eq_unjoin
Proof state before:
case mp
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
h : join i = k
⊢ i = k.unjoin
Tactic:
rw [←h, unjoin_join]
Proof state after:
no goals
Theorem: List.Index.join_eq_iff_eq_unjoin
Proof state before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
⊢ i = k.unjoin → join i = k
Tactic:
intro h
Proof state after:
case mpr
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
h : i = k.unjoin
⊢ join i = k
Theorem: List.Index.join_eq_iff_eq_unjoin
Proof state before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
k : xss.join.Index
h : i = k.unjoin
⊢ join i = k
Tactic:
rw [h, join_unjoin]
Proof state after:
no goals
Theorem: List.Index.unjoin_eq_iff_eq_join
Proof state before:
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i ↔ k = join i
Tactic:
constructor
Proof state after:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i → k = join i

case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k = join i → k.unjoin = i
Theorem: List.Index.unjoin_eq_iff_eq_join
Proof state before:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i → k = join i
Tactic:
intro h
Proof state after:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k.unjoin = i
⊢ k = join i
Theorem: List.Index.unjoin_eq_iff_eq_join
Proof state before:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k.unjoin = i
⊢ k = join i
Tactic:
rw [←h, join_unjoin]
Proof state after:
no goals