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

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]
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 }

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))
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

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
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

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
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

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
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

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⟩
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

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⟩
State after:
no goals

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
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

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
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

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⟩
State after:
no goals

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
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

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
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

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⟩
State after:
no goals