internlm/Lean-Github huggingface dataset:
Theorem: BishopFin.count_le_count_invimage
Proof 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
Proof 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) }
Theorem: BishopFin.count_le_count_invimage
Proof 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
Proof 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) }
Theorem: BishopFin.count_le_count_invimage
Proof 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)
Proof 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) }
Theorem: BishopFin.count_le_count_invimage
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage
Proof 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]
Proof 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 β)
Theorem: BishopFin.count_le_count_invimage
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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]
Proof 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 }
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof 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
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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⟩
Proof 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
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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]
Proof 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 }
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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⟩
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof 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
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof 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 }
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof 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 }
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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⟩
Proof 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 }
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof 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)
Theorem: BishopFin.count_le_count_invimage_of_surj
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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]
Proof 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 }
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof 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₂
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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⟩
Proof 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₂
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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]
Proof 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 }
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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⟩
Proof state after:
no goals
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof 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₂
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof 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
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof 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
Theorem: BishopFin.count_invimage_le_count_of_inj
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_bij
Proof 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 ?_ ?_
Proof 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
Theorem: BishopFin.count_eq_count_invimage_of_bij
Proof 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
Proof 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
Theorem: BishopFin.count_eq_count_invimage_of_bij
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_bij
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_bij
Proof 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
Proof state after:
no goals
Theorem: BishopFin.count_eq_count_invimage_of_inv
Proof state before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ count p = count (p ∘ f)
Tactic:
refine count_eq_count_invimage_of_bij f ?_ ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (a : α), ∃ b, f b = a

case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂