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

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count p = count (p ∘ f)
Tactic:
refine Nat.le_antisymm ?_ ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count p ≤ count (p ∘ f)

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p

State before:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count p ≤ count (p ∘ f)

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p
Tactic:
. exact count_le_count_invimage_of_surj f f_surj
State after:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p

State before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p
Tactic:
. exact count_invimage_le_count_of_inj f f_inj
State after:
no goals

State before:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count p ≤ count (p ∘ f)
Tactic:
exact count_le_count_invimage_of_surj f f_surj
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_surj : ∀ (a : α), ∃ b, f b = a
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p
Tactic:
exact count_invimage_le_count_of_inj f f_inj
State after:
no goals