Theorem: List.Index.unpi_eq_iff_eq_pi (Extra/Index/Pi.lean)

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
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

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
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✝

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]
State after:
no goals

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
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✝

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]
State after:
no goals