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

State before:
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i ↔ k = sigma i
Tactic:
constructor
State after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i → k = sigma i

case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k = sigma i → k.unsigma = i

State before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k.unsigma = i → k = sigma i
Tactic:
intro h
State after:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k.unsigma = i
⊢ k = sigma i

State before:
case mp
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k.unsigma = i
⊢ k = sigma i
Tactic:
cases h
State after:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ k = sigma k.unsigma

State before:
case mp.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
⊢ k = sigma k.unsigma
Tactic:
rw [sigma_unsigma]
State after:
no goals

State before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
⊢ k = sigma i → k.unsigma = i
Tactic:
intro h
State after:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k = sigma i
⊢ k.unsigma = i

State before:
case mpr
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
k : (xs.sigma f).Index
i : (i : xs.Index) × (f i.val).Index
h : k = sigma i
⊢ k.unsigma = i
Tactic:
cases h
State after:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).unsigma = i

State before:
case mpr.refl
α : Type u_1
xs : List α
β : α → Type u_2
f : (x : α) → List (β x)
i : (i : xs.Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
rw [unsigma_sigma]
State after:
no goals