Theorem: BishopFin.count_invimage_le_count_of_inj (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_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ count (p ∘ f) ≤ count p
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_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ card { a // (p ∘ f) a } ≤ card { a // p a }

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ card { a // (p ∘ f) a } ≤ card { a // p a }
Tactic:
refine card_le_card_of_inj ?f ?f_inj
State after:
case f
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ { a // (p ∘ f) a } → { a // p a }

case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ ∀ (a₁ a₂ : { a // (p ∘ f) a }), ?f a₁ = ?f a₂ → a₁ = a₂

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

case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ ∀ (a₁ a₂ : { a // (p ∘ f) a }), ?f a₁ = ?f a₂ → a₁ = a₂
Tactic:
. exact fun y => ⟨f y.1, y.2⟩
State after:
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ ∀ (a₁ a₂ : { a // (p ∘ f) a }),
    { val := f a₁.val, property := (_ : (p ∘ f) a₁.val) } = { val := f a₂.val, property := (_ : (p ∘ f) a₂.val) } →
      a₁ = a₂

State before:
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ ∀ (a₁ a₂ : { a // (p ∘ f) a }),
    { val := f a₁.val, property := (_ : (p ∘ f) a₁.val) } = { val := f a₂.val, property := (_ : (p ∘ f) a₂.val) } →
      a₁ = a₂
Tactic:
. intro y₁ y₂ h
  apply Subtype.eq; apply f_inj
  exact congrArg Subtype.val h
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_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ card { a // (p ∘ f) a } ≤ count p
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_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ card { a // (p ∘ f) a } ≤ card { a // p a }

State before:
case f
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ { a // (p ∘ f) a } → { a // p a }
Tactic:
exact fun y => ⟨f y.1, y.2⟩
State after:
no goals

State before:
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
⊢ ∀ (a₁ a₂ : { a // (p ∘ f) a }),
    { val := f a₁.val, property := (_ : (p ∘ f) a₁.val) } = { val := f a₂.val, property := (_ : (p ∘ f) a₂.val) } →
      a₁ = a₂
Tactic:
intro y₁ y₂ h
State after:
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁ = y₂

State before:
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁ = y₂
Tactic:
apply Subtype.eq
State after:
case f_inj.a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁.val = y₂.val

State before:
case f_inj.a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁.val = y₂.val
Tactic:
apply f_inj
State after:
case f_inj.a.a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ f y₁.val = f y₂.val

State before:
case f_inj.a.a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ f y₁.val = f y₂.val
Tactic:
exact congrArg Subtype.val h
State after:
no goals