Theorem: List.Index.sigma_eq_iff_eq_unsigma (Extra/Index/Sigma.lean)

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

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

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

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

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

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

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