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

State before:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.count fun t => ↑t.fst < ↑t.snd ∧ ↑x[↑t.fst] > ↑x[↑t.snd]
Tactic:
rewrite [BishopFin.count_eq_card]
State after:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.card { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

State before:
n : Nat
x : Permutation n
⊢ BishopFin.card (Inversion x) = BishopFin.card { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
Tactic:
refine BishopFin.card_eq_card_of_bij ?_ ?_ ?_
State after:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }), ∃ a, ?refine_1 a = b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x), ?refine_1 a₁ = ?refine_1 a₂ → a₁ = a₂

State before:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }

case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }), ∃ a, ?refine_1 a = b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x), ?refine_1 a₁ = ?refine_1 a₂ → a₁ = a₂
Tactic:
. exact fun iv => ⟨⟨iv.1,iv.2⟩, iv.3, iv.4⟩
State after:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂

State before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b

case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
. intro t; exact ⟨⟨t.1.1, t.1.2, t.2.1, t.2.2⟩, rfl⟩
State after:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂

State before:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
. intro iv₁ iv₂
  simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
  intro hfst hsnd
  cases iv₁; cases iv₂; cases hfst; cases hsnd; rfl
State after:
no goals

State before:
case refine_1
n : Nat
x : Permutation n
⊢ Inversion x → { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
Tactic:
exact fun iv => ⟨⟨iv.1,iv.2⟩, iv.3, iv.4⟩
State after:
no goals

State before:
case refine_2
n : Nat
x : Permutation n
⊢ ∀ (b : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }),
    ∃ a,
      { val := (a.fst, a.snd),
          property :=
            (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
        b
Tactic:
intro t
State after:
case refine_2
n : Nat
x : Permutation n
t : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
⊢ ∃ a,
    { val := (a.fst, a.snd),
        property :=
          (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
      t

State before:
case refine_2
n : Nat
x : Permutation n
t : { a // ↑a.fst < ↑a.snd ∧ ↑x[↑a.fst] > ↑x[↑a.snd] }
⊢ ∃ a,
    { val := (a.fst, a.snd),
        property :=
          (_ : ↑(a.fst, a.snd).fst < ↑(a.fst, a.snd).snd ∧ ↑x[↑(a.fst, a.snd).fst] > ↑x[↑(a.fst, a.snd).snd]) } =
      t
Tactic:
exact ⟨⟨t.1.1, t.1.2, t.2.1, t.2.2⟩, rfl⟩
State after:
no goals

State before:
case refine_3
n : Nat
x : Permutation n
⊢ ∀ (a₁ a₂ : Inversion x),
    { val := (a₁.fst, a₁.snd),
          property :=
            (_ :
              ↑(a₁.fst, a₁.snd).fst < ↑(a₁.fst, a₁.snd).snd ∧ ↑x[↑(a₁.fst, a₁.snd).fst] > ↑x[↑(a₁.fst, a₁.snd).snd]) } =
        { val := (a₂.fst, a₂.snd),
          property :=
            (_ :
              ↑(a₂.fst, a₂.snd).fst < ↑(a₂.fst, a₂.snd).snd ∧ ↑x[↑(a₂.fst, a₂.snd).fst] > ↑x[↑(a₂.fst, a₂.snd).snd]) } →
      a₁ = a₂
Tactic:
intro iv₁ iv₂
State after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ { val := (iv₁.fst, iv₁.snd),
        property :=
          (_ :
            ↑(iv₁.fst, iv₁.snd).fst < ↑(iv₁.fst, iv₁.snd).snd ∧
              ↑x[↑(iv₁.fst, iv₁.snd).fst] > ↑x[↑(iv₁.fst, iv₁.snd).snd]) } =
      { val := (iv₂.fst, iv₂.snd),
        property :=
          (_ :
            ↑(iv₂.fst, iv₂.snd).fst < ↑(iv₂.fst, iv₂.snd).snd ∧
              ↑x[↑(iv₂.fst, iv₂.snd).fst] > ↑x[↑(iv₂.fst, iv₂.snd).snd]) } →
    iv₁ = iv₂

State before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ { val := (iv₁.fst, iv₁.snd),
        property :=
          (_ :
            ↑(iv₁.fst, iv₁.snd).fst < ↑(iv₁.fst, iv₁.snd).snd ∧
              ↑x[↑(iv₁.fst, iv₁.snd).fst] > ↑x[↑(iv₁.fst, iv₁.snd).snd]) } =
      { val := (iv₂.fst, iv₂.snd),
        property :=
          (_ :
            ↑(iv₂.fst, iv₂.snd).fst < ↑(iv₂.fst, iv₂.snd).snd ∧
              ↑x[↑(iv₂.fst, iv₂.snd).fst] > ↑x[↑(iv₂.fst, iv₂.snd).snd]) } →
    iv₁ = iv₂
Tactic:
simp only [Subtype.mk.injEq, Prod.mk.injEq, and_imp]
State after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = iv₂

State before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
⊢ iv₁.fst = iv₂.fst → iv₁.snd = iv₂.snd → iv₁ = iv₂
Tactic:
intro hfst hsnd
State after:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
hfst : iv₁.fst = iv₂.fst
hsnd : iv₁.snd = iv₂.snd
⊢ iv₁ = iv₂

State before:
case refine_3
n : Nat
x : Permutation n
iv₁ iv₂ : Inversion x
hfst : iv₁.fst = iv₂.fst
hsnd : iv₁.snd = iv₂.snd
⊢ iv₁ = iv₂
Tactic:
cases iv₁
State after:
case refine_3.mk
n : Nat
x : Permutation n
iv₂ : Inversion x
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst = iv₂.fst
hsnd : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd = iv₂.snd
⊢ { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ } = iv₂

State before:
case refine_3.mk
n : Nat
x : Permutation n
iv₂ : Inversion x
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst = iv₂.fst
hsnd : { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd = iv₂.snd
⊢ { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ } = iv₂
Tactic:
cases iv₂
State after:
case refine_3.mk.mk
n : Nat
x : Permutation n
fst✝¹ snd✝¹ : Fin n
lt✝¹ : fst✝¹ < snd✝¹
inverted✝¹ : x[↑fst✝¹] > x[↑snd✝¹]
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.fst =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst
hsnd :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }

State before:
case refine_3.mk.mk
n : Nat
x : Permutation n
fst✝¹ snd✝¹ : Fin n
lt✝¹ : fst✝¹ < snd✝¹
inverted✝¹ : x[↑fst✝¹] > x[↑snd✝¹]
fst✝ snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hfst :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.fst =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.fst
hsnd :
  { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
cases hfst
State after:
case refine_3.mk.mk.refl
n : Nat
x : Permutation n
fst✝ snd✝¹ : Fin n
lt✝¹ : fst✝ < snd✝¹
inverted✝¹ : x[↑fst✝] > x[↑snd✝¹]
snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hsnd :
  { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }

State before:
case refine_3.mk.mk.refl
n : Nat
x : Permutation n
fst✝ snd✝¹ : Fin n
lt✝¹ : fst✝ < snd✝¹
inverted✝¹ : x[↑fst✝] > x[↑snd✝¹]
snd✝ : Fin n
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
hsnd :
  { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ }.snd =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
cases hsnd
State after:
case refine_3.mk.mk.refl.refl
n : Nat
x : Permutation n
fst✝ snd✝ : Fin n
lt✝¹ : fst✝ < snd✝
inverted✝¹ : x[↑fst✝] > x[↑snd✝]
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
⊢ { fst := fst✝, snd := snd✝, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }

State before:
case refine_3.mk.mk.refl.refl
n : Nat
x : Permutation n
fst✝ snd✝ : Fin n
lt✝¹ : fst✝ < snd✝
inverted✝¹ : x[↑fst✝] > x[↑snd✝]
lt✝ : fst✝ < snd✝
inverted✝ : x[↑fst✝] > x[↑snd✝]
⊢ { fst := fst✝, snd := snd✝, lt := lt✝¹, inverted := inverted✝¹ } =
    { fst := fst✝, snd := snd✝, lt := lt✝, inverted := inverted✝ }
Tactic:
rfl
State after:
no goals