Theorem: Permutation.get_comp (Fifteen/Data/Permutation/Basic.lean)

State before:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (comp x y)[i] = x[↑y[i]]
Tactic:
dsimp [comp]
State after:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (ofFn (fun i => x[↑y[↑i]]) (_ : ∀ (i j : Fin n), (fun i => x[↑y[↑i]]) i = (fun i => x[↑y[↑i]]) j → i = j))[i] =
    x[↑y[i]]

State before:
n : Nat
x y : Permutation n
i : Nat
h : i < n
⊢ (ofFn (fun i => x[↑y[↑i]]) (_ : ∀ (i j : Fin n), (fun i => x[↑y[↑i]]) i = (fun i => x[↑y[↑i]]) j → i = j))[i] =
    x[↑y[i]]
Tactic:
exact get_ofFn ..
State after:
no goals