internlm/Lean-Github huggingface dataset:
Theorem: BishopFin.count_split
Proof 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
)
Proof state after:
no goals
Theorem: BishopFin.count_split
Proof 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
)
Proof state after:
no goals
Theorem: BishopFin.count_split
Proof 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]
Proof 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 }
Theorem: BishopFin.count_split
Proof 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⟩
Proof 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₂
Theorem: BishopFin.count_split
Proof 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⟩
Proof 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₂
Theorem: BishopFin.count_split
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_split
Proof 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
Proof 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
Theorem: BishopFin.count_split
Proof 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⟩
Proof state after:
no goals
Theorem: BishopFin.count_split
Proof 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₂
Proof 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₂
Theorem: BishopFin.count_split
Proof 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]
Proof 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₂
Theorem: BishopFin.count_split
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_image_le_card
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
have := (elems α).countP_image_le_length nodup_elems (f := f)
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, a ∈ elems α ∧ f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Theorem: BishopFin.count_image_le_card
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, a ∈ elems α ∧ f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
simp only [mem_elems, true_and] at this
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Theorem: BishopFin.count_image_le_card
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
exact this
Proof state after:
no goals
Theorem: BishopFin.count_image_le_count
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, p a ∧ f a = b) ≤ count p
Tactic:
conv => rhs; rewrite [count_eq_card]
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, p a ∧ f a = b) ≤ card { a // p a }
Theorem: BishopFin.count_image_le_count
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, p a ∧ f a = b) ≤ card { a // p a }
Tactic:
refine trans (r:=Eq) ?_ (count_image_le_card (f ∘ Subtype.val))
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, p a ∧ f a = b) = count fun b => ∃ a, (f ∘ Subtype.val) a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, p a ∧ f a = b) = count fun b => ∃ a, (f ∘ Subtype.val) a = b
Tactic:
apply count_congr
Proof state after:
case h
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ ∀ (a : β), (∃ a_1, p a_1 ∧ f a_1 = a) ↔ ∃ a_1, (f ∘ Subtype.val) a_1 = a
Theorem: BishopFin.count_image_le_count
Proof state before:
case h
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ ∀ (a : β), (∃ a_1, p a_1 ∧ f a_1 = a) ↔ ∃ a_1, (f ∘ Subtype.val) a_1 = a
Tactic:
intro b
Proof state after:
case h
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) ↔ ∃ a, (f ∘ Subtype.val) a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) ↔ ∃ a, (f ∘ Subtype.val) a = b
Tactic:
constructor
Proof state after:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) → ∃ a, (f ∘ Subtype.val) a = b

case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) → ∃ a, (f ∘ Subtype.val) a = b

case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
Tactic:
. intro h; let ⟨a,hpa,hfa⟩ := h
  exact ⟨⟨a,hpa⟩, hfa⟩
Proof state after:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
Tactic:
. intro h; let ⟨⟨a,hpa⟩,hfa⟩ := h
  exact ⟨a,hpa,hfa⟩
Proof state after:
no goals
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) → ∃ a, (f ∘ Subtype.val) a = b
Tactic:
intro h
Proof state after:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, p a ∧ f a = b
⊢ ∃ a, (f ∘ Subtype.val) a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, p a ∧ f a = b
⊢ ∃ a, (f ∘ Subtype.val) a = b
Tactic:
let ⟨a,hpa,hfa⟩ := h
Proof state after:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, p a ∧ f a = b
a : α
hpa : p a
hfa : f a = b
⊢ ∃ a, (f ∘ Subtype.val) a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, p a ∧ f a = b
a : α
hpa : p a
hfa : f a = b
⊢ ∃ a, (f ∘ Subtype.val) a = b
Tactic:
exact ⟨⟨a,hpa⟩, hfa⟩
Proof state after:
no goals
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
Tactic:
intro h
Proof state after:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, (f ∘ Subtype.val) a = b
⊢ ∃ a, p a ∧ f a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, (f ∘ Subtype.val) a = b
⊢ ∃ a, p a ∧ f a = b
Tactic:
let ⟨⟨a,hpa⟩,hfa⟩ := h
Proof state after:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, (f ∘ Subtype.val) a = b
a : α
hpa : p a
hfa : (f ∘ Subtype.val) { val := a, property := hpa } = b
⊢ ∃ a, p a ∧ f a = b
Theorem: BishopFin.count_image_le_count
Proof state before:
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
h : ∃ a, (f ∘ Subtype.val) a = b
a : α
hpa : p a
hfa : (f ∘ Subtype.val) { val := a, property := hpa } = b
⊢ ∃ a, p a ∧ f a = b
Tactic:
exact ⟨a,hpa,hfa⟩
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
⊢ count p ≤ count (p ∘ f)
Tactic:
rewrite [count_eq_count_sub hf]
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Tactic:
let f' : β → {a // ∃ b, f b = a} := fun b => ⟨f b, b, rfl⟩
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Tactic:
have : f = Subtype.val ∘ f' := funext fun _ => rfl
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ f)
Tactic:
rewrite [this]
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ Subtype.val ∘ f')
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ count ((fun a => p a) ∘ Subtype.val) ≤ count (p ∘ Subtype.val ∘ f')
Tactic:
dsimp [count]
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ List.countP (fun a => decide (p a.val)) (elems { a // ∃ b, f b = a }) ≤
    List.countP (fun a => decide (p (f a))) (elems β)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ List.countP (fun a => decide (p a.val)) (elems { a // ∃ b, f b = a }) ≤
    List.countP (fun a => decide (p (f a))) (elems β)
Tactic:
conv =>
  rhs; equals ((elems β).map f').countP (fun a => decide (p a.val)) =>
    rewrite [List.countP_map]; rfl
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ List.countP (fun a => decide (p a.val)) (elems { a // ∃ b, f b = a }) ≤
    List.countP (fun a => decide (p a.val)) (List.map f' (elems β))
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ List.countP (fun a => decide (p a.val)) (elems { a // ∃ b, f b = a }) ≤
    List.countP (fun a => decide (p a.val)) (List.map f' (elems β))
Tactic:
refine List.countP_mono_right ?_ nodup_elems
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ elems { a // ∃ b, f b = a } ⊆ List.map f' (elems β)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
⊢ elems { a // ∃ b, f b = a } ⊆ List.map f' (elems β)
Tactic:
intro x _
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
x : { a // ∃ b, f b = a }
a✝ : x ∈ elems { a // ∃ b, f b = a }
⊢ x ∈ List.map f' (elems β)
Theorem: BishopFin.count_le_count_invimage
Proof state before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
x : { a // ∃ b, f b = a }
a✝ : x ∈ elems { a // ∃ b, f b = a }
⊢ x ∈ List.map f' (elems β)
Tactic:
simp only [List.mem_map]
Proof state after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
x : { a // ∃ b, f b = a }
a✝ : x ∈ elems { a // ∃ b, f b = a }
⊢ ∃ a, a ∈ elems β ∧ { val := f a, property := (_ : ∃ b, f b = f a) } = x