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

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 ?_ ?_
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₂

State before:
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₂
Tactic:
. exact fun a => ⟨g a, hfg a⟩
State after:
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₂

State before:
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₂
Tactic:
. intro b₁ b₂ hb
  rw [← hgf b₁, ← hgf b₂, hb]
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 : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (a : α), ∃ b, f b = a
Tactic:
exact fun a => ⟨g a, hfg a⟩
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 : β → α
g : α → β
hgf : ∀ (b : β), g (f b) = b
hfg : ∀ (a : α), f (g a) = a
⊢ ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
Tactic:
intro b₁ b₂ hb
State after:
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₂ : β
hb : f b₁ = f b₂
⊢ b₁ = b₂

State before:
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₂ : β
hb : f b₁ = f b₂
⊢ b₁ = b₂
Tactic:
rw [← hgf b₁, ← hgf b₂, hb]
State after:
no goals