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

State before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α = card β
Tactic:
refine Nat.le_antisymm ?_ ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
. show card α ≤ card β
  refine card_le_card_of_inj f ?_
  intros a₁ a₂ hfa
  rw [← hgf a₁, ← hgf a₂, hfa]
State after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
. show card β ≤ card α
  refine card_le_card_of_inj g ?_
  intro b₁ b₂ hgb
  rw [← hfg b₁, ← hfg b₂, hgb]
State after:
no goals

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β
Tactic:
refine card_le_card_of_inj f ?_
State after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
Tactic:
intros a₁ a₂ hfa
State after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
a₁ a₂ : α
hfa : f a₁ = f a₂
⊢ a₁ = a₂

State before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
a₁ a₂ : α
hfa : f a₁ = f a₂
⊢ a₁ = a₂
Tactic:
rw [← hgf a₁, ← hgf a₂, hfa]
State after:
no goals

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
refine card_le_card_of_inj g ?_
State after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : β), g a₁ = g a₂ → a₁ = a₂

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : β), g a₁ = g a₂ → a₁ = a₂
Tactic:
intro b₁ b₂ hgb
State after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
b₁ b₂ : β
hgb : g b₁ = g b₂
⊢ b₁ = b₂

State before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
b₁ b₂ : β
hgb : g b₁ = g b₂
⊢ b₁ = b₂
Tactic:
rw [← hfg b₁, ← hfg b₂, hgb]
State after:
no goals