Theorem: Permutation.Inversion.card_eq_of_mul (Fifteen/Data/Permutation/Inversion.lean)

State before:
n : Nat
x y : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Tactic:
rewrite [Inversion.card_eq x]
State after:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]

State before:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑(x * y)[↑t.fst] > ↑(x * y)[↑t.snd]
Tactic:
simp only [get_mul]
State after:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑x[↑y[↑t.fst]] > ↑x[↑y[↑t.snd]]

State before:
n : Nat
x y : Permutation n
⊢ (BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]) =
    BishopFin.count fun t => ↑y[↑t.fst] < ↑y[↑t.snd] ∧ ↑x[↑y[↑t.fst]] > ↑x[↑y[↑t.snd]]
Tactic:
refine BishopFin.count_eq_count_invimage_of_inv (Prod.map y.toFun y.toFun) (Prod.map y.inv.toFun y.inv.toFun) ?_ ?_
State after:
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b

case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a

State before:
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b

case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
. simp only [Prod.map, toFun_inv_toFun, implies_true]
State after:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a

State before:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
. simp only [Prod.map, toFun_toFun_inv, implies_true]
State after:
no goals

State before:
case refine_1
n : Nat
x y : Permutation n
⊢ ∀ (b : Fin n × Fin n), Prod.map (toFun (inv y)) (toFun (inv y)) (Prod.map (toFun y) (toFun y) b) = b
Tactic:
simp only [Prod.map, toFun_inv_toFun, implies_true]
State after:
no goals

State before:
case refine_2
n : Nat
x y : Permutation n
⊢ ∀ (a : Fin n × Fin n), Prod.map (toFun y) (toFun y) (Prod.map (toFun (inv y)) (toFun (inv y)) a) = a
Tactic:
simp only [Prod.map, toFun_toFun_inv, implies_true]
State after:
no goals