Theorem: OnCycleFactors.Fintype.card_pfun (Jordan/ConjClassCount.lean)

State before:
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
by_cases hp : p
State after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1

case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1

State before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
simp only [dif_pos hp]
State after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = Fintype.card (β hp)

State before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Fintype.card ((hp : p) → β hp) = Fintype.card (β hp)
Tactic:
rw [Fintype.card_eq]
State after:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Nonempty (((hp : p) → β hp) ≃ β hp)

State before:
case pos
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : p
⊢ Nonempty (((hp : p) → β hp) ≃ β hp)
Tactic:
exact ⟨@Equiv.funUnique p (β hp) (uniqueProp hp)⟩
State after:
no goals

State before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = if h : p then Fintype.card (β h) else 1
Tactic:
simp only [dif_neg hp]
State after:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = 1

State before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ Fintype.card ((hp : p) → β hp) = 1
Tactic:
rw [Fintype.card_eq_one_iff]
State after:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∃ x, ∀ (y : (hp : p) → β hp), y = x

State before:
case neg
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∃ x, ∀ (y : (hp : p) → β hp), y = x
Tactic:
use (fun h => False.elim (hp h))
State after:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∀ (y : (hp : p) → β hp), y = fun h => ⋯.elim

State before:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
⊢ ∀ (y : (hp : p) → β hp), y = fun h => ⋯.elim
Tactic:
intro u
State after:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
⊢ u = fun h => ⋯.elim

State before:
case h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
⊢ u = fun h => ⋯.elim
Tactic:
ext h
State after:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ u h = ⋯.elim

State before:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ u h = ⋯.elim
Tactic:
exfalso
State after:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ False

State before:
case h.h
α : Type ?u.398702
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
p : Prop
inst✝¹ : Decidable p
β : p → Type u_1
inst✝ : (hp : p) → Fintype (β hp)
hp : ¬p
u : (hp : p) → β hp
h : p
⊢ False
Tactic:
exact hp h
State after:
no goals