internlm/Lean-Github huggingface dataset:
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : β), g a₁ = g a₂ → a₁ = a₂
Tactic:
intro b₁ b₂ hgb
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
b₁ b₂ : β
hgb : g b₁ = g b₂
⊢ b₁ = b₂
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
b₁ b₂ : β
hgb : g b₁ = g b₂
⊢ b₁ = b₂
Tactic:
rw [← hfg b₁, ← hfg b₂, hgb]
Proof state after:
no goals
Theorem: BishopFin.card_sum_eq
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ card (α ⊕ β) = card α + card β
Tactic:
show ((elems α).map Sum.inl ++ (elems β).map Sum.inr).length = _
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (List.map Sum.inl (elems α) ++ List.map Sum.inr (elems β)) = card α + card β
Theorem: BishopFin.card_sum_eq
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (List.map Sum.inl (elems α) ++ List.map Sum.inr (elems β)) = card α + card β
Tactic:
simp only [List.length_append, List.length_map]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (elems α) + List.length (elems β) = card α + card β
Theorem: BishopFin.card_sum_eq
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
⊢ List.length (elems α) + List.length (elems β) = card α + card β
Tactic:
rfl
Proof state after:
no goals
Theorem: BishopFin.card_subset_le_card
Proof state before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ card { a // p a } ≤ card α
Tactic:
apply card_le_card_of_inj Subtype.val
Proof state after:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ ∀ (a₁ a₂ : { a // p a }), a₁.val = a₂.val → a₁ = a₂
Theorem: BishopFin.card_subset_le_card
Proof state before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ ∀ (a₁ a₂ : { a // p a }), a₁.val = a₂.val → a₁ = a₂
Tactic:
intro _ _
Proof state after:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
a₁✝ a₂✝ : { a // p a }
⊢ a₁✝.val = a₂✝.val → a₁✝ = a₂✝
Theorem: BishopFin.card_subset_le_card
Proof state before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
a₁✝ a₂✝ : { a // p a }
⊢ a₁✝.val = a₂✝.val → a₁✝ = a₂✝
Tactic:
exact Subtype.eq
Proof state after:
no goals
Theorem: BishopFin.count_eq_card
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count p = card { a // p a }
Tactic:
dsimp [count]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide (p a)) (elems α) = card { a // p a }
Theorem: BishopFin.count_eq_card
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide (p a)) (elems α) = card { a // p a }
Tactic:
rewrite [List.countP_eq_length_filter]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = card { a // p a }
Theorem: BishopFin.count_eq_card
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = card { a // p a }
Tactic:
conv => rhs; change subtype (p:=p) |>.elems' |>.length
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = List.length elems'
Theorem: BishopFin.count_eq_card
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = List.length elems'
Tactic:
dsimp [elems']
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) =
    List.length
      (List.pmap Subtype.mk (List.filter (fun a => decide (p a)) (elems α))
        (_ : ∀ (a : α), a ∈ List.filter (fun a => decide (p a)) (elems α) → p a))
Theorem: BishopFin.count_eq_card
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) =
    List.length
      (List.pmap Subtype.mk (List.filter (fun a => decide (p a)) (elems α))
        (_ : ∀ (a : α), a ∈ List.filter (fun a => decide (p a)) (elems α) → p a))
Tactic:
simp only [List.length_pmap]
Proof state after:
no goals
Theorem: BishopFin.count_true
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun x => True) = card α
Tactic:
dsimp [count]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => true) (elems α) = card α
Theorem: BishopFin.count_true
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => true) (elems α) = card α
Tactic:
rewrite [List.countP_true]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = card α
Theorem: BishopFin.count_true
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = card α
Tactic:
rfl
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_sub
Proof 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]
Proof 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 }
Theorem: BishopFin.count_eq_count_sub
Proof 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
Proof 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
Theorem: BishopFin.count_eq_count_sub
Proof 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⟩
Proof 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
Theorem: BishopFin.count_eq_count_sub
Proof 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⟩
Proof 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
Theorem: BishopFin.count_eq_count_sub
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_sub
Proof 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]
Proof 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 }
Theorem: BishopFin.count_eq_count_sub
Proof 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⟩
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_sub
Proof 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⟩
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_sub
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_le_one_of_unique
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ count p ≤ 1
Tactic:
dsimp [count]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ List.countP (fun a => decide (p a)) (elems α) ≤ 1
Theorem: BishopFin.count_le_one_of_unique
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ List.countP (fun a => decide (p a)) (elems α) ≤ 1
Tactic:
refine List.countP_le_one_of_unique_nodup ?_ nodup_elems
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), decide (p a) = true → decide (p b) = true → a = b
Theorem: BishopFin.count_le_one_of_unique
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), decide (p a) = true → decide (p b) = true → a = b
Tactic:
simp only [decide_eq_true_eq]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), p a → p b → a = b
Theorem: BishopFin.count_le_one_of_unique
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), p a → p b → a = b
Tactic:
exact p_unique
Proof state after:
no goals
Theorem: BishopFin.card_eq_count_add_count_not
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card α = count p + count fun a => ¬p a
Tactic:
dsimp [card]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = count p + count fun a => ¬p a
Theorem: BishopFin.card_eq_count_add_count_not
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = count p + count fun a => ¬p a
Tactic:
rewrite [(elems α).length_eq_countP_add_countP p]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun b => decide (p b)) (elems α) + List.countP (fun a => decide ¬decide (p a) = true) (elems α) =
    count p + count fun a => ¬p a
Theorem: BishopFin.card_eq_count_add_count_not
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬decide (p a) = true) (elems α) = count fun a => ¬p a
Tactic:
simp only [decide_eq_true_eq]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬p a) (elems α) = count fun a => ¬p a
Theorem: BishopFin.card_eq_count_add_count_not
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬p a) (elems α) = count fun a => ¬p a
Tactic:
rfl
Proof state after:
no goals
Theorem: BishopFin.count_or_le_add
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => p a ∨ q a) ≤ count p + count q
Tactic:
dsimp [count]
Proof state after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide (p a ∨ q a)) (elems α) ≤
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Theorem: BishopFin.count_or_le_add
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide (p a ∨ q a)) (elems α) ≤
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Tactic:
simp only [decide_or, List.countP_or_le_add]
Proof state after:
no goals
Theorem: BishopFin.count_disjoint_or
Proof 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 fun a => p a ∨ q a) = count p + count q
Tactic:
dsimp [count]
Proof 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)
⊢ List.countP (fun a => decide (p a ∨ q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Theorem: BishopFin.count_disjoint_or
Proof 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)
⊢ List.countP (fun a => decide (p a ∨ q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Tactic:
simp only [decide_or]
Proof 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)
⊢ List.countP (fun a => decide (p a) || decide (q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Theorem: BishopFin.count_disjoint_or
Proof 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)
⊢ List.countP (fun a => decide (p a) || decide (q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Tactic:
apply List.countP_disjoint
Proof state after:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), (decide (p a) && decide (q a)) = false
Theorem: BishopFin.count_disjoint_or
Proof state before:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), (decide (p a) && decide (q a)) = false
Tactic:
simp only [← decide_and, decide_eq_false_iff_not]
Proof state after:
case h
α : 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 ∧ q a)
Theorem: BishopFin.count_disjoint_or
Proof state before:
case h
α : 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 ∧ q a)
Tactic:
exact h
Proof state after:
no goals
Theorem: BishopFin.count_split
Proof 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)]
Proof 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
Theorem: BishopFin.count_split
Proof 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 _ ?_) ?_
Proof 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