Theorem: List1.toList1_eq_iff_toIndView_eq (GMLInit/Data/List/List1.lean)

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ (IndView.pure x).toList1 = List1.cons y [] ↔ (List1.cons y []).toIndView = IndView.pure x
Tactic:
unfold IndView.toList1 toIndView
State after:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] ↔ IndView.pure y = IndView.pure x

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] ↔ IndView.pure y = IndView.pure x
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] → IndView.pure y = IndView.pure x

case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ IndView.pure y = IndView.pure x → List1.cons x [] = List1.cons y []

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ List1.cons x [] = List1.cons y [] → IndView.pure y = IndView.pure x
Tactic:
intro | rfl => rfl
State after:
no goals

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
x✝ : List1.cons x [] = List1.cons y []
⊢ IndView.pure x = IndView.pure x
Tactic:
rfl
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
⊢ IndView.pure y = IndView.pure x → List1.cons x [] = List1.cons y []
Tactic:
intro | rfl => rfl
State after:
no goals

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y : α
x✝ : IndView.pure y = IndView.pure x
⊢ List1.cons y [] = List1.cons y []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ (IndView.pure x).toList1 = List1.cons y (head✝ :: tail✝) ↔ (List1.cons y (head✝ :: tail✝)).toIndView = IndView.pure x
Tactic:
unfold IndView.toList1 toIndView
State after:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) ↔ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

State before:
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) ↔ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) → IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x → List1.cons x [] = List1.cons y (head✝ :: tail✝)

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝) → IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : List1.cons x [] = List1.cons y (head✝ :: tail✝)
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : List1.cons x [] = List1.cons y (head✝ :: tail✝)
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
injection h with h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : [x] = y :: head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
h : [x] = y :: head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
injection h with hh ht
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
hh : x = y
ht : [] = head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
hh : x = y
ht : [] = head✝ :: tail✝
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
Tactic:
contradiction
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x → List1.cons x [] = List1.cons y (head✝ :: tail✝)
Tactic:
intro
State after:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
a✝ : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝)

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs : List1.IndView α
ys : List1 α
x y head✝ : α
tail✝ : List α
a✝ : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.pure x
⊢ List1.cons x [] = List1.cons y (head✝ :: tail✝)
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ (IndView.cons x xs).toList1 = List1.cons y [] ↔ (List1.cons y []).toIndView = IndView.cons x xs
Tactic:
unfold IndView.toList1 toIndView
State after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] ↔ IndView.pure y = IndView.cons x xs

State before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] ↔ IndView.pure y = IndView.cons x xs
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] → IndView.pure y = IndView.cons x xs

case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ IndView.pure y = IndView.cons x xs → List1.cons x xs.toList1.toList = List1.cons y []

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ List1.cons x xs.toList1.toList = List1.cons y [] → IndView.pure y = IndView.cons x xs
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : List1.cons x xs.toList1.toList = List1.cons y []
⊢ IndView.pure y = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : List1.cons x xs.toList1.toList = List1.cons y []
⊢ IndView.pure y = IndView.cons x xs
Tactic:
injection h with h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : x :: xs.toList1.toList = [y]
⊢ IndView.pure y = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
h : x :: xs.toList1.toList = [y]
⊢ IndView.pure y = IndView.cons x xs
Tactic:
injection h with hh ht
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ IndView.pure y = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ IndView.pure y = IndView.cons x xs
Tactic:
absurd ht
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ ¬xs.toList1.toList = []

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
hh : x = y
ht : xs.toList1.toList = []
⊢ ¬xs.toList1.toList = []
Tactic:
exact List1.ne_nil xs.toList1
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
⊢ IndView.pure y = IndView.cons x xs → List1.cons x xs.toList1.toList = List1.cons y []
Tactic:
intro
State after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
a✝ : IndView.pure y = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y []

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y : α
a✝ : IndView.pure y = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y []
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ (IndView.cons x xs).toList1 = List1.cons y (head✝ :: tail✝) ↔
    (List1.cons y (head✝ :: tail✝)).toIndView = IndView.cons x xs
Tactic:
unfold IndView.toList1 toIndView
State after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (head✝ :: tail✝) ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (head✝ :: tail✝) ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
rw [←cons_toList]
State after:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList ↔
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList →
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs →
    List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList →
    IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
injection h with h
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : x :: xs.toList1.toList = y :: (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : x :: xs.toList1.toList = y :: (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
injection h with hh ht
State after:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : x = y
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
case mp
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : x = y
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
cases hh
State after:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : xs.toList1.toList = (List1.cons head✝ tail✝).toList
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
have ht := List1.eq ht
State after:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs

State before:
case mp.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ IndView.cons x (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
Tactic:
congr
State after:
case mp.refl.e_a
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ (List1.cons head✝ tail✝).toIndView = xs

State before:
case mp.refl.e_a
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht✝ : xs.toList1.toList = (List1.cons head✝ tail✝).toList
ht : xs.toList1 = List1.cons head✝ tail✝
⊢ (List1.cons head✝ tail✝).toIndView = xs
Tactic:
exact toList1_eq_iff_toIndView_eq.mp ht
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
⊢ IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs →
    List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
intro h
State after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
h : IndView.cons y (List1.cons head✝ tail✝).toIndView = IndView.cons x xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
injection h with hh ht
State after:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : y = x
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList

State before:
case mpr
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
y head✝ : α
tail✝ : List α
hh : y = x
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons y (List1.cons head✝ tail✝).toList
Tactic:
cases hh
State after:
case mpr.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons x (List1.cons head✝ tail✝).toList

State before:
case mpr.refl
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ List1.cons x xs.toList1.toList = List1.cons x (List1.cons head✝ tail✝).toList
Tactic:
congr
State after:
case mpr.refl.e_xs.e_self
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ xs.toList1 = List1.cons head✝ tail✝

State before:
case mpr.refl.e_xs.e_self
α : Type u_1
β : Type ?u.8604
xs✝ : List1.IndView α
ys : List1 α
x : α
xs : List1.IndView α
head✝ : α
tail✝ : List α
ht : (List1.cons head✝ tail✝).toIndView = xs
⊢ xs.toList1 = List1.cons head✝ tail✝
Tactic:
exact toList1_eq_iff_toIndView_eq.mpr ht
State after:
no goals