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

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ count p = count (p ∘ Subtype.val)
Tactic:
iterate rewrite [count_eq_card]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = card { a // (p ∘ Subtype.val) a }

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = card { a // (p ∘ Subtype.val) a }
Tactic:
refine card_eq_card_of_inv ?f ?g ?hgf ?hfg
State after:
case f
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // p a } → { a // (p ∘ Subtype.val) a }

case g
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // (p ∘ Subtype.val) a } → { a // p a }

case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }), ?g (?f a) = a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }), ?f (?g b) = b

State before:
case f
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // p a } → { a // (p ∘ Subtype.val) a }

case g
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // (p ∘ Subtype.val) a } → { a // p a }

case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }), ?g (?f a) = a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }), ?f (?g b) = b
Tactic:
. exact fun x => ⟨⟨x.1, h x.1 x.2⟩, x.2⟩
State after:
case g
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // (p ∘ Subtype.val) a } → { a // p a }

case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }), ?g { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) } = a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }),
    { val := { val := (?g b).val, property := (_ : q (?g b).val) }, property := (_ : p (?g b).val) } = b

State before:
case g
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // (p ∘ Subtype.val) a } → { a // p a }

case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }), ?g { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) } = a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }),
    { val := { val := (?g b).val, property := (_ : q (?g b).val) }, property := (_ : p (?g b).val) } = b
Tactic:
. exact fun y => ⟨y.1.1, y.2⟩
State after:
case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }),
    { val := { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) }.val.val,
        property :=
          (_ :
            (p ∘ Subtype.val) { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) }.val) } =
      a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }),
    {
        val :=
          { val := { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val,
            property := (_ : q { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) },
        property := (_ : p { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) } =
      b

State before:
case hgf
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (a : { a // p a }),
    { val := { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) }.val.val,
        property :=
          (_ :
            (p ∘ Subtype.val) { val := { val := a.val, property := (_ : q a.val) }, property := (_ : p a.val) }.val) } =
      a

case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }),
    {
        val :=
          { val := { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val,
            property := (_ : q { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) },
        property := (_ : p { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) } =
      b
Tactic:
all_goals simp
State after:
no goals

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = count (p ∘ Subtype.val)
Tactic:
rewrite [count_eq_card]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ card { a // p a } = card { a // (p ∘ Subtype.val) a }

State before:
case f
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // p a } → { a // (p ∘ Subtype.val) a }
Tactic:
exact fun x => ⟨⟨x.1, h x.1 x.2⟩, x.2⟩
State after:
no goals

State before:
case g
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ { a // (p ∘ Subtype.val) a } → { a // p a }
Tactic:
exact fun y => ⟨y.1.1, y.2⟩
State after:
no goals

State before:
case hfg
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), p a → q a
⊢ ∀ (b : { a // (p ∘ Subtype.val) a }),
    {
        val :=
          { val := { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val,
            property := (_ : q { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) },
        property := (_ : p { val := b.val.val, property := (_ : (p ∘ Subtype.val) b.val) }.val) } =
      b
Tactic:
simp
State after:
no goals