Theorem: BishopFin.count_le_count_invimage (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 : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
⊢ count p ≤ count (p ∘ f)
Tactic:
rewrite [count_eq_count_sub hf]
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)

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

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

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

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

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

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

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

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

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 }
⊢ ∃ a, a ∈ elems β ∧ { val := f a, property := (_ : ∃ b, f b = f a) } = x
Tactic:
let ⟨a,b,ha⟩ := x
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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ ∃ a_1,
    a_1 ∈ elems β ∧ { val := f a_1, property := (_ : ∃ b, f b = f a_1) } = { val := a, property := (_ : ∃ b, f b = a) }

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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ ∃ a_1,
    a_1 ∈ elems β ∧ { val := f a_1, property := (_ : ∃ b, f b = f a_1) } = { val := a, property := (_ : ∃ b, f b = a) }
Tactic:
exists b
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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ b ∈ elems β ∧ { val := f b, property := (_ : ∃ b_1, f b_1 = f b) } = { val := a, property := (_ : ∃ b, f b = a) }

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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ b ∈ elems β ∧ { val := f b, property := (_ : ∃ b_1, f b_1 = f b) } = { val := a, property := (_ : ∃ b, f b = a) }
Tactic:
apply And.intro (mem_elems b)
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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ { val := f b, property := (_ : ∃ b_1, f b_1 = f b) } = { val := a, property := (_ : ∃ b, f b = a) }

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 : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ { val := f b, property := (_ : ∃ b_1, f b_1 = f b) } = { val := a, property := (_ : ∃ b, f b = a) }
Tactic:
exact Subtype.eq ha
State after:
no goals

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 (f a))) (elems β) = List.countP (fun a => decide (p a.val)) (List.map f' (elems β))
Tactic:
rewrite [List.countP_map]
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 (f a))) (elems β) = List.countP ((fun a => decide (p a.val)) ∘ f') (elems β)

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 (f a))) (elems β) = List.countP ((fun a => decide (p a.val)) ∘ f') (elems β)
Tactic:
rfl
State after:
no goals