Theorem: BishopFin.count_split (Fifteen/Logic/BishopFin.lean)

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count p = (count fun a => p a ∧ q a) + count fun a => p a ∧ ¬q a
Tactic:
conv =>
  lhs
  rewrite [count_eq_card, card_eq_count_add_count_not (q ∘ Subtype.val)]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count (q ∘ Subtype.val) + count fun a => ¬(q ∘ Subtype.val) a) =
    (count fun a => p a ∧ q a) + count fun a => p a ∧ ¬q a

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count (q ∘ Subtype.val) + count fun a => ¬(q ∘ Subtype.val) a) =
    (count fun a => p a ∧ q a) + count fun a => p a ∧ ¬q a
Tactic:
refine congr (congrArg _ ?_) ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count (q ∘ Subtype.val) = count fun a => p a ∧ q a

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => ¬(q ∘ Subtype.val) a) = count fun a => p a ∧ ¬q a

State before:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count (q ∘ Subtype.val) = count fun a => p a ∧ q a

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => ¬(q ∘ Subtype.val) a) = count fun a => p a ∧ ¬q a
Tactic:
all_goals (
  simp only [count_eq_card]
  apply card_eq_card_of_bij fun x => ⟨x.1.1, x.1.2, x.2⟩
  . intro y; exact ⟨⟨⟨y.1,y.2.1⟩,y.2.2⟩,rfl⟩
  . intro x₁ x₂
    simp only [Subtype.mk.injEq]
    exact Subtype.eq ∘ Subtype.eq
)
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => ¬(q ∘ Subtype.val) a) = count fun a => p a ∧ ¬q a
Tactic:
(
simp only [count_eq_card]
apply card_eq_card_of_bij fun x => ⟨x.1.1, x.1.2, x.2⟩
. intro y; exact ⟨⟨⟨y.1,y.2.1⟩,y.2.2⟩,rfl⟩
. intro x₁ x₂
simp only [Subtype.mk.injEq]
exact Subtype.eq ∘ Subtype.eq
)
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => ¬(q ∘ Subtype.val) a) = count fun a => p a ∧ ¬q a
Tactic:
simp only [count_eq_card]
State after:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card { a // ¬(q ∘ Subtype.val) a } = card { a // p a ∧ ¬q a }

State before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card { a // ¬(q ∘ Subtype.val) a } = card { a // p a ∧ ¬q a }
Tactic:
apply card_eq_card_of_bij fun x => ⟨x.1.1, x.1.2, x.2⟩
State after:
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (b : { a // p a ∧ ¬q a }), ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = b

case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂

State before:
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (b : { a // p a ∧ ¬q a }), ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = b

case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂
Tactic:
. intro y; exact ⟨⟨⟨y.1,y.2.1⟩,y.2.2⟩,rfl⟩
State after:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂

State before:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂
Tactic:
. intro x₁ x₂
  simp only [Subtype.mk.injEq]
  exact Subtype.eq ∘ Subtype.eq
State after:
no goals

State before:
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (b : { a // p a ∧ ¬q a }), ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = b
Tactic:
intro y
State after:
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
y : { a // p a ∧ ¬q a }
⊢ ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = y

State before:
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
y : { a // p a ∧ ¬q a }
⊢ ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = y
Tactic:
exact ⟨⟨⟨y.1,y.2.1⟩,y.2.2⟩,rfl⟩
State after:
no goals

State before:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂
Tactic:
intro x₁ x₂
State after:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
x₁ x₂ : { a // ¬(q ∘ Subtype.val) a }
⊢ { val := x₁.val.val, property := (_ : p x₁.val.val ∧ ¬q x₁.val.val) } =
      { val := x₂.val.val, property := (_ : p x₂.val.val ∧ ¬q x₂.val.val) } →
    x₁ = x₂

State before:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
x₁ x₂ : { a // ¬(q ∘ Subtype.val) a }
⊢ { val := x₁.val.val, property := (_ : p x₁.val.val ∧ ¬q x₁.val.val) } =
      { val := x₂.val.val, property := (_ : p x₂.val.val ∧ ¬q x₂.val.val) } →
    x₁ = x₂
Tactic:
simp only [Subtype.mk.injEq]
State after:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
x₁ x₂ : { a // ¬(q ∘ Subtype.val) a }
⊢ x₁.val.val = x₂.val.val → x₁ = x₂

State before:
case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
x₁ x₂ : { a // ¬(q ∘ Subtype.val) a }
⊢ x₁.val.val = x₂.val.val → x₁ = x₂
Tactic:
exact Subtype.eq ∘ Subtype.eq
State after:
no goals