Theorem: exists_hasSliceRankLE (LeanCamCombi/SliceRank.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
⊢ ∃ n, HasSliceRankLE n f
Tactic:
cases nonempty_fintype ι
State after:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
⊢ ∃ n, HasSliceRankLE n f

State before:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
⊢ ∃ n, HasSliceRankLE n f
Tactic:
have (i) := Fintype.ofFinite (α i)
State after:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
this : (i : ι) → Fintype (α i)
⊢ ∃ n, HasSliceRankLE n f

State before:
case intro
ι : Type u_1
R : Type u_2
inst✝³ : DecidableEq ι
α : ι → Type u_3
inst✝² : Semiring R
m n : ℕ
f✝ f₁ f₂ : ((i : ι) → α i) → R
inst✝¹ : Finite ι
inst✝ : ∀ (i : ι), Finite (α i)
f : ((i : ι) → α i) → R
val✝ : Fintype ι
this : (i : ι) → Fintype (α i)
⊢ ∃ n, HasSliceRankLE n f
Tactic:
exact ⟨_, hasSliceRankLE_card _⟩
State after:
no goals