Theorem: BishopFin.count_le_count_invimage_of_surj (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
⊢ count p ≤ count (p ∘ f)
Tactic:
iterate rewrite [count_eq_card]
State after:
α : 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
⊢ card { a // p a } ≤ card { a // (p ∘ f) a }

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
⊢ card { a // p a } ≤ card { a // (p ∘ f) a }
Tactic:
refine card_ge_card_of_surj ?f ?f_surj
State after:
case f
α : 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
⊢ { a // (p ∘ f) a } → { a // p a }

case f_surj
α : 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
⊢ ∀ (b : { a // p a }), ∃ a, ?f a = b

State before:
case f
α : 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
⊢ { a // (p ∘ f) a } → { a // p a }

case f_surj
α : 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
⊢ ∀ (b : { a // p a }), ∃ a, ?f a = b
Tactic:
. exact fun y => ⟨f y.1, y.2⟩
State after:
case f_surj
α : 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
⊢ ∀ (b : { a // p a }), ∃ a, { val := f a.val, property := (_ : (p ∘ f) a.val) } = b

State before:
case f_surj
α : 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
⊢ ∀ (b : { a // p a }), ∃ a, { val := f a.val, property := (_ : (p ∘ f) a.val) } = b
Tactic:
. intro x
  let ⟨a,ha⟩ := x
  let ⟨b,hb⟩ := f_surj a
  exists ⟨b, by dsimp; exact hb ▸ ha⟩
  exact Subtype.eq hb
State after:
no goals

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
⊢ card { a // p a } ≤ count (p ∘ f)
Tactic:
rewrite [count_eq_card]
State after:
α : 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
⊢ card { a // p a } ≤ card { a // (p ∘ f) a }

State before:
case f
α : 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
⊢ { a // (p ∘ f) a } → { a // p a }
Tactic:
exact fun y => ⟨f y.1, y.2⟩
State after:
no goals

State before:
case f_surj
α : 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
⊢ ∀ (b : { a // p a }), ∃ a, { val := f a.val, property := (_ : (p ∘ f) a.val) } = b
Tactic:
intro x
State after:
case f_surj
α : 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
x : { a // p a }
⊢ ∃ a, { val := f a.val, property := (_ : (p ∘ f) a.val) } = x

State before:
case f_surj
α : 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
x : { a // p a }
⊢ ∃ a, { val := f a.val, property := (_ : (p ∘ f) a.val) } = x
Tactic:
let ⟨a,ha⟩ := x
State after:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
⊢ ∃ a_1, { val := f a_1.val, property := (_ : (p ∘ f) a_1.val) } = { val := a, property := ha }

State before:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
⊢ ∃ a_1, { val := f a_1.val, property := (_ : (p ∘ f) a_1.val) } = { val := a, property := ha }
Tactic:
let ⟨b,hb⟩ := f_surj a
State after:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ ∃ a_1, { val := f a_1.val, property := (_ : (p ∘ f) a_1.val) } = { val := a, property := ha }

State before:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ ∃ a_1, { val := f a_1.val, property := (_ : (p ∘ f) a_1.val) } = { val := a, property := ha }
Tactic:
exists ⟨b, by dsimp; exact hb ▸ ha⟩
State after:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ { val := f { val := b, property := (_ : (p ∘ f) b) }.val,
      property := (_ : (p ∘ f) { val := b, property := (_ : (p ∘ f) b) }.val) } =
    { val := a, property := ha }

State before:
case f_surj
α : 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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ { val := f { val := b, property := (_ : (p ∘ f) b) }.val,
      property := (_ : (p ∘ f) { val := b, property := (_ : (p ∘ f) b) }.val) } =
    { val := a, property := ha }
Tactic:
exact Subtype.eq hb
State after:
no goals

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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ (p ∘ f) b
Tactic:
dsimp
State after:
α : 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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ p (f b)

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
x : { a // p a }
a : α
ha : p a
b : β
hb : f b = a
⊢ p (f b)
Tactic:
exact hb ▸ ha
State after:
no goals