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

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

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

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

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

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