rcases t_minimal s lt with ⟨i, hin, hi, his⟩
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
⊢ False
case intro.intro.intro
M : Type u_1
inst✝⁷ : Zero M
inst✝⁶ : One M
inst✝⁵ : Add M
inst✝⁴ : Mul M
inst✝³ : LT M
inst✝² : M ⊧ₘ* 𝐈𝚺₁
m : ℕ
inst✝¹ : Fact (1 ≤ m)
inst✝ : M ⊧ₘ* 𝐈𝐍𝐃𝚺 m
Γ : Polarity
P : M → Prop
hP : (Γ.coe, m)-Predicate P
a : M
this✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
hsn : s < exp a
hs : ∀ i < a, P i → i ∈ s
this : (Γ.alt.coe, m)-Predicate fun s => ∀ i < a, P i → i ∈ s
t : M
ht : ∀ i < a, P i → i ∈ t
t_minimal : ∀ t' < t, ∃ x < a, P x ∧ x ∉ t'
lt : s < t
i : M
hin : i < a
hi : P i
his : i ∉ s
⊢ False